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 * |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 7 | |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 8 | BINOPS = ['|', '&', '->'] |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 9 | QUANTS = ['exists', 'forall'] |
| 10 | |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 11 | class PolicyException(Exception): |
| 12 | pass |
| 13 | |
Sapan Bhatia | b69f470 | 2017-07-31 16:03:33 -0400 | [diff] [blame] | 14 | class ConstructNotHandled(Exception): |
| 15 | pass |
| 16 | |
| 17 | class TrivialPolicy(Exception): |
| 18 | pass |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 19 | |
| 20 | class AutoVariable: |
| 21 | def __init__(self, base): |
| 22 | self.base = base |
| 23 | |
| 24 | def __iter__(self): |
| 25 | self.idx = 0 |
| 26 | return self |
| 27 | |
| 28 | def next(self): |
| 29 | var = 'i%d' % self.idx |
| 30 | self.idx += 1 |
| 31 | return var |
| 32 | |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 33 | def gen_random_string(): |
| 34 | return ''.join(random.choice(string.ascii_lowercase + string.digits) for _ in range(5)) |
| 35 | |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 36 | class FOL2Python: |
| 37 | def __init__(self, context_map=None): |
| 38 | # This will produce i0, i1, i2 etc. |
| 39 | self.loopvar = iter(AutoVariable('i')) |
| 40 | self.verdictvar = iter(AutoVariable('result')) |
| 41 | |
| 42 | self.loop_variable = self.loopvar.next() |
| 43 | self.verdict_variable = self.verdictvar.next() |
| 44 | self.context_map = context_map |
| 45 | |
| 46 | if not self.context_map: |
| 47 | self.context_map = {'user': 'self', 'obj': 'obj'} |
| 48 | |
| 49 | def loop_next(self): |
| 50 | self.loop_variable = self.loopvar.next() |
| 51 | |
| 52 | def verdict_next(self): |
| 53 | self.verdict_variable = self.verdictvar.next() |
| 54 | |
| 55 | def gen_enumerate(self, fol): |
| 56 | pass |
| 57 | |
| 58 | def format_term_for_query(self, model, term, django=False): |
| 59 | if term.startswith(model + '.'): |
| 60 | term = term[len(model) + 1:] |
| 61 | if django: |
| 62 | term = term.replace('.', '__') |
| 63 | else: |
| 64 | term = '__elt' + '.' + term |
| 65 | return term |
| 66 | |
| 67 | def fol_to_python_filter(self, model, e, django=False, negate=False): |
| 68 | try: |
| 69 | (k, v), = e.items() |
| 70 | except AttributeError: |
| 71 | return [self.format_term_for_query(model, e)] |
| 72 | |
| 73 | if django: |
| 74 | if negate: |
| 75 | # De Morgan's negation |
| 76 | q_bracket = '~Q(%s)' |
| 77 | or_expr = ',' |
| 78 | and_expr = '|' |
| 79 | else: |
| 80 | q_bracket = 'Q(%s)' |
| 81 | or_expr = '|' |
| 82 | and_expr = ',' |
| 83 | else: |
| 84 | if negate: |
| 85 | # De Morgan's negation |
| 86 | q_bracket = 'not %s' |
| 87 | or_expr = ' and ' |
| 88 | and_expr = ' or ' |
| 89 | else: |
| 90 | q_bracket = '%s' |
| 91 | or_expr = ' or ' |
| 92 | and_expr = ' and ' |
| 93 | |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 94 | if k in ['=','in']: |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 95 | v = [self.format_term_for_query( |
| 96 | model, term, django=django) for term in v] |
| 97 | if django: |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 98 | operator_map = {'=':' = ','in':'__in'} |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 99 | else: |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 100 | operator_map = {'=':' == ','in':'in'} |
| 101 | operator = operator_map[k] |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 102 | return [q_bracket % operator.join(v)] |
| 103 | elif k == '|': |
| 104 | components = [self.fol_to_python_filter( |
| 105 | model, x, django=django).pop() for x in v] |
| 106 | return [or_expr.join(components)] |
| 107 | elif k == '&': |
| 108 | components = [self.fol_to_python_filter( |
| 109 | model, x, django=django).pop() for x in v] |
| 110 | return [and_expr.join(components)] |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 111 | elif k == '->': |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 112 | components = [self.fol_to_python_filter( |
| 113 | model, x, django=django).pop() for x in v] |
| 114 | return ['~%s | %s' % (components[0], components[1])] |
| 115 | |
| 116 | """ Convert a single leaf node from a string |
| 117 | to an AST""" |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 118 | def str_to_ast(self, s): |
| 119 | ast_module = ast.parse(s) |
| 120 | return ast_module.body[0] |
| 121 | |
Sapan Bhatia | b69f470 | 2017-07-31 16:03:33 -0400 | [diff] [blame] | 122 | def reduce_operands(self, operands): |
| 123 | if operands[0] in ['True','False']: |
| 124 | return (operands[0],operands[1]) |
| 125 | elif operands[1] in ['True','False']: |
| 126 | return (operands[1],operands[0]) |
| 127 | else: |
| 128 | return None |
| 129 | |
| 130 | """ Simplify binops with constants """ |
| 131 | def simplify_binop(self, binop): |
| 132 | (k,v), = binop.items() |
| 133 | if k == '->': |
| 134 | lhs, rhs = v |
| 135 | if lhs == 'True': |
| 136 | return rhs |
| 137 | elif rhs == 'True': |
| 138 | return 'True' |
| 139 | elif lhs == 'False': |
| 140 | return 'True' |
| 141 | elif rhs == 'False': |
| 142 | return {'not': lhs} |
| 143 | |
| 144 | var_expr = self.reduce_operands(v) |
| 145 | |
| 146 | if not var_expr: return binop |
| 147 | else: |
| 148 | constant, var = var_expr |
| 149 | if k=='|': |
| 150 | if constant=='True': |
| 151 | return 'True' |
| 152 | elif constant=='False': |
| 153 | return var |
| 154 | else: |
| 155 | raise Exception("Internal error - variable read as constant") |
| 156 | elif k=='&': |
| 157 | if constant=='True': |
| 158 | return var |
| 159 | elif constant=='False': |
| 160 | return 'False' |
| 161 | |
| 162 | def is_constant(self, var, fol): |
| 163 | try: |
| 164 | (k, v), = fol.items() |
| 165 | except AttributeError: |
| 166 | k = 'term' |
| 167 | v = fol |
| 168 | |
| 169 | if k in ['python', 'policy']: |
| 170 | # Treat as a constant and hoist, since it cannot be quantified |
| 171 | return True |
| 172 | elif k == 'term': |
| 173 | return not v.startswith(var) |
| 174 | elif k == 'not': |
| 175 | return self.is_constant(var, fol) |
| 176 | elif k in ['in', '=']: |
| 177 | lhs, rhs = v |
| 178 | return self.is_constant(var,lhs) and self.is_constant(var, rhs) |
| 179 | elif k in BINOPS: |
| 180 | lhs, rhs = v |
| 181 | return self.is_constant(lhs, var) and self.is_constant(rhs, var) |
| 182 | elif k in QUANTS: |
| 183 | is_constant = self.is_constant(var, fol[1]) |
| 184 | return is_constant |
| 185 | else: |
| 186 | raise ConstructNotHandled(k) |
| 187 | |
| 188 | def find_constants(self, var, fol, constants): |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 189 | try: |
| 190 | (k, v), = fol.items() |
| 191 | except AttributeError: |
| 192 | k = 'term' |
| 193 | v = fol |
| 194 | |
Sapan Bhatia | b69f470 | 2017-07-31 16:03:33 -0400 | [diff] [blame] | 195 | if k in ['python', 'policy']: |
| 196 | # Treat as a constant and hoist, since it cannot be quantified |
| 197 | if fol not in constants: |
| 198 | constants.append(fol) |
| 199 | return constants |
| 200 | elif k == 'term': |
| 201 | if not v.startswith(var): |
| 202 | constants.append(v) |
| 203 | return constants |
| 204 | elif k == 'not': |
| 205 | return self.find_constants(var, v, constants) |
| 206 | elif k in ['in', '=']: |
| 207 | lhs, rhs = v |
| 208 | if isinstance(lhs, str) and isinstance(rhs, str): |
| 209 | if not lhs.startswith(var) and not rhs.startswith(var): |
| 210 | constants.append(fol) |
| 211 | return constants |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 212 | else: |
Sapan Bhatia | b69f470 | 2017-07-31 16:03:33 -0400 | [diff] [blame] | 213 | constants = self.find_constants(var, lhs, constants) |
| 214 | return self.find_constants(var, rhs, constants) |
| 215 | elif k in BINOPS: |
| 216 | lhs, rhs = v |
| 217 | constants = self.find_constants(var, lhs, constants) |
| 218 | constants = self.find_constants(var, rhs, constants) |
| 219 | return constants |
| 220 | elif k in QUANTS: |
| 221 | is_constant = self.is_constant(var, v[1]) |
| 222 | if is_constant: constants.append(fol) |
| 223 | return constants |
| 224 | else: |
| 225 | raise ConstructNotHandled(k) |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 226 | |
Sapan Bhatia | b69f470 | 2017-07-31 16:03:33 -0400 | [diff] [blame] | 227 | """ Hoist constants out of quantifiers. Depth-first. """ |
| 228 | def hoist_outer(self, fol): |
| 229 | try: |
| 230 | (k, v), = fol.items() |
| 231 | except AttributeError: |
| 232 | k = 'term' |
| 233 | v = fol |
| 234 | |
| 235 | if k in ['python', 'policy']: |
| 236 | # Tainted, optimization and distribution not possible |
| 237 | return fol |
| 238 | elif k == 'term': |
| 239 | return fol |
| 240 | elif k == 'not': |
| 241 | vprime = self.hoist_outer(v) |
| 242 | return {'not': vprime} |
| 243 | elif k in ['in', '=']: |
| 244 | lhs, rhs = v |
| 245 | rlhs = self.hoist_outer(lhs) |
| 246 | rrhs = self.hoist_outer(rhs) |
| 247 | return {k:[rlhs,rrhs]} |
| 248 | elif k in BINOPS: |
| 249 | lhs, rhs = v |
| 250 | rlhs = self.hoist_outer(lhs) |
| 251 | rrhs = self.hoist_outer(rhs) |
| 252 | |
| 253 | fol_prime = {k: [rlhs, rrhs]} |
| 254 | fol_simplified = self.simplify_binop(fol_prime) |
| 255 | return fol_simplified |
| 256 | elif k in QUANTS: |
| 257 | rexpr = self.hoist_outer(v[1]) |
| 258 | return self.hoist_quant(k, [v[0],rexpr]) |
| 259 | else: |
| 260 | raise ConstructNotHandled(k) |
| 261 | |
| 262 | def replace_const(self, fol, c, value): |
| 263 | if fol == c: |
| 264 | return value |
| 265 | |
| 266 | try: |
| 267 | (k, v), = fol.items() |
| 268 | except AttributeError: |
| 269 | k = 'term' |
| 270 | v = fol |
| 271 | |
| 272 | if k == 'term': |
| 273 | if v == c: return value |
| 274 | else: return v |
| 275 | elif k == 'not': |
| 276 | new_expr = self.replace_const(v, c, value) |
| 277 | if new_expr=='True': |
| 278 | return 'False' |
| 279 | elif new_expr=='False': |
| 280 | return 'True' |
| 281 | else: |
| 282 | return {'not': new_expr} |
| 283 | elif k in ['in', '=']: |
| 284 | lhs, rhs = v |
| 285 | rlhs = self.replace_const(lhs, c, value) |
| 286 | rrhs = self.replace_const(rhs, c, value) |
| 287 | |
| 288 | if rlhs==rrhs: |
| 289 | return 'True' |
| 290 | else: |
| 291 | return {k: [rlhs, rrhs]} |
| 292 | elif k in BINOPS: |
| 293 | lhs, rhs = v |
| 294 | |
| 295 | rlhs = self.replace_const(lhs, c, value) |
| 296 | rrhs = self.replace_const(rhs, c, value) |
| 297 | |
| 298 | return self.simplify_binop({k:[rlhs,rrhs]}) |
| 299 | elif k in QUANTS: |
| 300 | var, expr = v |
| 301 | new_expr = self.replace_const(expr, c, value) |
| 302 | if new_expr in ['True', 'False']: |
| 303 | return new_expr |
| 304 | else: |
| 305 | return {k: [var, new_expr]} |
| 306 | else: |
| 307 | raise ConstructNotHandled(k) |
| 308 | |
| 309 | def shannon_expand(self, c, fol): |
| 310 | lhs = self.replace_const(fol, c, 'True') |
| 311 | rhs = self.replace_const(fol, c, 'False') |
| 312 | not_c = {'not': c} |
| 313 | rlhs = {'&': [c, lhs]} |
| 314 | rlhs = self.simplify_binop(rlhs) |
| 315 | |
| 316 | rrhs = {'&': [not_c, rhs]} |
| 317 | rrhs = self.simplify_binop(rrhs) |
| 318 | |
| 319 | combined = {'|': [rlhs, rrhs]} |
| 320 | return self.simplify_binop(combined) |
| 321 | |
| 322 | def hoist_quant(self, k, expr): |
| 323 | var, v = expr |
| 324 | |
| 325 | constants = self.find_constants(var, v, constants=[]) |
| 326 | |
| 327 | fol = {k: expr} |
| 328 | |
| 329 | for c in constants: |
| 330 | fol = self.shannon_expand(c, fol) |
| 331 | |
| 332 | return fol |
| 333 | |
| 334 | """ |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 335 | if var: |
| 336 | if k == 'term': |
| 337 | if not v.startswith(var): |
| 338 | return {'hoist': ['const', fol], 'result': 'True'} |
| 339 | else: |
| 340 | return {'hoist': [], 'result': fol} |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 341 | elif k in ['=', 'in']: |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 342 | lhs, rhs = v |
| 343 | if not lhs.startswith(var) and not rhs.startswith(var): |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 344 | return {'hoist': [k, fol], 'result': 'True'} # XXX |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 345 | else: |
| 346 | return {'hoist': [], 'result': fol} |
| 347 | elif k in BINOPS: |
| 348 | lhs, rhs = v |
| 349 | rlhs = self.hoist_constants(lhs, var) |
| 350 | rrhs = self.hoist_constants(rhs, var) |
| 351 | |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 352 | 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] | 353 | return {'hoist': ['=', fol], 'result': 'True'} |
| 354 | elif rlhs['hoist']: |
| 355 | return {'hoist': [k, lhs], 'result': rhs} |
| 356 | elif rrhs['hoist']: |
| 357 | return {'hoist': [k, rhs], 'result': lhs} |
| 358 | else: |
| 359 | return {'hoist': [], 'result': fol} |
| 360 | |
| 361 | elif k in QUANTS: |
| 362 | var2, expr = v |
| 363 | result = self.hoist_constants(expr, var2) |
| 364 | if result['hoist']: |
| 365 | if result['result'] == 'True': |
| 366 | return {'hoist': ['const'], 'result': result['hoist'][1]} |
| 367 | elif result['hoist'][0] in BINOPS: |
| 368 | return {'hoist': ['const'], 'result': {result['hoist'][0]: [result['hoist'][1], {k: [var2, result['result']]}]}} |
| 369 | else: |
| 370 | return {'hoist': ['const'], 'result': {k: [var2, result['result']]}} |
| 371 | else: |
| 372 | result = self.hoist_constants(expr, var) |
| 373 | if result['result'] == 'True': |
| 374 | return {'hoist': ['&', fol], 'result': 'True'} |
| 375 | else: |
| 376 | return {'hoist': [], 'result': fol} |
| 377 | else: |
| 378 | return {'hoist': [], 'result': fol} |
| 379 | else: |
| 380 | if k in BINOPS: |
| 381 | lhs, rhs = v |
| 382 | rlhs = self.hoist_constants(lhs) |
| 383 | rrhs = self.hoist_constants(rhs) |
| 384 | return {k: [rlhs, rrhs]} |
| 385 | elif k in QUANTS: |
| 386 | var, expr = v |
| 387 | result = self.hoist_constants(expr, var) |
| 388 | if result['hoist']: |
| 389 | if result['result'] == 'True': |
| 390 | return result['hoist'][1] |
| 391 | elif result['hoist'][0] in BINOPS: |
| 392 | return {result['hoist'][0]: [result['hoist'][1], {k: [var, result['result']]}]} |
| 393 | else: |
| 394 | return {k: [var, result['result']]} |
| 395 | else: |
| 396 | return fol |
| 397 | else: |
| 398 | return fol |
Sapan Bhatia | b69f470 | 2017-07-31 16:03:33 -0400 | [diff] [blame] | 399 | """ |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 400 | |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 401 | def gen_validation_function(self, fol, policy_name, message, tag): |
| 402 | if not tag: |
| 403 | tag = gen_random_string() |
| 404 | |
Sapan Bhatia | d3fcb66 | 2017-07-25 21:13:48 -0400 | [diff] [blame] | 405 | policy_function_name_template = 'policy_%s_' + '%(random_string)s' % {'random_string': tag} |
| 406 | policy_function_name = policy_function_name_template % policy_name |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 407 | self.verdict_next() |
| 408 | function_str = """ |
| 409 | def %(fn_name)s(obj, ctx): |
Sapan Bhatia | 9227b4d | 2017-07-25 23:14:48 -0400 | [diff] [blame] | 410 | if not %(vvar)s: raise ValidationError("%(message)s".format(obj=obj, ctx=ctx)) |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 411 | """ % {'fn_name': policy_function_name, 'vvar': self.verdict_variable, 'message': message} |
| 412 | |
| 413 | function_ast = self.str_to_ast(function_str) |
Sapan Bhatia | d3fcb66 | 2017-07-25 21:13:48 -0400 | [diff] [blame] | 414 | policy_code = self.gen_test(policy_function_name_template, fol, self.verdict_variable) |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 415 | |
| 416 | |
| 417 | function_ast.body = [policy_code] + function_ast.body |
| 418 | |
| 419 | return function_ast |
| 420 | |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 421 | def gen_test_function(self, fol, policy_name, tag): |
| 422 | if not tag: |
| 423 | tag = gen_random_string() |
| 424 | |
Sapan Bhatia | d3fcb66 | 2017-07-25 21:13:48 -0400 | [diff] [blame] | 425 | policy_function_name_template = 'policy_%s_' + '%(random_string)s' % {'random_string': tag} |
| 426 | policy_function_name = policy_function_name_template % policy_name |
| 427 | |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 428 | self.verdict_next() |
| 429 | function_str = """ |
| 430 | def %(fn_name)s(obj, ctx): |
| 431 | return %(vvar)s |
| 432 | """ % {'fn_name': policy_function_name, 'vvar': self.verdict_variable} |
| 433 | |
| 434 | function_ast = self.str_to_ast(function_str) |
Sapan Bhatia | d3fcb66 | 2017-07-25 21:13:48 -0400 | [diff] [blame] | 435 | policy_code = self.gen_test(policy_function_name_template, fol, self.verdict_variable) |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 436 | |
| 437 | function_ast.body = [policy_code] + function_ast.body |
| 438 | |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 439 | return function_ast |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 440 | |
Sapan Bhatia | d3fcb66 | 2017-07-25 21:13:48 -0400 | [diff] [blame] | 441 | def gen_test(self, fn_template, fol, verdict_var, bindings=None): |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 442 | if isinstance(fol, str): |
| 443 | return self.str_to_ast('%(verdict_var)s = %(constant)s' % {'verdict_var': verdict_var, 'constant': fol}) |
| 444 | |
| 445 | (k, v), = fol.items() |
| 446 | |
Sapan Bhatia | d3fcb66 | 2017-07-25 21:13:48 -0400 | [diff] [blame] | 447 | if k == 'policy': |
| 448 | policy_name, object_name = v |
| 449 | |
| 450 | policy_fn = fn_template % policy_name |
| 451 | call_str = """ |
| 452 | %(verdict_var)s = %(policy_fn)s(obj.%(object_name)s, ctx) |
Sapan Bhatia | b69f470 | 2017-07-31 16:03:33 -0400 | [diff] [blame] | 453 | """ % {'verdict_var': verdict_var, 'policy_fn': policy_fn, 'object_name': object_name} |
Sapan Bhatia | d3fcb66 | 2017-07-25 21:13:48 -0400 | [diff] [blame] | 454 | |
| 455 | call_ast = self.str_to_ast(call_str) |
| 456 | return call_ast |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 457 | if k == 'python': |
| 458 | try: |
| 459 | expr_ast = self.str_to_ast(v) |
| 460 | except SyntaxError: |
| 461 | raise PolicyException('Syntax error in %s' % v) |
| 462 | |
| 463 | if not isinstance(expr_ast, ast.Expr): |
| 464 | raise PolicyException( |
| 465 | '%s is not an expression' % expr_ast) |
| 466 | |
| 467 | assignment_str = """ |
| 468 | %(verdict_var)s = (%(escape_expr)s) |
Sapan Bhatia | b69f470 | 2017-07-31 16:03:33 -0400 | [diff] [blame] | 469 | """ % {'verdict_var': verdict_var, 'escape_expr': v} |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 470 | |
| 471 | assignment_ast = self.str_to_ast(assignment_str) |
| 472 | return assignment_ast |
| 473 | elif k == 'not': |
Sapan Bhatia | b69f470 | 2017-07-31 16:03:33 -0400 | [diff] [blame] | 474 | top_vvar = verdict_var |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 475 | self.verdict_next() |
| 476 | sub_vvar = self.verdict_variable |
Sapan Bhatia | d3fcb66 | 2017-07-25 21:13:48 -0400 | [diff] [blame] | 477 | block = self.gen_test(fn_template, v, sub_vvar) |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 478 | assignment_str = """ |
| 479 | %(verdict_var)s = not (%(subvar)s) |
| 480 | """ % {'verdict_var': top_vvar, 'subvar': sub_vvar} |
| 481 | |
| 482 | assignment_ast = self.str_to_ast(assignment_str) |
| 483 | |
| 484 | return ast.Module(body=[block, assignment_ast]) |
| 485 | elif k in ['=','in']: |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 486 | # This is the simplest case, we don't recurse further |
| 487 | # To use terms that are not simple variables, use |
| 488 | # the Python escape, e.g. {{ slice.creator is not None }} |
| 489 | lhs, rhs = v |
| 490 | |
| 491 | assignments = [] |
| 492 | |
| 493 | try: |
| 494 | for t in lhs, rhs: |
| 495 | py_expr = t['python'] |
| 496 | |
| 497 | self.verdict_next() |
| 498 | vv = self.verdict_variable |
| 499 | |
| 500 | try: |
| 501 | expr_ast = self.str_to_ast(py_expr) |
| 502 | except SyntaxError: |
| 503 | raise PolicyException('Syntax error in %s' % v) |
| 504 | |
| 505 | if not isinstance(expr_ast, ast.Expr): |
| 506 | raise PolicyException( |
| 507 | '%s is not an expression' % expr_ast) |
| 508 | |
| 509 | assignment_str = """ |
| 510 | %(verdict_var)s = (%(escape_expr)s) |
| 511 | """ % {'verdict_var': vv, 'escape_expr': py_expr} |
| 512 | |
| 513 | if t == lhs: |
| 514 | lhs = vv |
| 515 | else: |
| 516 | rhs = vv |
| 517 | |
| 518 | assignment_ast = self.str_to_ast(assignment_str) |
| 519 | assignments.append(assignment_ast) |
| 520 | except TypeError: |
| 521 | pass |
| 522 | |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 523 | if k=='=': |
| 524 | operator='==' |
| 525 | elif k=='in': |
| 526 | operator='in' |
| 527 | |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 528 | comparison_str = """ |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 529 | %(verdict_var)s = (%(lhs)s %(operator)s %(rhs)s) |
| 530 | """ % {'verdict_var': verdict_var, 'lhs': lhs, 'rhs': rhs, 'operator':operator} |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 531 | |
| 532 | comparison_ast = self.str_to_ast(comparison_str) |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 533 | combined_ast = ast.Module(body=assignments + [comparison_ast]) |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 534 | |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 535 | return combined_ast |
| 536 | elif k in BINOPS: |
| 537 | lhs, rhs = v |
| 538 | |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 539 | top_vvar = verdict_var |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 540 | |
| 541 | self.verdict_next() |
| 542 | lvar = self.verdict_variable |
| 543 | |
| 544 | self.verdict_next() |
| 545 | rvar = self.verdict_variable |
| 546 | |
Sapan Bhatia | d3fcb66 | 2017-07-25 21:13:48 -0400 | [diff] [blame] | 547 | lblock = self.gen_test(fn_template, lhs, lvar) |
| 548 | rblock = self.gen_test(fn_template, rhs, rvar) |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 549 | |
| 550 | invert = '' |
| 551 | if k == '&': |
| 552 | binop = 'and' |
| 553 | elif k == '|': |
| 554 | binop = 'or' |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 555 | elif k == '->': |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 556 | binop = 'or' |
| 557 | invert = 'not' |
| 558 | |
| 559 | binop_str = """ |
| 560 | %(verdict_var)s = %(invert)s %(lvar)s %(binop)s %(rvar)s |
| 561 | """ % {'verdict_var': top_vvar, 'invert': invert, 'lvar': lvar, 'binop': binop, 'rvar': rvar} |
| 562 | |
| 563 | binop_ast = self.str_to_ast(binop_str) |
| 564 | |
| 565 | combined_ast = ast.Module(body=[lblock, rblock, binop_ast]) |
| 566 | return combined_ast |
| 567 | elif k == 'exists': |
| 568 | # If the variable starts with a capital letter, |
| 569 | # we assume that it is a model. If it starts with |
| 570 | # a small letter, we assume it is an enumerable |
| 571 | # |
| 572 | # We do not support nested exists yet. FIXME. |
| 573 | |
| 574 | var, expr = v |
| 575 | |
| 576 | if var.istitle(): |
| 577 | f = self.fol_to_python_filter(var, expr, django=True) |
| 578 | entry = f.pop() |
| 579 | |
| 580 | python_str = """ |
Sapan Bhatia | 9227b4d | 2017-07-25 23:14:48 -0400 | [diff] [blame] | 581 | %(verdict_var)s = not not %(model)s.objects.filter(%(query)s) |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 582 | """ % {'verdict_var': verdict_var, 'model': var, 'query': entry} |
| 583 | |
| 584 | python_ast = ast.parse(python_str) |
| 585 | else: |
| 586 | f = self.fol_to_python_filter(var, expr, django=False) |
| 587 | entry = f.pop() |
| 588 | |
| 589 | python_str = """ |
| 590 | %(verdict_var)s = filter(lambda __elt:%(query)s, %(model)s) |
| 591 | """ % {'verdict_var': verdict_var, 'model': var, 'query': entry} |
| 592 | |
| 593 | python_ast = ast.parse(python_str) |
| 594 | |
| 595 | return python_ast |
| 596 | elif k=='forall': |
| 597 | var, expr = v |
| 598 | |
| 599 | if var.istitle(): |
| 600 | f = self.fol_to_python_filter(var, expr, django=True, negate = True) |
| 601 | entry = f.pop() |
| 602 | |
| 603 | self.verdict_next() |
| 604 | vvar = self.verdict_variable |
| 605 | |
| 606 | python_str = """ |
Sapan Bhatia | 9227b4d | 2017-07-25 23:14:48 -0400 | [diff] [blame] | 607 | %(verdict_var)s = not not %(model)s.objects.filter(%(query)s) |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 608 | """ % {'verdict_var': vvar, 'model': var, 'query': entry} |
| 609 | |
| 610 | python_ast = ast.parse(python_str) |
| 611 | else: |
| 612 | f = self.fol_to_python_filter(var, expr, django=False, negate = True) |
| 613 | entry = f.pop() |
| 614 | |
| 615 | python_str = """ |
| 616 | %(verdict_var)s = next(elt for elt in %(model)s if %(query)s) |
| 617 | """ % {'verdict_var': vvar, 'model': var, 'query': entry} |
| 618 | |
| 619 | python_ast = ast.parse(python_str) |
| 620 | |
| 621 | negate_str = """ |
| 622 | %(verdict_var)s = not %(vvar)s |
| 623 | """ % {'verdict_var': verdict_var, 'vvar': vvar} |
| 624 | |
| 625 | negate_ast = ast.parse(negate_str) |
| 626 | |
| 627 | return ast.Module(body=[python_ast, negate_ast]) |
| 628 | |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 629 | def xproto_fol_to_python_test(policy, fol, model, tag=None): |
| 630 | if isinstance(fol, jinja2.Undefined): |
| 631 | raise Exception('Could not find policy:', policy) |
| 632 | |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 633 | f2p = FOL2Python() |
Sapan Bhatia | b69f470 | 2017-07-31 16:03:33 -0400 | [diff] [blame] | 634 | fol_reduced = f2p.hoist_outer(fol) |
| 635 | |
| 636 | if fol_reduced in ['True','False'] and fol != fol_reduced: |
| 637 | raise TrivialPolicy("Policy %(name)s trivially reduces to %(reduced)s. If this is what you want, replace its contents with %(reduced)s"%{'name':policy, 'reduced':fol_reduced}) |
| 638 | |
| 639 | a = f2p.gen_test_function(fol_reduced, policy, tag='enforcer') |
| 640 | |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 641 | return astunparse.unparse(a) |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 642 | |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 643 | def xproto_fol_to_python_validator(policy, fol, model, message, tag=None): |
| 644 | if isinstance(fol, jinja2.Undefined): |
| 645 | raise Exception('Could not find policy:', policy) |
| 646 | |
| 647 | f2p = FOL2Python() |
Sapan Bhatia | b69f470 | 2017-07-31 16:03:33 -0400 | [diff] [blame] | 648 | fol_reduced = f2p.hoist_outer(fol) |
| 649 | |
| 650 | if fol_reduced in ['True','False'] and fol != fol_reduced: |
| 651 | raise TrivialPolicy("Policy %(name)s trivially reduces to %(reduced)s. If this is what you want, replace its contents with %(reduced)s"%{'name':policy, 'reduced':fol_reduced}) |
| 652 | |
| 653 | a = f2p.gen_validation_function(fol_reduced, policy, message, tag='validator') |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 654 | |
| 655 | return astunparse.unparse(a) |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 656 | |
| 657 | def main(): |
| 658 | while True: |
Sapan Bhatia | b69f470 | 2017-07-31 16:03:33 -0400 | [diff] [blame] | 659 | inp = '' |
| 660 | while True: |
| 661 | inp_line = raw_input() |
| 662 | if inp_line=='EOF': break |
| 663 | else: inp+=inp_line |
| 664 | |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 665 | fol_lexer = lex.lex(module=FOLLexer()) |
| 666 | fol_parser = yacc.yacc(module=FOLParser(), start='goal') |
| 667 | |
| 668 | val = fol_parser.parse(inp, lexer=fol_lexer) |
Sapan Bhatia | 5ea307d | 2017-07-19 00:13:21 -0400 | [diff] [blame] | 669 | a = xproto_fol_to_python_test('pol', val, 'output', 'Test') |
Sapan Bhatia | b69f470 | 2017-07-31 16:03:33 -0400 | [diff] [blame] | 670 | #f2p = FOL2Python() |
| 671 | #a = f2p.hoist_outer(val) |
Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 672 | print a |
| 673 | |
| 674 | |
| 675 | if __name__ == "__main__": |
| 676 | main() |