Merge "builtins for z3 theories"
This commit is contained in:
commit
2dc016d137
|
@ -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