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). +