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
This commit is contained in:
parent
75df78f5f2
commit
4b2b6fafbe
|
@ -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])
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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):
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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)),
|
||||
}
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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
|
||||
====================
|
||||
|
|
|
@ -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).
|
||||
|
Loading…
Reference in New Issue