|
1 | 1 | #!/usr/bin/env python
|
2 | 2 |
|
3 | 3 | """
|
| 4 | +Check that every process in a file has correct readsets and writesets. |
4 | 5 |
|
5 | 6 | Copyright (C) Sarah Mount, 2010.
|
6 | 7 |
|
|
22 | 23 | import compiler.ast as ast
|
23 | 24 | import compiler.visitor as visitor
|
24 | 25 |
|
25 |
| -import csp.tracer.icode as icode |
| 26 | +import exstatic.cspwarnings |
26 | 27 |
|
27 |
| -from csp.tracer.stack import Stack |
28 | 28 |
|
29 | 29 | __author__ = 'Sarah Mount <s.mount@wlv.ac.uk>'
|
30 | 30 | __date__ = 'April 2010'
|
31 | 31 |
|
32 | 32 |
|
33 | 33 | class ChannelChecker(visitor.ASTVisitor):
|
| 34 | + """Check that documented readsets and writesets are correct |
| 35 | + w.r.t. code. |
| 36 | + """ |
34 | 37 |
|
35 |
| - def __init__(self): |
| 38 | + def __init__(self, filename): |
36 | 39 | visitor.ASTVisitor.__init__(self)
|
37 |
| - self.model = '\n' |
38 |
| - self.processes = Stack() |
| 40 | + self.filename = filename |
| 41 | + self.current_process = '' |
| 42 | + self.current_process_lineno = 0 |
| 43 | + self.writeset = {} |
| 44 | + self.readset = {} |
| 45 | + self.readset_lineno = 0 |
| 46 | + self.writeset_lineno = 0 |
39 | 47 | return
|
40 | 48 |
|
41 | 49 | def extract_sets(self, doc):
|
| 50 | + """Extract the readset and writeset from function |
| 51 | + documentation. |
| 52 | + """ |
42 | 53 | readset = []
|
43 | 54 | writeset = []
|
44 |
| - if doc is None: |
45 |
| - return readset, writeset |
46 |
| - for line in doc.split('\n'): |
47 |
| - words = line.strip().split('=') |
48 |
| - if words is not None: |
49 |
| - if words[0].strip() == 'readset': |
50 |
| - chans = words[1].strip().split(',') |
51 |
| - readset = filter(lambda y: y is not '', |
52 |
| - map(lambda x: x.strip(), chans)) |
53 |
| - elif words[0].strip() == 'writeset': |
54 |
| - chans = words[1].strip().split(',') |
55 |
| - writeset = filter(lambda y: y is not '', |
56 |
| - map(lambda x: x.strip(), chans)) |
57 |
| - else: |
58 |
| - continue |
59 |
| - return readset, writeset |
| 55 | + has_readset = False |
| 56 | + has_writeset = False |
| 57 | + lineno = 0 |
| 58 | + if doc is not None: |
| 59 | + for line in doc.split('\n'): |
| 60 | + lineno += 1 |
| 61 | + words = line.strip().split('=') |
| 62 | + if words is not None: |
| 63 | + if words[0].strip() == 'readset': |
| 64 | + has_readset = True |
| 65 | + self.readset_lineno += lineno |
| 66 | + chans = words[1].strip().split(',') |
| 67 | + readset = filter(lambda y: y is not '', |
| 68 | + map(lambda x: x.strip(), chans)) |
| 69 | + elif words[0].strip() == 'writeset': |
| 70 | + has_writeset = True |
| 71 | + self.writeset_lineno += lineno |
| 72 | + chans = words[1].strip().split(',') |
| 73 | + writeset = filter(lambda y: y is not '', |
| 74 | + map(lambda x: x.strip(), chans)) |
| 75 | + |
| 76 | + # 'W002':'No readset given in documentation.' |
| 77 | + if not has_readset: |
| 78 | + exstatic.cspwarnings.create_error(self.filename, |
| 79 | + self.readset_lineno, |
| 80 | + self.current_process, |
| 81 | + 'W002') |
| 82 | + |
| 83 | + # 'W003':'No writeset given in documentation.' |
| 84 | + if not has_writeset: |
| 85 | + exstatic.cspwarnings.create_error(self.filename, |
| 86 | + self.writeset_lineno, |
| 87 | + self.current_process, |
| 88 | + 'W003') |
| 89 | + |
| 90 | + return set(readset), set(writeset) |
60 | 91 |
|
61 | 92 | def is_process(self, decorators):
|
| 93 | + """Determine whether or not the current function is a CSP |
| 94 | + process. |
| 95 | + """ |
62 | 96 | for decorator in decorators:
|
63 |
| - if (decorator.name == 'process' or |
64 |
| - decorator.name == 'forever'): |
| 97 | + if (decorator.name == 'process' or decorator.name == 'forever'): |
65 | 98 | return True
|
66 | 99 | return False
|
67 | 100 |
|
| 101 | + def check_sets(self, readset, writeset): |
| 102 | + """Check that the documented readset and writeset of the |
| 103 | + current function match the code inside the function |
| 104 | + definition. |
| 105 | +
|
| 106 | + @param readset the documented readset of the current process |
| 107 | + @param writeset the documented writeset of the current process |
| 108 | + """ |
| 109 | + # 'W001':'Channel in both readset and writeset.' |
| 110 | + if len(readset.intersection(writeset)) > 0: |
| 111 | + exstatic.cspwarnings.create_error(self.filename, |
| 112 | + self.readset_lineno, |
| 113 | + self.current_process, |
| 114 | + 'W001') |
| 115 | + |
| 116 | + # 'E004':'Channel appears in documented readset but not read |
| 117 | + # from in function body.' |
| 118 | + diff = set(self.readset.values()).difference(readset) |
| 119 | + for channel in diff: |
| 120 | + exstatic.cspwarnings.create_error(self.filename, |
| 121 | + self.readset_lineno, |
| 122 | + self.current_process, |
| 123 | + 'E004') |
| 124 | + |
| 125 | + # 'E005':'Channel is read from in function body but does not |
| 126 | + # appear in documented readset' |
| 127 | + diff = set(readset).difference(self.readset.values()) |
| 128 | + for channel in diff: |
| 129 | + for key in self.readset: |
| 130 | + exstatic.cspwarnings.create_error(self.filename, |
| 131 | + key, |
| 132 | + self.current_process, |
| 133 | + 'E005') |
| 134 | + |
| 135 | + # 'E006':'Channel appears in documented writeset but not |
| 136 | + # written to in function body.' |
| 137 | + diff = set(self.writeset.values()).difference(writeset) |
| 138 | + for channel in diff: |
| 139 | + exstatic.cspwarnings.create_error(self.filename, |
| 140 | + self.writeset_lineno, |
| 141 | + self.current_process, |
| 142 | + 'E006') |
| 143 | + |
| 144 | + # 'E007':'Channel is written to in function body but does not |
| 145 | + # appear in documented writeset' |
| 146 | + diff = set(writeset).difference(self.writeset.values()) |
| 147 | + for channel in diff: |
| 148 | + for key in self.writeset: |
| 149 | + exstatic.cspwarnings.create_error(self.filename, |
| 150 | + key, |
| 151 | + self.current_process, |
| 152 | + 'E007') |
| 153 | + |
| 154 | + return |
| 155 | + |
68 | 156 | def visitFunction(self, node):
|
69 |
| -# print "VISIT FUNCTION!", dir(node) |
70 |
| -# print node.code.__class__ |
| 157 | + """Visit function definition. |
| 158 | + """ |
| 159 | + |
| 160 | + # If this function definition is not a CSP process, ignore it. |
71 | 161 | if (node.decorators is None or
|
72 |
| - self.is_process(node.decorators) is None): |
| 162 | + self.is_process(node.decorators) is None): |
73 | 163 | return
|
74 |
| - print 'Function %s is a CSP process' % node.name |
| 164 | + |
| 165 | + # Store useful information about this process. |
| 166 | + self.current_process = node.name |
| 167 | + self.current_process_lineno = node.lineno |
| 168 | + self.readset_lineno, self.writeset_lineno = node.lineno, node.lineno |
75 | 169 | readset, writeset = self.extract_sets(node.doc)
|
76 |
| - print node.name, 'has readset:', readset, len(readset) |
77 |
| - print node.name, 'has writeset:', writeset, len(writeset) |
| 170 | + |
| 171 | + # 'I001':'Function is a CSP process or server process', |
| 172 | + exstatic.cspwarnings.create_error(self.filename, |
| 173 | + self.current_process_lineno, |
| 174 | + self.current_process, |
| 175 | + 'I001') |
| 176 | + |
| 177 | + # 'E002':'Channel in readset is not a formal parameter to this |
| 178 | + # process.', |
78 | 179 | for channel in readset:
|
79 | 180 | if not channel in node.argnames:
|
80 |
| - print 'ERROR line %i: Channel %s in readset is not a formal parameter to this process' % (node.lineno, channel) |
| 181 | + exstatic.cspwarnings.create_error(self.filename, |
| 182 | + self.readset_lineno, |
| 183 | + node.name, |
| 184 | + 'E002') |
| 185 | + |
| 186 | + # 'E003':'Channel in writeset is not a formal parameter to |
| 187 | + # this process.', |
81 | 188 | for channel in writeset:
|
82 | 189 | if not channel in node.argnames:
|
83 |
| - print 'ERROR line %i: Channel %s in writeset is not a formal parameter to this process' % (node.lineno, channel) |
| 190 | + exstatic.cspwarnings.create_error(self.filename, |
| 191 | + self.writeset_lineno, |
| 192 | + node.name, |
| 193 | + 'E003') |
84 | 194 |
|
85 |
| - # Ensure that we visit every line of code in this function. |
| 195 | + # Ensure that we visit every statement inside this fuction. |
86 | 196 | for stmt in node.code:
|
87 | 197 | self.visit(stmt)
|
88 | 198 |
|
| 199 | + # Check the documented readset and writeset against actual |
| 200 | + # method calls within the function. |
| 201 | + self.check_sets(readset, writeset) |
| 202 | + |
| 203 | + # Remove information held about this function. |
| 204 | + self.current_process = '' |
| 205 | + self.current_process_lineno = 0 |
| 206 | + self.writeset = {} |
| 207 | + self.readset = {} |
| 208 | + return |
| 209 | + |
89 | 210 | def visitCallFunc(self, node):
|
| 211 | + """Visit function call. |
| 212 | +
|
| 213 | + TODO: Deal with Alt and Barrier types. |
| 214 | + """ |
90 | 215 | callee = node.node
|
91 | 216 | if isinstance(callee, ast.Getattr):
|
92 | 217 | if not isinstance(callee.expr, ast.Getattr):
|
93 |
| - print 'Visiting anonymous function call %s' % callee.expr.name |
94 |
| -# print node |
95 |
| -# print dir(node) |
96 |
| - print callee.expr.name + '.' + callee.attrname |
97 |
| - |
98 |
| - # def visitAssign(self, node): |
99 |
| - # print 'VISIT ASSIGN' |
100 |
| - # if isinstance(node.expr, ast.CallFunc): |
101 |
| - # print 'Expr details:', node.expr.node.__dict__ |
102 |
| - # if node.expr.node.name == 'Channel': |
103 |
| - # self.channels.push(cspmodel.Channel(node.nodes[0].name)) |
| 218 | + # Catch all calls to channel read(). |
| 219 | + if callee.attrname == 'read': |
| 220 | + self.readset[callee.lineno] = callee.expr.name |
| 221 | + # Catch all calls to channel write() |
| 222 | + elif callee.attrname == 'write': |
| 223 | + self.writeset[callee.lineno] = callee.expr.name |
| 224 | + return |
104 | 225 |
|
105 | 226 |
|
106 | 227 | if __name__ == '__main__':
|
107 | 228 | import sys
|
108 |
| - |
109 |
| - lint = ChannelChecker() |
| 229 | + |
| 230 | + lint = ChannelChecker(sys.argv[1]) |
110 | 231 | compiler.walk(compiler.parseFile(sys.argv[1]),
|
111 | 232 | lint,
|
112 | 233 | walker=lint,
|
113 | 234 | verbose=5)
|
114 | 235 |
|
| 236 | + exstatic.cspwarnings.print_errors(excluded=[]) |
0 commit comments