blob: 3042e376f9a2ee939a5b4f99e05bb37fe7db3d7f [file] [log] [blame]
Matteo Scandolod2044a42017-08-07 16:08:28 -07001
2# Copyright 2017-present Open Networking Foundation
3#
4# Licensed under the Apache License, Version 2.0 (the "License");
5# you may not use this file except in compliance with the License.
6# You may obtain a copy of the License at
7#
8# http://www.apache.org/licenses/LICENSE-2.0
9#
10# Unless required by applicable law or agreed to in writing, software
11# distributed under the License is distributed on an "AS IS" BASIS,
12# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13# See the License for the specific language governing permissions and
14# limitations under the License.
15
16
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -040017import astunparse
18import ast
19import random
20import string
Sapan Bhatia5ea307d2017-07-19 00:13:21 -040021import jinja2
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -040022from plyxproto.parser import *
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -040023
Sapan Bhatia5ea307d2017-07-19 00:13:21 -040024BINOPS = ['|', '&', '->']
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -040025QUANTS = ['exists', 'forall']
26
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -040027class PolicyException(Exception):
28 pass
29
Sapan Bhatiab69f4702017-07-31 16:03:33 -040030class ConstructNotHandled(Exception):
31 pass
32
33class TrivialPolicy(Exception):
34 pass
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -040035
36class AutoVariable:
37 def __init__(self, base):
38 self.base = base
39
40 def __iter__(self):
41 self.idx = 0
42 return self
43
44 def next(self):
45 var = 'i%d' % self.idx
46 self.idx += 1
47 return var
48
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -040049def gen_random_string():
50 return ''.join(random.choice(string.ascii_lowercase + string.digits) for _ in range(5))
51
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -040052class FOL2Python:
53 def __init__(self, context_map=None):
54 # This will produce i0, i1, i2 etc.
55 self.loopvar = iter(AutoVariable('i'))
56 self.verdictvar = iter(AutoVariable('result'))
57
58 self.loop_variable = self.loopvar.next()
59 self.verdict_variable = self.verdictvar.next()
60 self.context_map = context_map
61
62 if not self.context_map:
63 self.context_map = {'user': 'self', 'obj': 'obj'}
64
65 def loop_next(self):
66 self.loop_variable = self.loopvar.next()
67
68 def verdict_next(self):
69 self.verdict_variable = self.verdictvar.next()
70
71 def gen_enumerate(self, fol):
72 pass
73
74 def format_term_for_query(self, model, term, django=False):
75 if term.startswith(model + '.'):
76 term = term[len(model) + 1:]
77 if django:
78 term = term.replace('.', '__')
79 else:
80 term = '__elt' + '.' + term
81 return term
82
83 def fol_to_python_filter(self, model, e, django=False, negate=False):
84 try:
85 (k, v), = e.items()
86 except AttributeError:
87 return [self.format_term_for_query(model, e)]
88
89 if django:
90 if negate:
91 # De Morgan's negation
92 q_bracket = '~Q(%s)'
93 or_expr = ','
94 and_expr = '|'
95 else:
96 q_bracket = 'Q(%s)'
97 or_expr = '|'
98 and_expr = ','
99 else:
100 if negate:
101 # De Morgan's negation
102 q_bracket = 'not %s'
103 or_expr = ' and '
104 and_expr = ' or '
105 else:
106 q_bracket = '%s'
107 or_expr = ' or '
108 and_expr = ' and '
109
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400110 if k in ['=','in']:
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400111 v = [self.format_term_for_query(
112 model, term, django=django) for term in v]
113 if django:
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400114 operator_map = {'=':' = ','in':'__in'}
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400115 else:
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400116 operator_map = {'=':' == ','in':'in'}
117 operator = operator_map[k]
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400118 return [q_bracket % operator.join(v)]
119 elif k == '|':
120 components = [self.fol_to_python_filter(
121 model, x, django=django).pop() for x in v]
122 return [or_expr.join(components)]
123 elif k == '&':
124 components = [self.fol_to_python_filter(
125 model, x, django=django).pop() for x in v]
126 return [and_expr.join(components)]
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400127 elif k == '->':
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400128 components = [self.fol_to_python_filter(
129 model, x, django=django).pop() for x in v]
130 return ['~%s | %s' % (components[0], components[1])]
131
132 """ Convert a single leaf node from a string
133 to an AST"""
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400134 def str_to_ast(self, s):
135 ast_module = ast.parse(s)
136 return ast_module.body[0]
137
Sapan Bhatiab69f4702017-07-31 16:03:33 -0400138 def reduce_operands(self, operands):
139 if operands[0] in ['True','False']:
140 return (operands[0],operands[1])
141 elif operands[1] in ['True','False']:
142 return (operands[1],operands[0])
143 else:
144 return None
145
146 """ Simplify binops with constants """
147 def simplify_binop(self, binop):
148 (k,v), = binop.items()
149 if k == '->':
150 lhs, rhs = v
151 if lhs == 'True':
152 return rhs
153 elif rhs == 'True':
154 return 'True'
155 elif lhs == 'False':
156 return 'True'
157 elif rhs == 'False':
158 return {'not': lhs}
159
160 var_expr = self.reduce_operands(v)
161
162 if not var_expr: return binop
163 else:
164 constant, var = var_expr
165 if k=='|':
166 if constant=='True':
167 return 'True'
168 elif constant=='False':
169 return var
170 else:
171 raise Exception("Internal error - variable read as constant")
172 elif k=='&':
173 if constant=='True':
174 return var
175 elif constant=='False':
176 return 'False'
177
178 def is_constant(self, var, fol):
179 try:
180 (k, v), = fol.items()
181 except AttributeError:
182 k = 'term'
183 v = fol
184
185 if k in ['python', 'policy']:
186 # Treat as a constant and hoist, since it cannot be quantified
187 return True
188 elif k == 'term':
189 return not v.startswith(var)
190 elif k == 'not':
191 return self.is_constant(var, fol)
192 elif k in ['in', '=']:
193 lhs, rhs = v
194 return self.is_constant(var,lhs) and self.is_constant(var, rhs)
195 elif k in BINOPS:
196 lhs, rhs = v
197 return self.is_constant(lhs, var) and self.is_constant(rhs, var)
198 elif k in QUANTS:
199 is_constant = self.is_constant(var, fol[1])
200 return is_constant
201 else:
202 raise ConstructNotHandled(k)
203
204 def find_constants(self, var, fol, constants):
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400205 try:
206 (k, v), = fol.items()
207 except AttributeError:
208 k = 'term'
209 v = fol
210
Sapan Bhatiab69f4702017-07-31 16:03:33 -0400211 if k in ['python', 'policy']:
212 # Treat as a constant and hoist, since it cannot be quantified
213 if fol not in constants:
214 constants.append(fol)
215 return constants
216 elif k == 'term':
217 if not v.startswith(var):
218 constants.append(v)
219 return constants
220 elif k == 'not':
221 return self.find_constants(var, v, constants)
222 elif k in ['in', '=']:
223 lhs, rhs = v
224 if isinstance(lhs, str) and isinstance(rhs, str):
225 if not lhs.startswith(var) and not rhs.startswith(var):
226 constants.append(fol)
227 return constants
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400228 else:
Sapan Bhatiab69f4702017-07-31 16:03:33 -0400229 constants = self.find_constants(var, lhs, constants)
230 return self.find_constants(var, rhs, constants)
231 elif k in BINOPS:
232 lhs, rhs = v
233 constants = self.find_constants(var, lhs, constants)
234 constants = self.find_constants(var, rhs, constants)
235 return constants
236 elif k in QUANTS:
237 is_constant = self.is_constant(var, v[1])
238 if is_constant: constants.append(fol)
239 return constants
240 else:
241 raise ConstructNotHandled(k)
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400242
Sapan Bhatiab69f4702017-07-31 16:03:33 -0400243 """ Hoist constants out of quantifiers. Depth-first. """
244 def hoist_outer(self, fol):
245 try:
246 (k, v), = fol.items()
247 except AttributeError:
248 k = 'term'
249 v = fol
250
251 if k in ['python', 'policy']:
252 # Tainted, optimization and distribution not possible
253 return fol
254 elif k == 'term':
255 return fol
256 elif k == 'not':
257 vprime = self.hoist_outer(v)
258 return {'not': vprime}
259 elif k in ['in', '=']:
260 lhs, rhs = v
261 rlhs = self.hoist_outer(lhs)
262 rrhs = self.hoist_outer(rhs)
263 return {k:[rlhs,rrhs]}
264 elif k in BINOPS:
265 lhs, rhs = v
266 rlhs = self.hoist_outer(lhs)
267 rrhs = self.hoist_outer(rhs)
268
269 fol_prime = {k: [rlhs, rrhs]}
270 fol_simplified = self.simplify_binop(fol_prime)
271 return fol_simplified
272 elif k in QUANTS:
273 rexpr = self.hoist_outer(v[1])
274 return self.hoist_quant(k, [v[0],rexpr])
275 else:
276 raise ConstructNotHandled(k)
277
278 def replace_const(self, fol, c, value):
279 if fol == c:
280 return value
281
282 try:
283 (k, v), = fol.items()
284 except AttributeError:
285 k = 'term'
286 v = fol
287
288 if k == 'term':
289 if v == c: return value
290 else: return v
291 elif k == 'not':
292 new_expr = self.replace_const(v, c, value)
293 if new_expr=='True':
294 return 'False'
295 elif new_expr=='False':
296 return 'True'
297 else:
298 return {'not': new_expr}
299 elif k in ['in', '=']:
300 lhs, rhs = v
301 rlhs = self.replace_const(lhs, c, value)
302 rrhs = self.replace_const(rhs, c, value)
303
304 if rlhs==rrhs:
305 return 'True'
306 else:
307 return {k: [rlhs, rrhs]}
308 elif k in BINOPS:
309 lhs, rhs = v
310
311 rlhs = self.replace_const(lhs, c, value)
312 rrhs = self.replace_const(rhs, c, value)
313
314 return self.simplify_binop({k:[rlhs,rrhs]})
315 elif k in QUANTS:
316 var, expr = v
317 new_expr = self.replace_const(expr, c, value)
318 if new_expr in ['True', 'False']:
319 return new_expr
320 else:
321 return {k: [var, new_expr]}
322 else:
323 raise ConstructNotHandled(k)
324
325 def shannon_expand(self, c, fol):
326 lhs = self.replace_const(fol, c, 'True')
327 rhs = self.replace_const(fol, c, 'False')
328 not_c = {'not': c}
329 rlhs = {'&': [c, lhs]}
330 rlhs = self.simplify_binop(rlhs)
331
332 rrhs = {'&': [not_c, rhs]}
333 rrhs = self.simplify_binop(rrhs)
334
335 combined = {'|': [rlhs, rrhs]}
336 return self.simplify_binop(combined)
337
338 def hoist_quant(self, k, expr):
339 var, v = expr
340
341 constants = self.find_constants(var, v, constants=[])
342
343 fol = {k: expr}
344
345 for c in constants:
346 fol = self.shannon_expand(c, fol)
347
348 return fol
349
350 """
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400351 if var:
352 if k == 'term':
353 if not v.startswith(var):
354 return {'hoist': ['const', fol], 'result': 'True'}
355 else:
356 return {'hoist': [], 'result': fol}
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400357 elif k in ['=', 'in']:
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400358 lhs, rhs = v
359 if not lhs.startswith(var) and not rhs.startswith(var):
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400360 return {'hoist': [k, fol], 'result': 'True'} # XXX
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400361 else:
362 return {'hoist': [], 'result': fol}
363 elif k in BINOPS:
364 lhs, rhs = v
365 rlhs = self.hoist_constants(lhs, var)
366 rrhs = self.hoist_constants(rhs, var)
367
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400368 if rlhs['hoist'] and rrhs['hoist'] and rlhs['result']=='True' and llhs['result']=='True':
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400369 return {'hoist': ['=', fol], 'result': 'True'}
370 elif rlhs['hoist']:
371 return {'hoist': [k, lhs], 'result': rhs}
372 elif rrhs['hoist']:
373 return {'hoist': [k, rhs], 'result': lhs}
374 else:
375 return {'hoist': [], 'result': fol}
376
377 elif k in QUANTS:
378 var2, expr = v
379 result = self.hoist_constants(expr, var2)
380 if result['hoist']:
381 if result['result'] == 'True':
382 return {'hoist': ['const'], 'result': result['hoist'][1]}
383 elif result['hoist'][0] in BINOPS:
384 return {'hoist': ['const'], 'result': {result['hoist'][0]: [result['hoist'][1], {k: [var2, result['result']]}]}}
385 else:
386 return {'hoist': ['const'], 'result': {k: [var2, result['result']]}}
387 else:
388 result = self.hoist_constants(expr, var)
389 if result['result'] == 'True':
390 return {'hoist': ['&', fol], 'result': 'True'}
391 else:
392 return {'hoist': [], 'result': fol}
393 else:
394 return {'hoist': [], 'result': fol}
395 else:
396 if k in BINOPS:
397 lhs, rhs = v
398 rlhs = self.hoist_constants(lhs)
399 rrhs = self.hoist_constants(rhs)
400 return {k: [rlhs, rrhs]}
401 elif k in QUANTS:
402 var, expr = v
403 result = self.hoist_constants(expr, var)
404 if result['hoist']:
405 if result['result'] == 'True':
406 return result['hoist'][1]
407 elif result['hoist'][0] in BINOPS:
408 return {result['hoist'][0]: [result['hoist'][1], {k: [var, result['result']]}]}
409 else:
410 return {k: [var, result['result']]}
411 else:
412 return fol
413 else:
414 return fol
Sapan Bhatiab69f4702017-07-31 16:03:33 -0400415 """
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400416
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400417 def gen_validation_function(self, fol, policy_name, message, tag):
418 if not tag:
419 tag = gen_random_string()
420
Sapan Bhatiad3fcb662017-07-25 21:13:48 -0400421 policy_function_name_template = 'policy_%s_' + '%(random_string)s' % {'random_string': tag}
422 policy_function_name = policy_function_name_template % policy_name
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400423 self.verdict_next()
424 function_str = """
425def %(fn_name)s(obj, ctx):
Sapan Bhatia9227b4d2017-07-25 23:14:48 -0400426 if not %(vvar)s: raise ValidationError("%(message)s".format(obj=obj, ctx=ctx))
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400427 """ % {'fn_name': policy_function_name, 'vvar': self.verdict_variable, 'message': message}
428
429 function_ast = self.str_to_ast(function_str)
Sapan Bhatiad3fcb662017-07-25 21:13:48 -0400430 policy_code = self.gen_test(policy_function_name_template, fol, self.verdict_variable)
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400431
432
433 function_ast.body = [policy_code] + function_ast.body
434
435 return function_ast
436
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400437 def gen_test_function(self, fol, policy_name, tag):
438 if not tag:
439 tag = gen_random_string()
440
Sapan Bhatiab5ce1862017-07-31 15:48:19 -0400441 policy_function_name_template = '%s_' + '%(random_string)s' % {'random_string': tag}
Sapan Bhatiad3fcb662017-07-25 21:13:48 -0400442 policy_function_name = policy_function_name_template % policy_name
443
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400444 self.verdict_next()
445 function_str = """
446def %(fn_name)s(obj, ctx):
447 return %(vvar)s
448 """ % {'fn_name': policy_function_name, 'vvar': self.verdict_variable}
449
450 function_ast = self.str_to_ast(function_str)
Sapan Bhatiad3fcb662017-07-25 21:13:48 -0400451 policy_code = self.gen_test(policy_function_name_template, fol, self.verdict_variable)
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400452
453 function_ast.body = [policy_code] + function_ast.body
454
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400455 return function_ast
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400456
Sapan Bhatiad3fcb662017-07-25 21:13:48 -0400457 def gen_test(self, fn_template, fol, verdict_var, bindings=None):
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400458 if isinstance(fol, str):
459 return self.str_to_ast('%(verdict_var)s = %(constant)s' % {'verdict_var': verdict_var, 'constant': fol})
460
461 (k, v), = fol.items()
462
Sapan Bhatiad3fcb662017-07-25 21:13:48 -0400463 if k == 'policy':
464 policy_name, object_name = v
465
466 policy_fn = fn_template % policy_name
467 call_str = """
Sapan Bhatiac6543dd2017-12-07 11:40:36 -0500468if obj.%(object_name)s:
469 %(verdict_var)s = %(policy_fn)s(obj.%(object_name)s, ctx)
470else:
471 # Everybody has access to null objects
472 %(verdict_var)s = True
Sapan Bhatiab69f4702017-07-31 16:03:33 -0400473 """ % {'verdict_var': verdict_var, 'policy_fn': policy_fn, 'object_name': object_name}
Sapan Bhatiad3fcb662017-07-25 21:13:48 -0400474
475 call_ast = self.str_to_ast(call_str)
476 return call_ast
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400477 if k == 'python':
478 try:
479 expr_ast = self.str_to_ast(v)
480 except SyntaxError:
481 raise PolicyException('Syntax error in %s' % v)
482
483 if not isinstance(expr_ast, ast.Expr):
484 raise PolicyException(
485 '%s is not an expression' % expr_ast)
486
487 assignment_str = """
488%(verdict_var)s = (%(escape_expr)s)
Sapan Bhatiab69f4702017-07-31 16:03:33 -0400489 """ % {'verdict_var': verdict_var, 'escape_expr': v}
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400490
491 assignment_ast = self.str_to_ast(assignment_str)
492 return assignment_ast
493 elif k == 'not':
Sapan Bhatiab69f4702017-07-31 16:03:33 -0400494 top_vvar = verdict_var
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400495 self.verdict_next()
496 sub_vvar = self.verdict_variable
Sapan Bhatiad3fcb662017-07-25 21:13:48 -0400497 block = self.gen_test(fn_template, v, sub_vvar)
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400498 assignment_str = """
499%(verdict_var)s = not (%(subvar)s)
500 """ % {'verdict_var': top_vvar, 'subvar': sub_vvar}
501
502 assignment_ast = self.str_to_ast(assignment_str)
503
504 return ast.Module(body=[block, assignment_ast])
505 elif k in ['=','in']:
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400506 # This is the simplest case, we don't recurse further
507 # To use terms that are not simple variables, use
508 # the Python escape, e.g. {{ slice.creator is not None }}
509 lhs, rhs = v
510
511 assignments = []
512
513 try:
514 for t in lhs, rhs:
515 py_expr = t['python']
516
517 self.verdict_next()
518 vv = self.verdict_variable
519
520 try:
521 expr_ast = self.str_to_ast(py_expr)
522 except SyntaxError:
523 raise PolicyException('Syntax error in %s' % v)
524
525 if not isinstance(expr_ast, ast.Expr):
526 raise PolicyException(
527 '%s is not an expression' % expr_ast)
528
529 assignment_str = """
530%(verdict_var)s = (%(escape_expr)s)
531 """ % {'verdict_var': vv, 'escape_expr': py_expr}
532
533 if t == lhs:
534 lhs = vv
535 else:
536 rhs = vv
537
538 assignment_ast = self.str_to_ast(assignment_str)
539 assignments.append(assignment_ast)
540 except TypeError:
541 pass
542
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400543 if k=='=':
544 operator='=='
545 elif k=='in':
546 operator='in'
547
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400548 comparison_str = """
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400549%(verdict_var)s = (%(lhs)s %(operator)s %(rhs)s)
550 """ % {'verdict_var': verdict_var, 'lhs': lhs, 'rhs': rhs, 'operator':operator}
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400551
552 comparison_ast = self.str_to_ast(comparison_str)
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400553 combined_ast = ast.Module(body=assignments + [comparison_ast])
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400554
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400555 return combined_ast
556 elif k in BINOPS:
557 lhs, rhs = v
558
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400559 top_vvar = verdict_var
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400560
561 self.verdict_next()
562 lvar = self.verdict_variable
563
564 self.verdict_next()
565 rvar = self.verdict_variable
566
Sapan Bhatiad3fcb662017-07-25 21:13:48 -0400567 lblock = self.gen_test(fn_template, lhs, lvar)
568 rblock = self.gen_test(fn_template, rhs, rvar)
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400569
570 invert = ''
571 if k == '&':
572 binop = 'and'
573 elif k == '|':
574 binop = 'or'
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400575 elif k == '->':
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400576 binop = 'or'
577 invert = 'not'
578
579 binop_str = """
580%(verdict_var)s = %(invert)s %(lvar)s %(binop)s %(rvar)s
581 """ % {'verdict_var': top_vvar, 'invert': invert, 'lvar': lvar, 'binop': binop, 'rvar': rvar}
582
583 binop_ast = self.str_to_ast(binop_str)
584
585 combined_ast = ast.Module(body=[lblock, rblock, binop_ast])
586 return combined_ast
587 elif k == 'exists':
588 # If the variable starts with a capital letter,
589 # we assume that it is a model. If it starts with
590 # a small letter, we assume it is an enumerable
591 #
592 # We do not support nested exists yet. FIXME.
593
594 var, expr = v
595
596 if var.istitle():
597 f = self.fol_to_python_filter(var, expr, django=True)
598 entry = f.pop()
599
600 python_str = """
Sapan Bhatia9227b4d2017-07-25 23:14:48 -0400601%(verdict_var)s = not not %(model)s.objects.filter(%(query)s)
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400602 """ % {'verdict_var': verdict_var, 'model': var, 'query': entry}
603
604 python_ast = ast.parse(python_str)
605 else:
606 f = self.fol_to_python_filter(var, expr, django=False)
607 entry = f.pop()
608
609 python_str = """
610%(verdict_var)s = filter(lambda __elt:%(query)s, %(model)s)
611 """ % {'verdict_var': verdict_var, 'model': var, 'query': entry}
612
613 python_ast = ast.parse(python_str)
614
615 return python_ast
616 elif k=='forall':
617 var, expr = v
618
619 if var.istitle():
620 f = self.fol_to_python_filter(var, expr, django=True, negate = True)
621 entry = f.pop()
622
623 self.verdict_next()
624 vvar = self.verdict_variable
625
626 python_str = """
Sapan Bhatia9227b4d2017-07-25 23:14:48 -0400627%(verdict_var)s = not not %(model)s.objects.filter(%(query)s)
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400628 """ % {'verdict_var': vvar, 'model': var, 'query': entry}
629
630 python_ast = ast.parse(python_str)
631 else:
632 f = self.fol_to_python_filter(var, expr, django=False, negate = True)
633 entry = f.pop()
634
635 python_str = """
636%(verdict_var)s = next(elt for elt in %(model)s if %(query)s)
637 """ % {'verdict_var': vvar, 'model': var, 'query': entry}
638
639 python_ast = ast.parse(python_str)
640
641 negate_str = """
642%(verdict_var)s = not %(vvar)s
643 """ % {'verdict_var': verdict_var, 'vvar': vvar}
644
645 negate_ast = ast.parse(negate_str)
646
647 return ast.Module(body=[python_ast, negate_ast])
648
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400649def xproto_fol_to_python_test(policy, fol, model, tag=None):
650 if isinstance(fol, jinja2.Undefined):
651 raise Exception('Could not find policy:', policy)
652
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400653 f2p = FOL2Python()
Sapan Bhatiab69f4702017-07-31 16:03:33 -0400654 fol_reduced = f2p.hoist_outer(fol)
655
656 if fol_reduced in ['True','False'] and fol != fol_reduced:
657 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})
658
Sapan Bhatiab5ce1862017-07-31 15:48:19 -0400659 a = f2p.gen_test_function(fol_reduced, policy, tag='security_check')
Sapan Bhatiab69f4702017-07-31 16:03:33 -0400660
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400661 return astunparse.unparse(a)
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400662
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400663def xproto_fol_to_python_validator(policy, fol, model, message, tag=None):
664 if isinstance(fol, jinja2.Undefined):
665 raise Exception('Could not find policy:', policy)
666
667 f2p = FOL2Python()
Sapan Bhatiab69f4702017-07-31 16:03:33 -0400668 fol_reduced = f2p.hoist_outer(fol)
669
670 if fol_reduced in ['True','False'] and fol != fol_reduced:
671 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})
672
673 a = f2p.gen_validation_function(fol_reduced, policy, message, tag='validator')
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400674
675 return astunparse.unparse(a)
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400676
677def main():
678 while True:
Sapan Bhatiab69f4702017-07-31 16:03:33 -0400679 inp = ''
680 while True:
681 inp_line = raw_input()
682 if inp_line=='EOF': break
683 else: inp+=inp_line
684
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400685 fol_lexer = lex.lex(module=FOLLexer())
Sapan Bhatia6e346832018-01-12 12:08:21 -0500686 fol_parser = yacc.yacc(module=FOLParser(), start='goal', outputdir='/tmp', debug=0)
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400687
688 val = fol_parser.parse(inp, lexer=fol_lexer)
Sapan Bhatia5ea307d2017-07-19 00:13:21 -0400689 a = xproto_fol_to_python_test('pol', val, 'output', 'Test')
Sapan Bhatiab69f4702017-07-31 16:03:33 -0400690 #f2p = FOL2Python()
691 #a = f2p.hoist_outer(val)
Sapan Bhatia3e3c1cd2017-07-15 01:35:44 -0400692 print a
693
694
695if __name__ == "__main__":
696 main()