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