tools/checkers/vcc.py

   1 #!/usr/bin/env python
   2 #
   3 # Copyright (c) 2010 Martin Decky
   4 # Copyright (c) 2010 Ondrej Sery
   5 # All rights reserved.
   6 #
   7 # Redistribution and use in source and binary forms, with or without
   8 # modification, are permitted provided that the following conditions
   9 # are met:
  10 #
  11 # - Redistributions of source code must retain the above copyright
  12 #   notice, this list of conditions and the following disclaimer.
  13 # - Redistributions in binary form must reproduce the above copyright
  14 #   notice, this list of conditions and the following disclaimer in the
  15 #   documentation and/or other materials provided with the distribution.
  16 # - The name of the author may not be used to endorse or promote products
  17 #   derived from this software without specific prior written permission.
  18 #
  19 # THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
  20 # IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
  21 # OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
  22 # IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
  23 # INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
  24 # NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
  25 # DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
  26 # THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
  27 # (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
  28 # THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  29 #
  30 """
  31 Wrapper for Vcc checker
  32 """
  33
  34 import sys
  35 import os
  36 import subprocess
  37 import jobfile
  38 import re
  39
  40 jobs = [
  41         "kernel/kernel.job"
  42 ]
  43
  44 re_attribute = re.compile("__attribute__\s*\(\(.*\)\)")
  45 re_va_list = re.compile("__builtin_va_list")
  46
  47 specification = ""
  48
  49 def usage(prname):
  50         "Print usage syntax"
  51         print(prname + " <ROOT> [VCC_PATH]")
  52
  53 def cygpath(upath):
  54         "Convert Unix (Cygwin) path to Windows path"
  55
  56         return subprocess.Popen(['cygpath', '--windows', '--absolute', upath], stdout = subprocess.PIPE).communicate()[0].strip()
  57
  58 def preprocess(srcfname, tmpfname, base, options):
  59         "Preprocess source using GCC preprocessor and compatibility tweaks"
  60
  61         global specification
  62
  63         args = ['gcc', '-E']
  64         args.extend(options.split())
  65         args.extend(['-DCONFIG_VERIFY_VCC=1', srcfname])
  66
  67         # Change working directory
  68
  69         cwd = os.getcwd()
  70         os.chdir(base)
  71
  72         preproc = subprocess.Popen(args, stdout = subprocess.PIPE).communicate()[0]
  73
  74         tmpf = open(tmpfname, "w")
  75         tmpf.write(specification)
  76
  77         for line in preproc.splitlines():
  78
  79                 # Ignore preprocessor directives
  80
  81                 if (line.startswith('#')):
  82                         continue
  83
  84                 # Remove __attribute__((.*)) GCC extension
  85
  86                 line = re.sub(re_attribute, "", line)
  87
  88                 # Ignore unsupported __builtin_va_list type
  89                 # (a better solution replacing __builrin_va_list with
  90                 # an emulated implementation is needed)
  91
  92                 line = re.sub(re_va_list, "void *", line)
  93
  94                 tmpf.write("%s\n" % line)
  95
  96         tmpf.close()
  97
  98         os.chdir(cwd)
  99
 100         return True
 101
 102 def vcc(vcc_path, root, job):
 103         "Run Vcc on a jobfile"
 104
 105         # Parse jobfile
 106
 107         inname = os.path.join(root, job)
 108
 109         if (not os.path.isfile(inname)):
 110                 print("Unable to open %s" % inname)
 111                 print("Did you run \"make precheck\" on the source tree?")
 112                 return False
 113
 114         inf = open(inname, "r")
 115         records = inf.read().splitlines()
 116         inf.close()
 117
 118         for record in records:
 119                 arg = jobfile.parse_arg(record)
 120                 if (not arg):
 121                         return False
 122
 123                 if (len(arg) < 6):
 124                         print("Not enough jobfile record arguments")
 125                         return False
 126
 127                 srcfname = arg[0]
 128                 tgtfname = arg[1]
 129                 tool = arg[2]
 130                 category = arg[3]
 131                 base = arg[4]
 132                 options = arg[5]
 133
 134                 srcfqname = os.path.join(base, srcfname)
 135                 if (not os.path.isfile(srcfqname)):
 136                         print("Source %s not found" % srcfqname)
 137                         return False
 138
 139                 tmpfname = "%s.preproc" % srcfname
 140                 tmpfqname = os.path.join(base, tmpfname)
 141
 142                 vccfname = "%s.i" % srcfname
 143                 vccfqname = os.path.join(base, vccfname);
 144
 145                 # Only C files are interesting for us
 146                 if (tool != "cc"):
 147                         continue
 148
 149                 # Preprocess sources
 150
 151                 if (not preprocess(srcfname, tmpfname, base, options)):
 152                         return False
 153
 154                 # Run Vcc
 155                 print(" -- %s --" % srcfname)
 156                 retval = subprocess.Popen([vcc_path, '/pointersize:32', '/newsyntax', cygpath(tmpfqname)]).wait()
 157
 158                 if (retval != 0):
 159                         return False
 160
 161                 # Cleanup, but only if verification was successful
 162                 # (to be able to examine the preprocessed file)
 163
 164                 if (os.path.isfile(tmpfqname)):
 165                         os.remove(tmpfqname)
 166                         os.remove(vccfqname)
 167
 168         return True
 169
 170 def main():
 171         global specification
 172
 173         if (len(sys.argv) < 2):
 174                 usage(sys.argv[0])
 175                 return
 176
 177         rootdir = os.path.abspath(sys.argv[1])
 178         if (len(sys.argv) > 2):
 179                 vcc_path = sys.argv[2]
 180         else:
 181                 vcc_path = "/cygdrive/c/Program Files (x86)/Microsoft Research/Vcc/Binaries/vcc"
 182
 183         if (not os.path.isfile(vcc_path)):
 184                 print("%s is not a binary." % vcc_path)
 185                 print("Please supply the full Cygwin path to Vcc as the second argument.")
 186                 return
 187
 188         config = os.path.join(rootdir, "HelenOS.config")
 189
 190         if (not os.path.isfile(config)):
 191                 print("%s not found." % config)
 192                 print("Please specify the path to HelenOS build tree root as the first argument.")
 193                 return
 194
 195         specpath = os.path.join(rootdir, "tools/checkers/vcc.h")
 196         if (not os.path.isfile(specpath)):
 197                 print("%s not found." % config)
 198                 return
 199
 200         specfile = file(specpath, "r")
 201         specification = specfile.read()
 202         specfile.close()
 203
 204         for job in jobs:
 205                 if (not vcc(vcc_path, rootdir, job)):
 206                         print()
 207                         print("Failed job: %s" % job)
 208                         return
 209
 210         print()
 211         print("All jobs passed")
 212
 213 if __name__ == '__main__':
 214         main()