From 4b2b6fafbe6d717b401864913acd447d20e5cfde Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre=20Cr=C3=A9gut?= Date: Fri, 26 Oct 2018 14:43:20 +0200 Subject: [PATCH] builtins for z3 theories Adds basic comparison, arithmetic and bit arithmetic to Z3 theories. Builtins depend on the kind of theory in use. Z3 builtins are the only polymorphic predicates of the engine. Change-Id: Icb68c71ec29604638282a34d34ce06f1e1d69275 Implements: blueprint alternative-engine-z3 --- congress/tests/z3/test_typechecker.py | 20 +++- congress/tests/z3/test_z3theory.py | 62 +++++++++++-- congress/tests/z3/z3mock.py | 56 +++++++++-- congress/z3/typechecker.py | 93 ++++++++++++++----- congress/z3/z3builtins.py | 53 +++++++++++ congress/z3/z3theory.py | 64 +++++++------ congress/z3/z3types.py | 2 +- doc/source/user/policy.rst | 26 +++++- .../notes/z3-builtins-461251858ea2bf88.yaml | 8 ++ 9 files changed, 311 insertions(+), 73 deletions(-) create mode 100644 congress/z3/z3builtins.py create mode 100644 releasenotes/notes/z3-builtins-461251858ea2bf88.yaml diff --git a/congress/tests/z3/test_typechecker.py b/congress/tests/z3/test_typechecker.py index f02e743da..3b6c0112b 100644 --- a/congress/tests/z3/test_typechecker.py +++ b/congress/tests/z3/test_typechecker.py @@ -170,7 +170,8 @@ class TestTypeChecker(base.TestCase): self.world['t2'] = t2 self.rules = ast.parse( 'l(2). l(3). p(x) :- l(x). q(x,x) :- m(x). ' - 'm("a"). k(x) :- t2:f(x). r(y) :- q(x,y).') + 'm("a"). k(x) :- t2:f(x). r(y) :- q(x,y). ' + 's(x) :- l(y),builtin:plus(y, 2, x).') for rule in self.rules: t1.insert(rule) for rule in ast.parse("f(3)."): @@ -192,12 +193,21 @@ class TestTypeChecker(base.TestCase): tc = typechecker.Typechecker([self.t1], self.world) tc.reset_type_environment() env = tc.type_env - self.assertEqual(4, len(env.keys())) + self.assertEqual(5, len(env.keys())) for variables in six.itervalues(env): for (v, cell) in six.iteritems(variables): self.assertIn(v, [u'x', u'y']) self.assertEqual(mkc(None, False), cell) + def test_reset_polymorphic_calls(self): + tc = typechecker.Typechecker([self.t1], self.world) + tc.reset_type_environment() + env = tc.type_env_builtins + rule = self.rules[7] + typ = mkc(None, False) + self.assertEqual(5, len(env.keys())) + self.assertEqual({1: [typ, typ, typ]}, env[rule.id]) + def test_type_facts(self): tc = typechecker.Typechecker([self.t1], self.world) tc.reset_types() @@ -225,10 +235,14 @@ class TestTypeChecker(base.TestCase): def test_type_all(self): tc = typechecker.Typechecker([self.t1], self.world) - tc.type_all() + type_env = tc.type_all() smap = self.t1.schema.map self.assertEqual('Int', smap['p'][0]['type']) # propagation of l self.assertEqual('Str', smap['q'][0]['type']) # propagation of m self.assertEqual('Str', smap['q'][1]['type']) self.assertEqual('Str', smap['r'][0]['type']) self.assertEqual('Scalar', smap['k'][0]['type']) # prop of ext table + self.assertEqual('Int', smap['s'][0]['type']) # through builtins + rule = self.rules[7] + typ = mkc('Int', False) + self.assertEqual([typ, typ, typ], type_env[rule.id][1]) diff --git a/congress/tests/z3/test_z3theory.py b/congress/tests/z3/test_z3theory.py index bcb006375..863db9979 100644 --- a/congress/tests/z3/test_z3theory.py +++ b/congress/tests/z3/test_z3theory.py @@ -252,6 +252,17 @@ class TestZ3Context(base.TestCase): context.declare_tables() return (context, t1, rule) + def init_one_builtin(self, body, typ, arity): + context = z3theory.Z3Context() + world = {} + t1 = z3theory.Z3Theory('t1', theories=world) + world['t1'] = t1 + context.register(t1) + rule = ast.parse('p(x) :- ' + body + '.')[0] + t1.schema.map['p'] = [mkc(typ)] + context.declare_tables() + return (context, t1, rule, {0: [mkc(typ)] * arity}) + def init_one_theory(self, prog): context = z3theory.Z3Context() world = {} @@ -265,7 +276,7 @@ class TestZ3Context(base.TestCase): @mockz3 def test_compile_atoms(self): (context, t1, rule) = self.init_one_rule() - result = context.compile_atoms(t1, rule.head, rule.body) + result = context.compile_atoms({}, t1, rule.head, rule.body) self.assertEqual(3, len(result)) (vars, head, body) = result self.assertEqual(2, len(vars)) @@ -284,10 +295,45 @@ class TestZ3Context(base.TestCase): self.assertEqual(z3.Z3_OP_UNINTERPRETED, body[1].children()[1].decl().kind()) + @mockz3 + def test_compile_binop_builtin(self): + tests = [('plus', 'bvadd'), ('minus', 'bvsub'), ('mul', 'bvmul'), + ('and', 'bvand'), ('or', 'bvor')] + for (datalogName, z3Name) in tests: + (context, t1, rule, env) = self.init_one_builtin( + 'builtin:' + datalogName + '(2, 3, x)', 'Int', 3) + result = context.compile_atoms(env, t1, rule.head, rule.body) + (_, _, body) = result + # two literals in the body + self.assertEqual(1, len(body)) + # First body literal is l + eqExpr = body[0] + self.assertEqual('=', eqExpr.decl().name()) + right = eqExpr.children()[0] + self.assertEqual(z3Name, right.decl().name()) + self.assertEqual(2, right.children()[0].as_long()) + self.assertEqual(3, right.children()[1].as_long()) + + @mockz3 + def test_compile_builtin_tests(self): + tests = [('gt', 'bvsgt'), ('lt', 'bvslt'), ('gteq', 'bvsge'), + ('lteq', 'bvsle'), ('equal', '=')] + for (datalogName, z3Name) in tests: + (context, t1, rule, env) = self.init_one_builtin( + 'builtin:' + datalogName + '(2, x)', 'Int', 2) + result = context.compile_atoms(env, t1, rule.head, rule.body) + (_, _, body) = result + # two literals in the body + self.assertEqual(1, len(body)) + # First body literal is l + testExpr = body[0] + self.assertEqual(z3Name, testExpr.decl().name()) + self.assertEqual(2, testExpr.children()[0].as_long()) + @mockz3 def test_compile_rule(self): (context, t1, rule) = self.init_one_rule() - context.compile_rule(t1, rule) + context.compile_rule({}, t1, rule) result = context.context._rules[0] # pylint: disable=E1101 self.assertEqual('forall', result.decl().name()) self.assertEqual('=>', result.children()[2].decl().name()) @@ -306,14 +352,14 @@ class TestZ3Context(base.TestCase): context = self.init_three_theories() context.declare_tables() context.declare_external_tables() - context.compile_theory(context.z3theories['t1']) + context.compile_theory({}, context.z3theories['t1']) rules = context.context._rules # pylint: disable=E1101 self.assertEqual(3, len(rules)) @mockz3 def test_compile_all(self): context = self.init_three_theories() - context.compile_all() + context.compile_all({}) rules = context.context._rules # pylint: disable=E1101 rels = context.context._relations # pylint: disable=E1101 self.assertEqual(4, len(rules)) @@ -412,8 +458,8 @@ class TestTypeConstraints(base.TestCase): @mockz3 def test_compile_all_ok(self): context = self.init_two_theories('p("a"). p(x) :- t2:p(x).') - context.typecheck() - context.compile_all() + env = context.typecheck() + context.compile_all(env) rules = context.context._rules # pylint: disable=E1101 self.assertEqual(2, len(rules)) @@ -427,7 +473,7 @@ class TestTypeConstraints(base.TestCase): def test_compile_fails_values(self): context = self.init_two_theories('p("c"). p(x) :- t2:p(x).') # Type-check succeeds - context.typecheck() + env = context.typecheck() # But we are caught when trying to convert 'c' as a 'Small' value self.assertRaises(exception.PolicyRuntimeException, - context.compile_all) + context.compile_all, env) diff --git a/congress/tests/z3/z3mock.py b/congress/tests/z3/z3mock.py index a2531737d..73ea8c55f 100644 --- a/congress/tests/z3/z3mock.py +++ b/congress/tests/z3/z3mock.py @@ -85,9 +85,15 @@ class ExprRef(object): return repr(self._decl) + repr(self.args) +class BoolRef(ExprRef): + def __init__(self, decl, args): + super(BoolRef, self).__init__(decl, args) + pass + + class BitVecRef(ExprRef): - def __init__(self, decl, val, sort): - super(BitVecRef, self).__init__(decl, []) + def __init__(self, decl, args, sort, val=None): + super(BitVecRef, self).__init__(decl, args) self.val = val self.sort = sort @@ -97,16 +103,50 @@ class BitVecRef(ExprRef): def size(self): return self.sort.size() + def __add__(self, b): + return BitVecRef(FuncDeclRef('bvadd', 1028), [self, b], self.sort) + + def __sub__(self, b): + return BitVecRef(FuncDeclRef('bvsub', 1029), [self, b], self.sort) + + def __mul__(self, b): + return BitVecRef(FuncDeclRef('bvmul', 1030), [self, b], self.sort) + + def __or__(self, b): + return BitVecRef(FuncDeclRef('bvor', 1050), [self, b], self.sort) + + def __and__(self, b): + return BitVecRef(FuncDeclRef('bvand', 1049), [self, b], self.sort) + + def __not__(self, b): + return BitVecRef(FuncDeclRef('bvnot', 1051), [self, b], self.sort) + + def __lt__(self, b): + return BoolRef(FuncDeclRef('bvslt', 1046), [self, b]) + + def __le__(self, b): + return BoolRef(FuncDeclRef('bvsle', 1042), [self, b]) + + def __gt__(self, b): + return BoolRef(FuncDeclRef('bvsgt', 1048), [self, b]) + + def __ge__(self, b): + return BoolRef(FuncDeclRef('bvsge', 1044), [self, b]) + + def __eq__(self, b): + return BoolRef(FuncDeclRef('=', 258), [self, b]) + + def __ne__(self, b): + return BoolRef(FuncDeclRef('distinct', 259), [self, b]) + def __repr__(self): - return "bv({})".format(self.val) + return ( + "bv({})".format(self.val) if self.val is not None + else super(BitVecRef, self).__repr__()) def BitVecVal(v, s): - return BitVecRef(FuncDeclRef('bv', Z3_OP_BNUM), v, s) - - -class BoolRef(ExprRef): - pass + return BitVecRef(FuncDeclRef('bv', Z3_OP_BNUM), [], s, v) def BoolVal(val): diff --git a/congress/z3/typechecker.py b/congress/z3/typechecker.py index a74951099..6773e7906 100644 --- a/congress/z3/typechecker.py +++ b/congress/z3/typechecker.py @@ -64,6 +64,7 @@ import six from congress import data_types from congress.datalog import compile as ast from congress import exception +from congress.z3 import z3builtins MYPY = False # pylint: disable = ungrouped-imports @@ -76,12 +77,13 @@ if MYPY: CELLTYPE = TypedDict( 'CELLTYPE', {'nullable': bool, 'type': Optional[str]}) + GEN_TYPE_ENV = Dict[str, Dict[int, List[CELLTYPE]]] LOG = logging.getLogger(__name__) def min_type(name1, name2, strict): - # type: (str, str, boolean) -> Optional[str] + # type: (str, str, bool) -> Optional[str] """Given two type names, gives back the most precise one or None. If one of the type is more precise than the other, give it back otherwise @@ -108,6 +110,7 @@ class Typechecker(object): self.work = False self.once = False self.type_env = {} # type: Dict[str, Dict[str, CELLTYPE]] + self.type_env_builtins = {} # type: GEN_TYPE_ENV def constrain_type(self, cell, typ): # type: (CELLTYPE, str) -> None @@ -129,7 +132,7 @@ class Typechecker(object): self.work = True def type_cells(self, cell1, cell2, strict): - # type: (CELLTYPE, Union[str, CELLTYPE]) -> Optional[str] + # type: (CELLTYPE, Union[str, CELLTYPE], bool) -> Optional[str] """Propagates type constraints between two type cells Updates work if a change has been made. @@ -156,18 +159,19 @@ class Typechecker(object): if typ1 is None and typ2 is not None: cell1['type'] = typ2 self.work = True - elif typ1 is not None and typ2 is None: - cell2['type'] = typ1 - self.work = True - elif typ1 is not None: # then typ2 is not None too - if typ1 != typ2: - typ3 = min_type(typ1, typ2, strict) - if typ3 is not None: - cell1['type'] = typ3 - cell2['type'] = typ3 - self.work = True - else: - return "{} != {}".format(typ1, typ2) + elif typ1 is not None: + if typ2 is None: + cell2['type'] = typ1 + self.work = True + else: # then typ2 is not None too + if typ1 != typ2: + typ3 = min_type(typ1, typ2, strict) + if typ3 is not None: + cell1['type'] = typ3 + cell2['type'] = typ3 + self.work = True + else: + return "{} != {}".format(typ1, typ2) # else: two unresolved constraints, we do nothing return None @@ -189,6 +193,32 @@ class Typechecker(object): def reset_type_environment(self): """Reset the type environment for all variables in rules""" + def builtin_type_env(atom): + """Generates the type of a builtin. + + The builtin can be polymorphic + For a fixed type, we must tell if the type is nullable. + Nullable types must begin with character @. + """ + tablename = atom.table.table + builtin = z3builtins.BUILTINS.get(tablename) + if builtin is None: + raise exception.PolicyRuntimeException( + 'Unknown builtin {}'.format(tablename)) + typ_vars = [ + {'type': None, 'nullable': False} + for _ in range(builtin.ty_vars)] + + def cell(t): + return ( + {'type': arg[1:], 'nullable': True} + if arg[0] == '@' + else {'type': arg, 'nullable': False}) + return [ + typ_vars[arg] if isinstance(arg, int) else cell(arg) + for arg in builtin.args + ] + self.type_env = { rule.id: { variable.name: {'type': None, 'nullable': False} @@ -198,6 +228,16 @@ class Typechecker(object): for ruleset in theory.rules.rules.values() for rule in ruleset } + self.type_env_builtins = { + rule.id: { + pos: builtin_type_env(atom) + for (pos, atom) in enumerate(rule.body) + if atom.table.service == 'builtin' + } + for theory in self.theories + for ruleset in theory.rules.rules.values() + for rule in ruleset + } def reset_types(self): """Set all types in theory to typechecks to bottom""" @@ -227,18 +267,23 @@ class Typechecker(object): """One type iteration over a single rule""" LOG.debug("Type rule %s", rule.id) var_types = self.type_env[rule.id] + builtin_types = self.type_env_builtins[rule.id] - def type_atom(atom): - # type: (ast.Literal) -> None + def type_atom(atom, pos): + # type: (ast.Literal, int) -> None """Type iteration for a single atom""" table = atom.table svc = theory.name if table.service is None else table.service tablename = table.table if svc == 'builtin': - raise exception.PolicyRuntimeException( - 'typing Z3 theories with builtin not supported yet') - strict = svc not in self.theorynames - tbl_schema = self.world[svc].schema.map[tablename] + if pos == -1: + raise exception.PolicyRuntimeException( + 'builtin not authorized in rule head') + strict = False + tbl_schema = builtin_types.get(pos, []) # type: List[CELLTYPE] + else: + strict = svc not in self.theorynames + tbl_schema = self.world[svc].schema.map[tablename] for (arg, typ_col) in six.moves.zip(atom.arguments, tbl_schema): if isinstance(arg, ast.Variable): typ_var = var_types[arg.name] @@ -252,11 +297,12 @@ class Typechecker(object): elif isinstance(arg, ast.ObjectConstant) and self.once: self.type_constant(arg.name, typ_col) - for atom in rule.body: - type_atom(atom) - type_atom(rule.head) + for (pos, atom) in enumerate(rule.body): + type_atom(atom, pos) + type_atom(rule.head, -1) def type_all(self): + # type: () -> GEN_TYPE_ENV """Iterative typechecker""" self.reset_types() self.reset_type_environment() @@ -273,3 +319,4 @@ class Typechecker(object): for rule in ruleset: self.type_rule(theory, rule) self.once = False + return self.type_env_builtins diff --git a/congress/z3/z3builtins.py b/congress/z3/z3builtins.py new file mode 100644 index 000000000..c68bdbe02 --- /dev/null +++ b/congress/z3/z3builtins.py @@ -0,0 +1,53 @@ +# Copyright (c) 2018 Orange. All rights reserved. +# +# Licensed under the Apache License, Version 2.0 (the "License"); you may +# not use this file except in compliance with the License. You may obtain +# a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +# WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +# License for the specific language governing permissions and limitations +# under the License. +# + +import collections + +# BuiltinPred describes a builtin predicate +# +# @param ty_vars: the number of generic type variables +# @param args: an array describing the type of each argument of the predicate. +# It is a string for standard type and an integer for type variables in +# the range 0, ty_vars - 1. +# @param z3: a function generating the z3 code from an array coding the +# z3 arguments +BuiltinPred = collections.namedtuple( + 'BuiltinPred', + ['args', 'ty_vars', 'z3']) + +# Warning: the z3 code operates on syntax and builds syntax. It does not +# perform an operation on the fly. This is a clever trick of z3 library +# but may puzzle the casual reader. +BUILTINS = { + # Bit arithmetic + "and": BuiltinPred( + ty_vars=1, args=[0, 0, 0], z3=(lambda x, y, z: z == x & y)), + "or": BuiltinPred( + ty_vars=1, args=[0, 0, 0], z3=(lambda x, y, z: z == x | y)), + "bnot": BuiltinPred(ty_vars=1, args=[0, 0], z3=(lambda x, y: y == ~x)), + # Arithmetic (limited as it may render z3 slow in some modes) + "plus": BuiltinPred( + ty_vars=1, args=[0, 0, 0], z3=(lambda x, y, z: z == x + y)), + "minus": BuiltinPred( + ty_vars=1, args=[0, 0, 0], z3=(lambda x, y, z: z == x - y)), + "mul": BuiltinPred( + ty_vars=1, args=[0, 0, 0], z3=(lambda x, y, z: z == x * y)), + # Comparisons + "lt": BuiltinPred(ty_vars=1, args=[0, 0], z3=(lambda x, y: x < y)), + "lteq": BuiltinPred(ty_vars=1, args=[0, 0], z3=(lambda x, y: x <= y)), + "equal": BuiltinPred(ty_vars=1, args=[0, 0], z3=(lambda x, y: x == y)), + "gteq": BuiltinPred(ty_vars=1, args=[0, 0], z3=(lambda x, y: x >= y)), + "gt": BuiltinPred(ty_vars=1, args=[0, 0], z3=(lambda x, y: x > y)), +} diff --git a/congress/z3/z3theory.py b/congress/z3/z3theory.py index 24ac6a228..3b8b0c277 100644 --- a/congress/z3/z3theory.py +++ b/congress/z3/z3theory.py @@ -30,6 +30,7 @@ from congress.datalog import ruleset from congress.datalog import unify from congress import exception from congress.z3 import typechecker +from congress.z3 import z3builtins from congress.z3 import z3types # pylint: disable = ungrouped-imports @@ -37,7 +38,8 @@ MYPY = False if MYPY: # pylint: disable = unused-import from congress.datalog import topdown # noqa - from typing import Dict, Callable, Union, List, Any, Tuple # noqa + from mypy_extensions import TypedDict # noqa + from typing import Dict, Callable, Optional, Union, List, Any, Tuple # noqa import z3 # noqa Z3_RESULT = Tuple[Union[bool, List[List[z3.ExprRef]]], List[ast.Variable], @@ -219,16 +221,16 @@ class Z3Context(object): # There is no reset on Z3 context. Replace with a new one. self.context = Z3OPT.Fixedpoint() self.context.set(**Z3_ENGINE_OPTIONS) - self.typecheck() - self.compile_all() + type_env = self.typecheck() + self.compile_all(type_env) self.synchronize_external() z3query = self.compile_query(theory, query) self.context.query(z3query) z3answer = self.context.get_answer() answer = z3types.z3_to_array(z3answer) typ_args = theory.schema.types(query.table.table) - variables = [] - translators = [] + variables = [] # type: List[ast.Variable] + translators = [] # type: List[z3types.Z3Type] for arg, typ_arg in six.moves.zip(query.arguments, typ_args): if isinstance(arg, ast.Variable) and arg not in variables: translators.append( @@ -286,7 +288,8 @@ class Z3Context(object): """Declares the table of a litteral if necessary""" service = lit.table.service table = lit.table.table - if service is not None and service not in self.z3theories: + if (service is not None and service != 'builtin' and + service not in self.z3theories): self.externals.add((service, table)) for theory in six.itervalues(self.z3theories): for rules in six.itervalues(theory.rules.rules): @@ -312,6 +315,7 @@ class Z3Context(object): self.context.fact(z3fact) def compile_atoms(self, + type_env, theory, # type: Z3Theory head, # type: ast.Literal body # type: List[ast.Literal] @@ -340,20 +344,26 @@ class Z3Context(object): raise exception.PolicyException( "Expr {} not handled by Z3".format(expr)) - def compile_atom(literal): + def compile_atom(literal, pos=-1): """Compiles an atom in Z3""" name = literal.table.table svc = literal.table.service if svc == 'builtin': - raise exception.PolicyException( - "Builtins not handled by Z3 yet") - lit_theory = theory if svc is None else self.theories[svc] - translators = [ - self.type_registry.get_translator(str(arg_type.type)) - for arg_type in lit_theory.schema.types(name)] - fullname = lit_theory.name + ":" + name + translators = [ + self.type_registry.get_translator(str(arg_type['type'])) + for arg_type in type_env[pos] + ] + fullname = 'builtin:'+name + else: + lit_theory = theory if svc is None else self.theories[svc] + translators = [ + self.type_registry.get_translator(str(arg_type.type)) + for arg_type in lit_theory.schema.types(name)] + fullname = lit_theory.name + ":" + name try: - z3func = self.relations[fullname] + z3func = ( + z3builtins.BUILTINS[name].z3 if svc == 'builtin' + else self.relations[fullname]) z3args = (compile_expr(arg, tr) for (arg, tr) in six.moves.zip(literal.arguments, translators)) @@ -365,20 +375,20 @@ class Z3Context(object): "Z3: Relation %s not registered" % fullname) z3head = compile_atom(head) - z3body = [compile_atom(atom) for atom in body] + z3body = [compile_atom(atom, pos) for (pos, atom) in enumerate(body)] # We give back variables explicitely and do not rely on declare_var and # abstract. Otherwise rules are cluttered with useless variables. return (z3vars, z3head, z3body) - def compile_rule(self, theory, rule): - # type: (Z3Theory, ast.Rule) -> None + def compile_rule(self, type_env, theory, rule): + # type: (typechecker.GEN_TYPE_ENV, Z3Theory, ast.Rule) -> None """compiles a single rule :param theory: the theory containing the rule :param rule: the rule to compile. """ - z3vars, z3head, z3body = self.compile_atoms(theory, rule.head, - rule.body) + z3vars, z3head, z3body = self.compile_atoms( + type_env.get(rule.id, {}), theory, rule.head, rule.body) term1 = (z3head if z3body == [] else Z3OPT.Implies(Z3OPT.And(*z3body), z3head)) term2 = term1 if z3vars == [] else Z3OPT.ForAll(z3vars, term1) @@ -392,11 +402,11 @@ class Z3Context(object): :param litteral: the query :returns: an existentially quantified litteral in Z3 format. """ - z3vars, z3head, _ = self.compile_atoms(theory, literal, []) + z3vars, z3head, _ = self.compile_atoms({}, theory, literal, []) return z3head if z3vars == [] else Z3OPT.Exists(z3vars, z3head) - def compile_theory(self, theory): - # type: (Z3Theory) -> None + def compile_theory(self, type_env, theory): + # type: (typechecker.GEN_TYPE_ENV, Z3Theory) -> None """Compiles all the rules of a theory :param theory: theory to compile. Will be marked clean after. @@ -404,24 +414,24 @@ class Z3Context(object): self.compile_facts(theory) for rules in six.itervalues(theory.rules.rules): for rule in rules: - self.compile_rule(theory, rule) + self.compile_rule(type_env, theory, rule) theory.dirty = False - def compile_all(self): + def compile_all(self, type_env): """Compile all Z3 theories""" self.relations = {} self.externals.clear() self.declare_tables() self.declare_external_tables() for theory in six.itervalues(self.z3theories): - self.compile_theory(theory) + self.compile_theory(type_env, theory) self.last_compiled = time.time() def typecheck(self): """Typechecker for rules defined""" typer = typechecker.Typechecker( self.z3theories.values(), self.theories) - typer.type_all() + return typer.type_all() def inject(self, theoryname, tablename): # type: (str, str) -> None diff --git a/congress/z3/z3types.py b/congress/z3/z3types.py index d99284886..65cd302ec 100644 --- a/congress/z3/z3types.py +++ b/congress/z3/z3types.py @@ -45,7 +45,7 @@ class Z3Type(object): @abc.abstractmethod def to_z3(self, val, strict=False): - # type: (Any) -> z3.ExprRef + # type: (Any, bool) -> z3.ExprRef """Transforms a value from OpenStack in a Z3 value""" raise NotImplementedError diff --git a/doc/source/user/policy.rst b/doc/source/user/policy.rst index bc1533da9..4007e641d 100644 --- a/doc/source/user/policy.rst +++ b/doc/source/user/policy.rst @@ -503,12 +503,32 @@ Z3 imposes a different set of restrictions on the Datalog language. First it lifts the recursivity restriction of the internal engine and supports stratified negation. -But z3 policies do not support the set of builtins of regular policies. Some -builtins will be supported in the future. +But z3 policies do not support the set of builtins of regular policies. +Supported builtins are: + +============== ======================================================= +Builtins Description +============== ======================================================= +lt(x, y) True if x < y +lteq(x, y) True if x <= y +equal(x, y) True if x == y +gt(x, y) True if x > y +gteq(x, y) True if x >= y +plus(x, y, z) z = x + y +minus(x, y, z) z = x - y +mul(x, y, z) z = x * y +or(x, y, z) z = x | y (bitwise or) +and(x, y, z) z = x & y (bitwise and) +bnot(x, y) y = ~x (bitwise not) +============== ======================================================= + +As for regular theories, all builtins are referenced in rules using the +prefix *builtin:*. Z3 is a typed Datalog engine. Although the type-checking engine silently infer types, it may refuse some policies that mix columns of different -types. +types. Internally Z3 codes everything as bitvectors and the integer type +is in fact a 32 bitvector type. 3. Multiple Policies ==================== diff --git a/releasenotes/notes/z3-builtins-461251858ea2bf88.yaml b/releasenotes/notes/z3-builtins-461251858ea2bf88.yaml new file mode 100644 index 000000000..341c7e805 --- /dev/null +++ b/releasenotes/notes/z3-builtins-461251858ea2bf88.yaml @@ -0,0 +1,8 @@ +--- +prelude: > +features: + - | + Built-ins have been added to z3 policies. Available builtins cover + comparisons (equal, less than, greater than), basic arithmetic (plus, + minus, mul) and bitwise operations (and, or, not on bitvectors). +