Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 1 | import astunparse |
| 2 | import ast |
| 3 | import random |
| 4 | import string |
| 5 | from plyxproto.parser import * |
| 6 | import pdb |
| 7 | |
| 8 | BINOPS = ['|', '&', '=>'] |
| 9 | QUANTS = ['exists', 'forall'] |
| 10 | |
| 11 | |
| 12 | class PolicyException(Exception): |
| 13 | pass |
| 14 | |
| 15 | |
| 16 | class AutoVariable: |
| 17 | def __init__(self, base): |
| 18 | self.base = base |
| 19 | |
| 20 | def __iter__(self): |
| 21 | self.idx = 0 |
| 22 | return self |
| 23 | |
| 24 | def next(self): |
| 25 | var = 'i%d' % self.idx |
| 26 | self.idx += 1 |
| 27 | return var |
| 28 | |
| 29 | |
| 30 | def gen_random_string(): |
| 31 | return ''.join(random.choice(string.ascii_lowercase + string.digits) for _ in range(5)) |
| 32 | |
| 33 | |
| 34 | class FOL2Python: |
| 35 | def __init__(self, context_map=None): |
| 36 | # This will produce i0, i1, i2 etc. |
| 37 | self.loopvar = iter(AutoVariable('i')) |
| 38 | self.verdictvar = iter(AutoVariable('result')) |
| 39 | |
| 40 | self.loop_variable = self.loopvar.next() |
| 41 | self.verdict_variable = self.verdictvar.next() |
| 42 | self.context_map = context_map |
| 43 | |
| 44 | if not self.context_map: |
| 45 | self.context_map = {'user': 'self', 'obj': 'obj'} |
| 46 | |
| 47 | def loop_next(self): |
| 48 | self.loop_variable = self.loopvar.next() |
| 49 | |
| 50 | def verdict_next(self): |
| 51 | self.verdict_variable = self.verdictvar.next() |
| 52 | |
| 53 | def gen_enumerate(self, fol): |
| 54 | pass |
| 55 | |
| 56 | def format_term_for_query(self, model, term, django=False): |
| 57 | if term.startswith(model + '.'): |
| 58 | term = term[len(model) + 1:] |
| 59 | if django: |
| 60 | term = term.replace('.', '__') |
| 61 | else: |
| 62 | term = '__elt' + '.' + term |
| 63 | return term |
| 64 | |
| 65 | def fol_to_python_filter(self, model, e, django=False, negate=False): |
| 66 | try: |
| 67 | (k, v), = e.items() |
| 68 | except AttributeError: |
| 69 | return [self.format_term_for_query(model, e)] |
| 70 | |
| 71 | if django: |
| 72 | if negate: |
| 73 | # De Morgan's negation |
| 74 | q_bracket = '~Q(%s)' |
| 75 | or_expr = ',' |
| 76 | and_expr = '|' |
| 77 | else: |
| 78 | q_bracket = 'Q(%s)' |
| 79 | or_expr = '|' |
| 80 | and_expr = ',' |
| 81 | else: |
| 82 | if negate: |
| 83 | # De Morgan's negation |
| 84 | q_bracket = 'not %s' |
| 85 | or_expr = ' and ' |
| 86 | and_expr = ' or ' |
| 87 | else: |
| 88 | q_bracket = '%s' |
| 89 | or_expr = ' or ' |
| 90 | and_expr = ' and ' |
| 91 | |
| 92 | if k == '=': |
| 93 | v = [self.format_term_for_query( |
| 94 | model, term, django=django) for term in v] |
| 95 | if django: |
| 96 | operator = ' = ' |
| 97 | else: |
| 98 | operator = ' == ' |
| 99 | return [q_bracket % operator.join(v)] |
| 100 | elif k == '|': |
| 101 | components = [self.fol_to_python_filter( |
| 102 | model, x, django=django).pop() for x in v] |
| 103 | return [or_expr.join(components)] |
| 104 | elif k == '&': |
| 105 | components = [self.fol_to_python_filter( |
| 106 | model, x, django=django).pop() for x in v] |
| 107 | return [and_expr.join(components)] |
| 108 | elif k == '=>': |
| 109 | components = [self.fol_to_python_filter( |
| 110 | model, x, django=django).pop() for x in v] |
| 111 | return ['~%s | %s' % (components[0], components[1])] |
| 112 | |
| 113 | """ Convert a single leaf node from a string |
| 114 | to an AST""" |
| 115 | |
| 116 | def str_to_ast(self, s): |
| 117 | ast_module = ast.parse(s) |
| 118 | return ast_module.body[0] |
| 119 | |
| 120 | def hoist_constants(self, fol, var=None): |
| 121 | try: |
| 122 | (k, v), = fol.items() |
| 123 | except AttributeError: |
| 124 | k = 'term' |
| 125 | v = fol |
| 126 | |
| 127 | if k == 'python': |
| 128 | # Tainted, don't optimize |
| 129 | if var: |
| 130 | return {'hoist': []} |
| 131 | else: |
| 132 | return fol |
| 133 | |
| 134 | if var: |
| 135 | if k == 'term': |
| 136 | if not v.startswith(var): |
| 137 | return {'hoist': ['const', fol], 'result': 'True'} |
| 138 | else: |
| 139 | return {'hoist': [], 'result': fol} |
| 140 | elif k == '=': |
| 141 | lhs, rhs = v |
| 142 | if not lhs.startswith(var) and not rhs.startswith(var): |
| 143 | return {'hoist': ['=', fol], 'result': 'True'} # XXX |
| 144 | else: |
| 145 | return {'hoist': [], 'result': fol} |
| 146 | elif k in BINOPS: |
| 147 | lhs, rhs = v |
| 148 | rlhs = self.hoist_constants(lhs, var) |
| 149 | rrhs = self.hoist_constants(rhs, var) |
| 150 | |
| 151 | if rlhs['hoist'] and rrhs['hoist']: |
| 152 | return {'hoist': ['=', fol], 'result': 'True'} |
| 153 | elif rlhs['hoist']: |
| 154 | return {'hoist': [k, lhs], 'result': rhs} |
| 155 | elif rrhs['hoist']: |
| 156 | return {'hoist': [k, rhs], 'result': lhs} |
| 157 | else: |
| 158 | return {'hoist': [], 'result': fol} |
| 159 | |
| 160 | elif k in QUANTS: |
| 161 | var2, expr = v |
| 162 | result = self.hoist_constants(expr, var2) |
| 163 | if result['hoist']: |
| 164 | if result['result'] == 'True': |
| 165 | return {'hoist': ['const'], 'result': result['hoist'][1]} |
| 166 | elif result['hoist'][0] in BINOPS: |
| 167 | return {'hoist': ['const'], 'result': {result['hoist'][0]: [result['hoist'][1], {k: [var2, result['result']]}]}} |
| 168 | else: |
| 169 | return {'hoist': ['const'], 'result': {k: [var2, result['result']]}} |
| 170 | else: |
| 171 | result = self.hoist_constants(expr, var) |
| 172 | if result['result'] == 'True': |
| 173 | return {'hoist': ['&', fol], 'result': 'True'} |
| 174 | else: |
| 175 | return {'hoist': [], 'result': fol} |
| 176 | else: |
| 177 | return {'hoist': [], 'result': fol} |
| 178 | else: |
| 179 | if k in BINOPS: |
| 180 | lhs, rhs = v |
| 181 | rlhs = self.hoist_constants(lhs) |
| 182 | rrhs = self.hoist_constants(rhs) |
| 183 | return {k: [rlhs, rrhs]} |
| 184 | elif k in QUANTS: |
| 185 | var, expr = v |
| 186 | result = self.hoist_constants(expr, var) |
| 187 | if result['hoist']: |
| 188 | if result['result'] == 'True': |
| 189 | return result['hoist'][1] |
| 190 | elif result['hoist'][0] in BINOPS: |
| 191 | return {result['hoist'][0]: [result['hoist'][1], {k: [var, result['result']]}]} |
| 192 | else: |
| 193 | return {k: [var, result['result']]} |
| 194 | else: |
| 195 | return fol |
| 196 | else: |
| 197 | return fol |
| 198 | |
| 199 | def gen_test_function(self, fol, policy_name, tag): |
| 200 | if not tag: |
| 201 | tag = gen_random_string() |
| 202 | |
| 203 | policy_function_name = 'policy_%(policy_name)s_%(random_string)s' % { |
| 204 | 'policy_name': policy_name, 'random_string': tag} |
| 205 | self.verdict_next() |
| 206 | function_str = """ |
| 207 | def %(fn_name)s(obj, ctx): |
| 208 | return %(vvar)s |
| 209 | """ % {'fn_name': policy_function_name, 'vvar': self.verdict_variable} |
| 210 | |
| 211 | function_ast = self.str_to_ast(function_str) |
| 212 | policy_code = self.gen_test(fol, self.verdict_variable) |
| 213 | |
| 214 | function_ast.body = [policy_code] + function_ast.body |
| 215 | |
| 216 | return astunparse.unparse(function_ast) |
| 217 | |
| 218 | def gen_test(self, fol, verdict_var, bindings=None): |
| 219 | if isinstance(fol, str): |
| 220 | return self.str_to_ast('%(verdict_var)s = %(constant)s' % {'verdict_var': verdict_var, 'constant': fol}) |
| 221 | |
| 222 | (k, v), = fol.items() |
| 223 | |
| 224 | if k == '=': |
| 225 | # This is the simplest case, we don't recurse further |
| 226 | # To use terms that are not simple variables, use |
| 227 | # the Python escape, e.g. {{ slice.creator is not None }} |
| 228 | lhs, rhs = v |
| 229 | |
| 230 | assignments = [] |
| 231 | |
| 232 | try: |
| 233 | for t in lhs, rhs: |
| 234 | py_expr = t['python'] |
| 235 | |
| 236 | self.verdict_next() |
| 237 | vv = self.verdict_variable |
| 238 | |
| 239 | try: |
| 240 | expr_ast = self.str_to_ast(py_expr) |
| 241 | except SyntaxError: |
| 242 | raise PolicyException('Syntax error in %s' % v) |
| 243 | |
| 244 | if not isinstance(expr_ast, ast.Expr): |
| 245 | raise PolicyException( |
| 246 | '%s is not an expression' % expr_ast) |
| 247 | |
| 248 | assignment_str = """ |
| 249 | %(verdict_var)s = (%(escape_expr)s) |
| 250 | """ % {'verdict_var': vv, 'escape_expr': py_expr} |
| 251 | |
| 252 | if t == lhs: |
| 253 | lhs = vv |
| 254 | else: |
| 255 | rhs = vv |
| 256 | |
| 257 | assignment_ast = self.str_to_ast(assignment_str) |
| 258 | assignments.append(assignment_ast) |
| 259 | except TypeError: |
| 260 | pass |
| 261 | |
| 262 | comparison_str = """ |
| 263 | %(verdict_var)s = (%(lhs)s == %(rhs)s) |
| 264 | """ % {'verdict_var': verdict_var, 'lhs': lhs, 'rhs': rhs} |
| 265 | |
| 266 | comparison_ast = self.str_to_ast(comparison_str) |
| 267 | |
| 268 | combined_ast = ast.Module(body=assignments + [comparison_ast]) |
| 269 | return combined_ast |
| 270 | elif k in BINOPS: |
| 271 | lhs, rhs = v |
| 272 | |
| 273 | top_vvar = self.verdict_variable |
| 274 | |
| 275 | self.verdict_next() |
| 276 | lvar = self.verdict_variable |
| 277 | |
| 278 | self.verdict_next() |
| 279 | rvar = self.verdict_variable |
| 280 | |
| 281 | lblock = self.gen_test(lhs, lvar) |
| 282 | rblock = self.gen_test(rhs, rvar) |
| 283 | |
| 284 | invert = '' |
| 285 | if k == '&': |
| 286 | binop = 'and' |
| 287 | elif k == '|': |
| 288 | binop = 'or' |
| 289 | elif k == '=>': |
| 290 | binop = 'or' |
| 291 | invert = 'not' |
| 292 | |
| 293 | binop_str = """ |
| 294 | %(verdict_var)s = %(invert)s %(lvar)s %(binop)s %(rvar)s |
| 295 | """ % {'verdict_var': top_vvar, 'invert': invert, 'lvar': lvar, 'binop': binop, 'rvar': rvar} |
| 296 | |
| 297 | binop_ast = self.str_to_ast(binop_str) |
| 298 | |
| 299 | combined_ast = ast.Module(body=[lblock, rblock, binop_ast]) |
| 300 | return combined_ast |
| 301 | elif k == 'exists': |
| 302 | # If the variable starts with a capital letter, |
| 303 | # we assume that it is a model. If it starts with |
| 304 | # a small letter, we assume it is an enumerable |
| 305 | # |
| 306 | # We do not support nested exists yet. FIXME. |
| 307 | |
| 308 | var, expr = v |
| 309 | |
| 310 | if var.istitle(): |
| 311 | f = self.fol_to_python_filter(var, expr, django=True) |
| 312 | entry = f.pop() |
| 313 | |
| 314 | python_str = """ |
| 315 | %(verdict_var)s = %(model)s.objects.filter(%(query)s)[0] |
| 316 | """ % {'verdict_var': verdict_var, 'model': var, 'query': entry} |
| 317 | |
| 318 | python_ast = ast.parse(python_str) |
| 319 | else: |
| 320 | f = self.fol_to_python_filter(var, expr, django=False) |
| 321 | entry = f.pop() |
| 322 | |
| 323 | python_str = """ |
| 324 | %(verdict_var)s = filter(lambda __elt:%(query)s, %(model)s) |
| 325 | """ % {'verdict_var': verdict_var, 'model': var, 'query': entry} |
| 326 | |
| 327 | python_ast = ast.parse(python_str) |
| 328 | |
| 329 | return python_ast |
| 330 | elif k=='forall': |
| 331 | var, expr = v |
| 332 | |
| 333 | if var.istitle(): |
| 334 | f = self.fol_to_python_filter(var, expr, django=True, negate = True) |
| 335 | entry = f.pop() |
| 336 | |
| 337 | self.verdict_next() |
| 338 | vvar = self.verdict_variable |
| 339 | |
| 340 | python_str = """ |
| 341 | %(verdict_var)s = %(model)s.objects.filter(%(query)s)[0] |
| 342 | """ % {'verdict_var': vvar, 'model': var, 'query': entry} |
| 343 | |
| 344 | python_ast = ast.parse(python_str) |
| 345 | else: |
| 346 | f = self.fol_to_python_filter(var, expr, django=False, negate = True) |
| 347 | entry = f.pop() |
| 348 | |
| 349 | python_str = """ |
| 350 | %(verdict_var)s = next(elt for elt in %(model)s if %(query)s) |
| 351 | """ % {'verdict_var': vvar, 'model': var, 'query': entry} |
| 352 | |
| 353 | python_ast = ast.parse(python_str) |
| 354 | |
| 355 | negate_str = """ |
| 356 | %(verdict_var)s = not %(vvar)s |
| 357 | """ % {'verdict_var': verdict_var, 'vvar': vvar} |
| 358 | |
| 359 | negate_ast = ast.parse(negate_str) |
| 360 | |
| 361 | return ast.Module(body=[python_ast, negate_ast]) |
| 362 | |
| 363 | def xproto_fol_to_python_test(fol, model, tag=None): |
| 364 | f2p = FOL2Python() |
| 365 | fol = f2p.hoist_constants(fol) |
| 366 | a = f2p.gen_test_function(fol, 'output', tag) |
| 367 | return a |
| 368 | |
| 369 | |
| 370 | def main(): |
| 371 | while True: |
| 372 | inp = raw_input() |
| 373 | fol_lexer = lex.lex(module=FOLLexer()) |
| 374 | fol_parser = yacc.yacc(module=FOLParser(), start='goal') |
| 375 | |
| 376 | val = fol_parser.parse(inp, lexer=fol_lexer) |
| 377 | a = xproto_fol_to_python_test(val, 'output') |
| 378 | print a |
| 379 | |
| 380 | |
| 381 | if __name__ == "__main__": |
| 382 | main() |