Merge "Z3 engine as an alternative Datalog engine"

This commit is contained in:
Zuul 2018-07-26 22:06:56 +00:00 committed by Gerrit Code Review
commit 5c43a61a02
19 changed files with 2123 additions and 21 deletions

View File

@ -32,6 +32,7 @@ ACTION_POLICY_TYPE = 'action'
MATERIALIZED_POLICY_TYPE = 'materialized'
DELTA_POLICY_TYPE = 'delta'
DATASOURCE_POLICY_TYPE = 'datasource'
Z3_POLICY_TYPE = 'z3'
class Tracer(object):

View File

@ -30,24 +30,10 @@ from congress import exception
LOG = logging.getLogger(__name__)
class NonrecursiveRuleTheory(topdown.TopDownTheory):
"""A non-recursive collection of Rules."""
def __init__(self, name=None, abbr=None,
schema=None, theories=None, desc=None, owner=None):
super(NonrecursiveRuleTheory, self).__init__(
name=name, abbr=abbr, theories=theories, schema=schema,
desc=desc, owner=owner)
# dictionary from table name to list of rules with that table in head
self.rules = ruleset.RuleSet()
self.kind = base.NONRECURSIVE_POLICY_TYPE
if schema is None:
self.schema = compile.Schema()
class RuleHandlingMixin(object):
# External Interface
# SELECT implemented by TopDownTheory
def initialize_tables(self, tablenames, facts):
"""Event handler for (re)initializing a collection of tables
@ -226,6 +212,7 @@ class NonrecursiveRuleTheory(topdown.TopDownTheory):
def _insert_actual(self, rule):
"""Insert RULE and return True if there was a change."""
self.dirty = True
if compile.is_atom(rule):
rule = compile.Rule(rule, [], rule.location)
self.log(rule.head.table.table, "Insert: %s", repr(rule))
@ -233,6 +220,7 @@ class NonrecursiveRuleTheory(topdown.TopDownTheory):
def _delete_actual(self, rule):
"""Delete RULE and return True if there was a change."""
self.dirty = True
if compile.is_atom(rule):
rule = compile.Rule(rule, [], rule.location)
self.log(rule.head.table.table, "Delete: %s", rule)
@ -247,6 +235,26 @@ class NonrecursiveRuleTheory(topdown.TopDownTheory):
results.extend(self.rules.get_rules(table))
return results
class NonrecursiveRuleTheory(RuleHandlingMixin, topdown.TopDownTheory):
"""A non-recursive collection of Rules."""
def __init__(self, name=None, abbr=None,
schema=None, theories=None, desc=None, owner=None):
super(NonrecursiveRuleTheory, self).__init__(
name=name, abbr=abbr, theories=theories, schema=schema,
desc=desc, owner=owner)
# dictionary from table name to list of rules with that table in head
self.rules = ruleset.RuleSet()
self.kind = base.NONRECURSIVE_POLICY_TYPE
if schema is None:
self.schema = compile.Schema()
# Indicates that a rule was added/removed
# Used by the compiler to know if a theory should be recompiled.
self.dirty = False
# SELECT implemented by TopDownTheory
def head_index(self, table, match_literal=None):
"""Return head index.

View File

@ -56,7 +56,7 @@ def validate_policy_item(item):
"kind": {
"title": "Policy kind",
"type": "string",
"enum": ["database", "nonrecursive", "action", "materialized",
"enum": ["database", "nonrecursive", "action", "z3", "materialized",
"delta", "datasource"]
},
"abbreviation": {

View File

@ -41,6 +41,8 @@ from congress.dse2 import data_service
from congress import exception
from congress.synchronizer import policy_rule_synchronizer
from congress import utils
from congress.z3 import z3theory
from congress.z3 import z3types
LOG = logging.getLogger(__name__)
@ -622,6 +624,12 @@ class Runtime (object):
PolicyClass = materialized.MaterializedViewTheory
elif kind == base.DATASOURCE_POLICY_TYPE:
PolicyClass = nonrecursive.DatasourcePolicyTheory
elif kind == base.Z3_POLICY_TYPE:
if z3types.Z3_AVAILABLE:
PolicyClass = z3theory.Z3Theory
else:
raise exception.PolicyException(
"Z3 not available. Please install it")
else:
raise exception.PolicyException(
"Unknown kind of policy: %s" % kind)
@ -685,14 +693,17 @@ class Runtime (object):
if not permitted:
# This shouldn't happen
msg = ";".join(str(x) for x in errs)
LOG.exception("%s:: failed to empty theory %s: %s",
self.name, name, msg)
LOG.exception("agnostic:: failed to empty theory %s: %s",
name_or_id, msg)
raise exception.PolicyException("Policy %s could not be deleted "
"since rules could not all be "
"deleted: %s" % (name, msg))
# delete disabled rules
self.disabled_events = [event for event in self.disabled_events
if event.target != name]
# explicit destructor could be part of the generic Theory interface.
if isinstance(self.theory.get(name, None), z3theory.Z3Theory):
self.theory[name].drop()
# actually delete the theory
del self.theory[name]
@ -1217,7 +1228,10 @@ class Runtime (object):
graph_changes = self.global_dependency_graph.formula_update(
events, include_atoms=False)
if graph_changes:
if self.global_dependency_graph.has_cycle():
if (self.global_dependency_graph.has_cycle() and
z3theory.irreducible_cycle(
self.theory,
self.global_dependency_graph.cycles())):
# TODO(thinrichs): include path
errors.append(exception.PolicyException(
"Rules are recursive"))

View File

View File

@ -0,0 +1,234 @@
# Copyright 2018 Orange
#
# 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.
"""Unit tests for typechecker"""
import six
from congress import data_types
from congress.datalog import base as datalog
from congress.datalog import compile as ast
from congress.datalog import nonrecursive
from congress.datalog import ruleset
from congress.tests import base
from congress.z3 import typechecker
def mkc(typ, nullable):
return {'type': typ, 'nullable': nullable}
class TestMinTypes(base.TestCase):
def setUp(self):
try:
data_types.TypesRegistry.type_class('Enum')
except KeyError:
typ = data_types.create_congress_enum_type(
'Enum', ['a', 'b', 'c'], data_types.Str)
data_types.TypesRegistry.register(typ)
super(TestMinTypes, self).setUp()
def test_not_convertible(self):
self.assertIsNone(typechecker.min_type('Str', 'Int', False))
def test_convertible(self):
self.assertEqual('Enum', typechecker.min_type('Str', 'Enum', False))
self.assertEqual('Enum', typechecker.min_type('Enum', 'Str', False))
def test_constrained(self):
self.assertEqual('Enum', typechecker.min_type('Str', 'Enum', True))
self.assertIsNone(typechecker.min_type('Enum', 'Str', True))
class TestCellPrimitives(base.TestCase):
def test_constrain1(self):
tc = typechecker.Typechecker([], [])
cell = mkc(None, False)
tc.work = False
tc.constrain_type(cell, 'Str')
self.assertEqual('Str', cell['type'])
self.assertIs(True, tc.work)
def test_constrain2(self):
tc = typechecker.Typechecker([], [])
cell = mkc('Int', False)
tc.work = False
tc.constrain_type(cell, 'Str')
self.assertEqual('Scalar', cell['type'])
self.assertIs(True, tc.work)
def test_constrain3(self):
tc = typechecker.Typechecker([], [])
cell = mkc('Str', False)
tc.work = False
tc.constrain_type(cell, 'Str')
self.assertEqual('Str', cell['type'])
self.assertIs(False, tc.work)
def test_nullable1(self):
tc = typechecker.Typechecker([], [])
cell = mkc('Str', False)
tc.work = False
tc.set_nullable(cell)
self.assertIs(True, cell['nullable'])
self.assertIs(True, tc.work)
def test_nullable2(self):
tc = typechecker.Typechecker([], [])
cell = mkc('Str', True)
tc.work = False
tc.set_nullable(cell)
self.assertIs(True, cell['nullable'])
self.assertIs(False, tc.work)
def test_type_cells1(self):
tc = typechecker.Typechecker([], [])
cell1, cell2 = mkc('Str', True), mkc(None, False)
self.assertIsNone(tc.type_cells(cell1, cell2, False))
self.assertEqual(mkc('Str', True), cell1)
self.assertEqual(mkc('Str', True), cell2)
self.assertIs(True, tc.work)
def test_type_cells2(self):
tc = typechecker.Typechecker([], [])
cell1, cell2 = mkc(None, False), mkc('Str', True)
self.assertIsNone(tc.type_cells(cell1, cell2, False))
self.assertEqual(mkc('Str', True), cell1)
self.assertEqual(mkc('Str', True), cell2)
self.assertIs(True, tc.work)
def test_type_cells3(self):
tc = typechecker.Typechecker([], [])
cell1, cell2 = mkc(None, False), mkc('Str', True)
self.assertIsNone(tc.type_cells(cell1, cell2, False))
self.assertEqual(mkc('Str', True), cell1)
self.assertEqual(mkc('Str', True), cell2)
self.assertIs(True, tc.work)
def test_type_cells4(self):
tc = typechecker.Typechecker([], [])
cell1, cell2 = mkc('Str', False), mkc('Str', False)
self.assertIsNone(tc.type_cells(cell1, cell2, False))
self.assertEqual(mkc('Str', False), cell1)
self.assertEqual(mkc('Str', False), cell2)
self.assertIs(False, tc.work)
cell1, cell2 = mkc('Str', True), mkc('Str', True)
self.assertIsNone(tc.type_cells(cell1, cell2, False))
cell1, cell2 = mkc(None, False), mkc(None, False)
self.assertIsNone(tc.type_cells(cell1, cell2, False))
self.assertIs(False, tc.work)
def test_type_cells5(self):
tc = typechecker.Typechecker([], [])
cell1, cell2 = mkc('Int', False), mkc('Str', True)
self.assertIsNotNone(tc.type_cells(cell1, cell2, False))
def test_type_constant(self):
tc = typechecker.Typechecker([], [])
def check(val, typ, nullable):
cell = mkc(None, False)
tc.type_constant(val, cell)
self.assertEqual(mkc(typ, nullable), cell)
check(1, 'Int', False)
check('aaa', 'Str', False)
check(True, 'Bool', False)
check(1.3, 'Float', False)
check(None, None, True)
check((1, 3), 'Scalar', False)
class MinTheory(nonrecursive.RuleHandlingMixin, datalog.Theory):
def __init__(self, name, theories):
super(MinTheory, self).__init__(name=name, theories=theories)
self.rules = ruleset.RuleSet()
self.schema = ast.Schema()
class TestTypeChecker(base.TestCase):
def setUp(self):
self.world = {}
t1 = MinTheory('t1', self.world)
t2 = MinTheory('t2', self.world)
self.world['t1'] = t1
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).')
for rule in self.rules:
t1.insert(rule)
for rule in ast.parse("f(3)."):
t2.insert(rule)
self.t1 = t1
self.t2 = t2
super(TestTypeChecker, self).setUp()
def test_reset(self):
tc = typechecker.Typechecker([self.t1], self.world)
tc.reset_types()
sch1 = self.t1.schema
for (_, cols) in six.iteritems(sch1.map):
for col in cols:
self.assertIs(False, col['nullable'])
self.assertIsNone(col['type'])
def test_reset_variables(self):
tc = typechecker.Typechecker([self.t1], self.world)
tc.reset_type_environment()
env = tc.type_env
self.assertEqual(4, 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_type_facts(self):
tc = typechecker.Typechecker([self.t1], self.world)
tc.reset_types()
tc.reset_type_environment()
tc.type_facts(self.t1)
cols1 = self.t1.schema.map['l']
self.assertEqual(1, len(cols1))
self.assertEqual('Int', cols1[0]['type'])
self.assertIs(False, cols1[0]['nullable'])
cols2 = self.t1.schema.map['m']
self.assertEqual(1, len(cols2))
self.assertEqual('Str', cols2[0]['type'])
self.assertIs(False, cols2[0]['nullable'])
def test_type_rule(self):
rule = self.rules[2]
tc = typechecker.Typechecker([self.t1], self.world)
tc.reset_types()
tc.reset_type_environment()
tc.type_facts(self.t1)
tc.type_rule(self.t1, rule)
self.assertEqual(mkc('Int', False), tc.type_env[rule.id]['x'])
self.assertEqual('Int', self.t1.schema.map['p'][0]['type'])
self.assertIs(True, tc.work)
def test_type_all(self):
tc = typechecker.Typechecker([self.t1], self.world)
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

View File

@ -0,0 +1,433 @@
# Copyright 2018 Orange
#
# 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.
"""Unit tests for z3theory"""
import mock
import six
from congress import data_types
from congress.datalog import compile as ast
from congress.datalog import topdown
from congress import exception
from congress.tests import base
from congress.tests.z3 import z3mock as z3
from congress.z3 import z3theory
from congress.z3 import z3types
def mockz3(f):
z3types.Z3_AVAILABLE = True
return (
mock.patch("congress.z3.z3types.z3", new=z3)
(mock.patch("congress.z3.z3theory.Z3OPT", new=z3)(f)))
class TestZ3Utilities(base.TestCase):
def test_irreducible_cycle(self):
t1 = mock.MagicMock(spec=z3theory.Z3Theory)
t2 = mock.MagicMock(spec=z3theory.Z3Theory)
t3 = mock.MagicMock(spec=topdown.TopDownTheory)
theories = {'t1': t1, 't2': t2, 't3': t3}
for name, th in six.iteritems(theories):
th.name = name
cycles = [['t1:p', 't2:q', 't1:r'], ['t1:p1', 't2:q2']]
r = z3theory.irreducible_cycle(theories, cycles)
self.assertIs(False, r)
cycles = [['t1:p', 't2:q', 't1:r'], ['t3:p1', 't2:q2']]
r = z3theory.irreducible_cycle(theories, cycles)
self.assertIs(True, r)
def test_congress_constant(self):
test_cases = [
(3, "INTEGER", 3), ("aa", "STRING", "aa"),
(4.3, "FLOAT", 4.3), ([], "STRING", "[]")]
for (val, typ, name) in test_cases:
obj = z3theory.congress_constant(val)
self.assertIsInstance(
obj, ast.ObjectConstant,
msg=('not a constant for %s' % (str(val))))
self.assertEqual(typ, obj.type)
self.assertEqual(name, obj.name)
def test_retrieve(self):
theory = mock.MagicMock(spec=topdown.TopDownTheory)
theory.name = 'test'
theory.schema = mock.MagicMock(spec=ast.Schema)
theory.schema.arity.return_value = 3
z3theory.retrieve(theory, 'table')
args = theory.select.call_args
query = args[0][0]
self.assertIsInstance(query, ast.Literal)
self.assertEqual('table', query.table.table)
self.assertEqual('test', query.table.service)
self.assertEqual(3, len(query.arguments))
self.assertIs(
True,
all(isinstance(arg, ast.Variable) for arg in query.arguments))
class TestZ3Theory(base.TestCase):
@mockz3
def setUp(self):
world = {}
self.theory = z3theory.Z3Theory('test', theories=world)
world['test'] = self.theory # invariant to maintain in agnostic
super(TestZ3Theory, self).setUp()
def test_init(self):
self.assertIsInstance(self.theory.schema, ast.Schema)
self.assertIsInstance(self.theory.z3context, z3theory.Z3Context)
context = z3theory.Z3Context.get_context()
self.assertIn('test', context.z3theories)
self.assertEqual(self.theory, context.z3theories['test'])
def test_select(self):
context = z3theory.Z3Context.get_context()
context.select = mock.MagicMock()
lit = ast.Literal(ast.Tablename('t'), [])
self.theory.select(lit)
context.select.assert_called_once_with(self.theory, lit, True)
def test_drop(self):
self.theory.drop()
context = z3theory.Z3Context.get_context()
self.assertNotIn('test', context.z3theories)
def test_arity(self):
lit = ast.Literal(ast.Tablename('t'),
[ast.Variable('x'), ast.Variable('x')])
self.theory.insert(lit)
self.assertEqual(2, self.theory.arity('t'))
def mkc(name, nullable=False):
return {'type': name, 'nullable': nullable}
class TestZ3Context(base.TestCase):
@mockz3
def test_registration(self):
context = z3theory.Z3Context()
theory = mock.MagicMock(z3theory.Z3Theory)
name = 'test'
world = {}
theory.name = name
theory.theories = world
world['foo'] = theory
context.register(theory)
self.assertIn(name, context.z3theories)
self.assertEqual(theory, context.z3theories[name])
self.assertEqual(world, context.theories)
context.drop(theory)
self.assertNotIn(name, context.z3theories)
@mockz3
def test_get_context(self):
self.assertIsInstance(
z3theory.Z3Context.get_context(), z3theory.Z3Context)
@mockz3
def test_declare_table(self):
"""Test single table declaration
Declare table declares the relation of a single table from its type
"""
context = z3theory.Z3Context()
name = 'test'
tbname = 'table'
world = {}
theory = z3theory.Z3Theory(name, theories=world)
theory.schema.map[tbname] = [mkc('Int'), mkc('Int')]
world[name] = theory
context.declare_table(theory, tbname)
# Only the mock as a _relations element and pylint is confused
rels = context.context._relations # pylint: disable=E1101
self.assertEqual(1, len(rels))
self.assertEqual(name + ':' + tbname, rels[0].name())
self.assertEqual(3, len(rels[0]._typs))
@mockz3
def test_declare_tables(self):
"""Test declaration of internal z3theories tables
Declare tables must iterate over all schemas and create relations
with the right arity and types
"""
context = z3theory.Z3Context()
world = {}
t1 = z3theory.Z3Theory('t1', theories=world)
t2 = z3theory.Z3Theory('t2', theories=world)
world['t1'] = t1
world['t2'] = t2
t1.schema.map['p'] = [mkc('Int')]
t1.schema.map['q'] = [mkc('Str'), mkc('Str')]
t2.schema.map['k'] = [mkc('Bool')]
context.register(t1)
context.register(t2)
context.declare_tables()
# Only the mock as a _relations element and pylint is confused
rels = context.context._relations # pylint: disable=E1101
self.assertEqual(3, len(rels))
self.assertIn('t1:q', context.relations)
self.assertEqual(2, len(context.relations['t1:p']._typs))
def init_three_theories(self):
context = z3theory.Z3Context()
world = {}
for name in ['t1', 't2', 't3']:
world[name] = z3theory.Z3Theory(name, theories=world)
t1, t2, t3 = world['t1'], world['t2'], world['t3']
context.register(t1)
context.register(t2)
# t3 is kept external
# Declare rules
for rule in ast.parse('p(x) :- t2:r(x), t3:s(x). q(x) :- p(x). p(4).'):
t1.insert(rule)
for rule in ast.parse('r(x) :- t1:p(x).'):
t2.insert(rule)
# typechecker
t1.schema.map['p'] = [mkc('Int')]
t1.schema.map['q'] = [mkc('Int')]
t2.schema.map['r'] = [mkc('Int')]
t3.schema.map['s'] = [mkc('Int')]
t3.schema.map['t'] = [mkc('Int')]
return context
@mockz3
def test_declare_external_tables(self):
"""Test declaration of internal z3theories tables
Declare tables must iterate over all schemas and create relations
with the right arity and types
"""
context = self.init_three_theories()
context.declare_external_tables()
# Only the mock as a _relations element and pylint is confused
rels = context.context._relations # pylint: disable=E1101
self.assertEqual(1, len(rels))
self.assertIn('t3:s', context.relations)
@mockz3
def test_compile_facts(self):
context = z3theory.Z3Context()
world = {}
t1 = z3theory.Z3Theory('t1', theories=world)
world['t1'] = t1
context.register(t1)
for rule in ast.parse('l(1,2). l(3,4). l(5,6).'):
t1.insert(rule)
t1.schema.map['l'] = [mkc('Int'), mkc('Int')]
context.declare_tables()
context.compile_facts(t1)
rules = context.context.get_rules()
self.assertEqual(3, len(rules))
self.assertIs(True, all(r.decl().name() == 't1:l' for r in rules))
self.assertEqual(
[[1, 2], [3, 4], [5, 6]],
[[c.as_long() for c in r.children()] for r in rules])
def init_one_rule(self):
context = z3theory.Z3Context()
world = {}
t1 = z3theory.Z3Theory('t1', theories=world)
world['t1'] = t1
context.register(t1)
rule = ast.parse('p(x) :- l(x,y), l(3,x).')[0]
t1.schema.map['l'] = [mkc('Int'), mkc('Int')]
t1.schema.map['p'] = [mkc('Int')]
context.declare_tables()
return (context, t1, rule)
def init_one_theory(self, prog):
context = z3theory.Z3Context()
world = {}
t1 = z3theory.Z3Theory('t1', theories=world)
world['t1'] = t1
context.register(t1)
for rule in ast.parse(prog):
t1.insert(rule)
return (context, t1)
@mockz3
def test_compile_atoms(self):
(context, t1, rule) = self.init_one_rule()
result = context.compile_atoms(t1, rule.head, rule.body)
self.assertEqual(3, len(result))
(vars, head, body) = result
self.assertEqual(2, len(vars))
# two variables
self.assertIs(
True, all(x.decl().kind() == z3.Z3_OP_UNINTERPRETED for x in vars))
# two literals in the body
self.assertEqual(2, len(body))
# Head literal is p
self.assertEqual('t1:p', head.decl().name())
# First body literal is l
self.assertEqual('t1:l', body[0].decl().name())
# First arg of second body literal is a compiled int constant
self.assertEqual(3, body[1].children()[0].as_long())
# Second arg of second body literal is a variable
self.assertEqual(z3.Z3_OP_UNINTERPRETED,
body[1].children()[1].decl().kind())
@mockz3
def test_compile_rule(self):
(context, t1, rule) = self.init_one_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())
self.assertEqual(
'and', result.children()[2].children()[0].decl().name())
@mockz3
def test_compile_query(self):
(context, t1, rule) = self.init_one_rule()
result = context.compile_query(t1, rule.head)
self.assertEqual('exists', result.decl().name())
self.assertEqual('t1:p', result.children()[1].decl().name())
@mockz3
def test_compile_theory(self):
context = self.init_three_theories()
context.declare_tables()
context.declare_external_tables()
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()
rules = context.context._rules # pylint: disable=E1101
rels = context.context._relations # pylint: disable=E1101
self.assertEqual(4, len(rules))
self.assertEqual(['t1:p', 't1:q', 't2:r', 't3:s'],
sorted([k.name() for k in rels]))
@staticmethod
def mk_z3_result(context):
sort = context.type_registry.get_type('Int')
def vec(x):
return z3.BitVecVal(x, sort)
x, y = z3.Const('x', sort), z3.Const('y', sort)
return z3.Or(z3.And(z3.Eq(x, vec(1)), z3.Eq(y, vec(2))),
z3.And(z3.Eq(x, vec(3)), z3.Eq(y, vec(4))))
@mock.patch('congress.z3.z3types.z3.Fixedpoint.get_answer')
@mockz3
def test_eval(self, mock_get_answer):
(context, t1) = self.init_one_theory('l(1,2). l(3,4).')
expr = self.mk_z3_result(context)
mock_get_answer.return_value = expr
query = ast.parse('l(x,y)')[0]
result = context.eval(t1, query)
self.assertEqual(2, len(result[1]))
self.assertEqual(2, len(result[2]))
self.assertIs(True, all(len(row) == 2 for row in result[0]))
@mock.patch('congress.z3.z3types.z3.Fixedpoint.get_answer')
@mockz3
def test_select(self, mock_get_answer):
(context, t1) = self.init_one_theory('l(1,2). l(3,4).')
expr = self.mk_z3_result(context)
mock_get_answer.return_value = expr
query = ast.parse('l(x,y)')[0]
result = context.select(t1, query, True)
self.assertEqual(ast.parse('l(1,2). l(3,4).'), result)
@mockz3
def test_inject(self):
theory = mock.MagicMock(spec=topdown.TopDownTheory)
world = {'t': theory}
theory.name = 't'
theory.schema = ast.Schema()
theory.schema.map['l'] = [mkc('Int'), mkc('Int')]
theory.select.return_value = ast.parse('l(1,2). l(3,4). l(5,6)')
context = z3theory.Z3Context()
# An external theory world
context.theories = world
# inject the declaration of external relation without rules
param_types = [
context.type_registry.get_type(typ)
for typ in ['Int', 'Int', 'Bool']]
relation = z3.Function('t:l', *param_types)
context.context.register_relation(relation)
context.relations['t:l'] = relation
# the test
context.inject('t', 'l')
rules = context.context._rules # pylint: disable=E1101
self.assertIs(True, all(r.decl().name() == 't:l' for r in rules))
self.assertEqual(
[[1, 2], [3, 4], [5, 6]],
sorted([[c.as_long() for c in r.children()] for r in rules]))
class TestTypeConstraints(base.TestCase):
@mockz3
def setUp(self):
try:
data_types.TypesRegistry.type_class('Small')
except KeyError:
typ = data_types.create_congress_enum_type(
'Small', ['a', 'b'], data_types.Str)
data_types.TypesRegistry.register(typ)
super(TestTypeConstraints, self).setUp()
@staticmethod
def init_two_theories(prog):
context = z3theory.Z3Context()
world = {}
for name in ['t1', 't2']:
world[name] = z3theory.Z3Theory(name, theories=world)
t1, t2 = world['t1'], world['t2']
context.register(t1)
# t2 is kept external
# Declare rules
for rule in ast.parse(prog):
t1.insert(rule)
# typechecker
t2.schema.map['p'] = [mkc('Small')]
t2.schema.map['q'] = [mkc('Str')]
return context
@mockz3
def test_compile_all_ok(self):
context = self.init_two_theories('p("a"). p(x) :- t2:p(x).')
context.typecheck()
context.compile_all()
rules = context.context._rules # pylint: disable=E1101
self.assertEqual(2, len(rules))
@mockz3
def test_compile_fails_constraints(self):
# Two external tables with different types: caught by typechecker.
context = self.init_two_theories('p(x) :- t2:p(x), t2:q(x).')
self.assertRaises(exception.PolicyRuntimeException, context.typecheck)
@mockz3
def test_compile_fails_values(self):
context = self.init_two_theories('p("c"). p(x) :- t2:p(x).')
# Type-check succeeds
context.typecheck()
# But we are caught when trying to convert 'c' as a 'Small' value
self.assertRaises(exception.PolicyRuntimeException,
context.compile_all)

View File

@ -0,0 +1,184 @@
# Copyright 2018 Orange
#
# 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.
"""Unit tests for z3types"""
import mock
from congress import data_types
from congress import exception
from congress.tests import base
from congress.tests.z3 import z3mock as z3
from congress.z3 import z3types
def mockz3(f):
z3types.Z3_AVAILABLE = True
return mock.patch("congress.z3.z3types.z3", new=z3)(f)
class TestBoolType(base.TestCase):
"""Z3 Boolean values"""
@mockz3
def setUp(self):
self.type = z3types.BoolType()
super(TestBoolType, self).setUp()
@mockz3
def test_to_z3(self):
self.assertEqual(z3.Z3_OP_TRUE, self.type.to_z3(True).decl().kind())
self.assertEqual(z3.Z3_OP_FALSE, self.type.to_z3(False).decl().kind())
@mockz3
def test_from_z3(self):
self.assertEqual(True, self.type.to_os(z3.BoolVal(True)))
self.assertEqual(False, self.type.to_os(z3.BoolVal(False)))
class TestStringType(base.TestCase):
"""Z3 String values"""
@mockz3
def setUp(self):
self.type = z3types.StringType('string', size=8)
super(TestStringType, self).setUp()
@mockz3
def test_to_z3(self):
x = self.type.to_z3('aaaa')
self.assertEqual(8, x.size())
# Do not try to use equality on Z3 values.
self.assertEqual(self.type.to_z3('aaaa').as_long(), x.as_long())
self.assertIs(False,
self.type.to_z3('bbbb').as_long() == x.as_long())
@mockz3
def test_from_z3(self):
self.assertEqual('aaaa', self.type.to_os(self.type.to_z3('aaaa')))
class TestIntType(base.TestCase):
"""Z3 Int values"""
@mockz3
def setUp(self):
self.type = z3types.IntType('int', size=16)
super(TestIntType, self).setUp()
@mockz3
def test_to_z3(self):
x = self.type.to_z3(342)
self.assertEqual(16, x.size())
self.assertEqual(342, x.as_long())
@mockz3
def test_from_z3(self):
self.assertEqual(421, self.type.to_os(self.type.to_z3(421)))
class TestZ3TypeRegistry(base.TestCase):
"""Other Z3Types Unit tests"""
def setUp(self):
try:
data_types.TypesRegistry.type_class('Foo')
except KeyError:
typ = data_types.create_congress_enum_type(
'Foo', ['a', 'b'], data_types.Str)
data_types.TypesRegistry.register(typ)
super(TestZ3TypeRegistry, self).setUp()
@mockz3
def test_get_type(self):
registry = z3types.TypeRegistry()
t = registry.get_type('Bool')
self.assertIs(True, isinstance(t, z3.BoolSort))
t = registry.get_type('Foo')
self.assertIs(True, isinstance(t, z3.BitVecSort))
@mockz3
def test_get_translator(self):
registry = z3types.TypeRegistry()
t = registry.get_translator('Bool')
self.assertIs(True, isinstance(t, z3types.BoolType))
t = registry.get_translator('Foo')
self.assertIs(True, isinstance(t, z3types.FiniteType))
@mockz3
def test_register(self):
registry = z3types.TypeRegistry()
test_type = mock.MagicMock()
test_type.name = 'Bar'
registry.register(test_type)
self.assertEqual(test_type, registry.get_translator('Bar'))
@mockz3
def test_reset(self):
registry = z3types.TypeRegistry()
test_type = mock.MagicMock()
test_type.name = 'Bar'
registry.register(test_type)
registry.reset()
test_type.reset.assert_called_once_with()
class TestZ3ToArray(base.TestCase):
@staticmethod
def project(z3res):
return [[x.as_long() for x in vec] for vec in z3res]
@mockz3
def test_sat(self):
self.assertIs(True, z3types.z3_to_array(z3.BoolVal(True)))
self.assertIs(False, z3types.z3_to_array(z3.BoolVal(False)))
@mockz3
def test_simple(self):
s = z3.BitVecSort(10)
def vec(x):
return z3.BitVecVal(x, s)
x, y = z3.Const('x', s), z3.Const('y', s)
expr = z3.Eq(x, vec(1))
self.assertEqual([[1]], self.project(z3types.z3_to_array(expr)))
expr = z3.And(z3.Eq(x, vec(1)), z3.Eq(y, vec(2)))
self.assertEqual([[1, 2]], self.project(z3types.z3_to_array(expr)))
@mockz3
def test_two_dims(self):
s = z3.BitVecSort(10)
def vec(x):
return z3.BitVecVal(x, s)
x, y = z3.Const('x', s), z3.Const('y', s)
expr = z3.Or(z3.Eq(x, vec(1)), z3.Eq(x, vec(2)))
self.assertEqual([[1], [2]], self.project(z3types.z3_to_array(expr)))
expr = z3.Or(z3.And(z3.Eq(x, vec(1)), z3.Eq(y, vec(2))),
z3.And(z3.Eq(x, vec(3)), z3.Eq(y, vec(4))))
self.assertEqual([[1, 2], [3, 4]],
self.project(z3types.z3_to_array(expr)))
@mockz3
def test_fails(self):
s = z3.BitVecSort(10)
x = z3.Const('x', s)
expr = x
self.assertRaises(exception.PolicyRuntimeException,
z3types.z3_to_array, expr)
expr = z3.Or(x, x)
self.assertRaises(exception.PolicyRuntimeException,
z3types.z3_to_array, expr)

181
congress/tests/z3/z3mock.py Normal file
View File

@ -0,0 +1,181 @@
# Copyright 2018 Orange
#
# 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.
"""A Mock of Z3"""
Z3_OP_OR = 262
Z3_OP_AND = 261
Z3_OP_EQ = 258
Z3_OP_FALSE = 257
Z3_OP_TRUE = 256
Z3_OP_NOT = 265
Z3_OP_IMPLIES = 266
Z3_OP_BNUM = 1024
Z3_OP_UNINTERPRETED = 2354
class BoolSort(object):
def __repr__(self):
return 'bool'
class BitVecSort(object):
def __init__(self, size):
self._size = size
def size(self):
return self._size
def __repr__(self):
return 'BV({})'.format(self._size)
class FuncDeclRef(object):
def __init__(self, name, kind, typs=None):
self._name = name
self._kind = kind
self._typs = [] if typs is None else typs
def name(self):
return self._name
def kind(self):
return self._kind
def __eq__(self, x):
return (isinstance(x, self.__class__) and x._name == self._name and
x._kind == self._kind)
def __call__(self, *args):
return ExprRef(self, args)
def __repr__(self):
return (self._name if self._typs == []
else self._name + repr(self._typs))
class ExprRef(object):
def __init__(self, decl, args):
self._decl = decl
self.args = args
def decl(self):
return self._decl
def children(self):
return self.args
def __eq__(self, v):
return ExprRef(FuncDeclRef('=', Z3_OP_EQ), [self, v])
def __repr__(self):
return repr(self._decl) + repr(self.args)
class BitVecRef(ExprRef):
def __init__(self, decl, val, sort):
super(BitVecRef, self).__init__(decl, [])
self.val = val
self.sort = sort
def as_long(self):
return self.val
def size(self):
return self.sort.size()
def __repr__(self):
return "bv({})".format(self.val)
def BitVecVal(v, s):
return BitVecRef(FuncDeclRef('bv', Z3_OP_BNUM), v, s)
class BoolRef(ExprRef):
pass
def BoolVal(val):
return BoolRef(FuncDeclRef('true' if val else 'false',
Z3_OP_TRUE if val else Z3_OP_FALSE),
[])
def And(*args):
return BoolRef(FuncDeclRef('and', Z3_OP_AND), args)
def Or(*args):
return BoolRef(FuncDeclRef('or', Z3_OP_OR), args)
def Not(arg):
return BoolRef(FuncDeclRef('not', Z3_OP_NOT), [arg])
def Eq(arg1, arg2):
return BoolRef(FuncDeclRef('=', Z3_OP_EQ), [arg1, arg2])
def Implies(a, b):
return BoolRef(FuncDeclRef("=>", Z3_OP_IMPLIES), [a, b])
def ForAll(l, t):
return BoolRef(FuncDeclRef("forall", 0), l + [t])
def Exists(l, t):
return BoolRef(FuncDeclRef("exists", 0), l + [t])
def Const(x, sort):
return ExprRef(FuncDeclRef(x, Z3_OP_UNINTERPRETED, typs=[sort]), [])
def Function(f, *args):
return FuncDeclRef(f, Z3_OP_UNINTERPRETED, typs=args)
class Fixedpoint(object):
def __init__(self):
self._relations = []
self._rules = []
self._options = {}
def set(self, **kwargs):
self._options = kwargs
def register_relation(self, r):
self._relations.append(r)
def fact(self, f):
self._rules.append(f)
def rule(self, r):
self._rules.append(r)
def query(self, q):
pass
@staticmethod
def get_answer():
return BoolVal(True)
def get_rules(self):
return self._rules

0
congress/z3/__init__.py Normal file
View File

275
congress/z3/typechecker.py Normal file
View File

@ -0,0 +1,275 @@
# 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.
#
"""A static Datalog typechecker.
It is mandatory for Z3, but should be usable by the standard engine.
Everything should be typable as we can always assign CongressStr as
a catch-all type.
The typechecker works as follows:
* Types are stored in theories schema.
* First we reset all types to bottom in theories that we want to type-check.
The type-checker must not change the types in other theories.
The bottom type is None with nullability set to False.
It must be set explicitly because otherwise the default type is scalar, True
which corresponds to the top type in the type hierarchy.
* We prepare a type environment for each rule (identified by rule.id).that
contains the type of the variables (again a cell initialized to the bottom
type)
* First we type facts. Then we type rules iteratively.
A work phase types all the rules in the theories. Typing a rule means
propagating constraints in atoms. head and body atoms are treated with
the same algorithm.
* We request types to be the same when we solve a constraint or to be in
direct subtype relation. In that case we take the most precise type.
The reason for this is that we do not precisely constrain constants in
programs. Their type will be forced by the constraints from external tables.
Verification will occur when we translate the value to Z3.
* Types from external tables cannot be constrained. If the type of an
external table should be changed, typing fails.
* built-ins support will be added in the future. It is the only tricky point
as we usually need polymorphism for equalities, tests, some numeric
operations that can operate on various size of integers.
* convergence: there is a finite number of type cells (one per column for
tables and one per variable for rules). We iterate only if the type of
at least one type cell has been made more precise. There are only finite
ascending chains of types if the type hierarchy is well founded (and it is
ultimately based on python inheritance hierarchy which is well-founded).
"""
from oslo_log import log as logging
import six
from congress import data_types
from congress.datalog import compile as ast
from congress import exception
MYPY = False
# pylint: disable = ungrouped-imports
if MYPY:
# pylint: disable = unused-import
from mypy_extensions import TypedDict # noqa
from typing import Any, Union, List, Dict, Optional # noqa
from congress.datalog import base # noqa
CELLTYPE = TypedDict(
'CELLTYPE', {'nullable': bool, 'type': Optional[str]})
LOG = logging.getLogger(__name__)
def min_type(name1, name2, strict):
# type: (str, str, boolean) -> 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
gives back None. strict implies that the second type cannot be
constrained. Usually because it is defined in an external table.
"""
typ1 = data_types.TypesRegistry.type_class(name1)
typ2 = data_types.TypesRegistry.type_class(name2)
if typ2.least_ancestor([typ1]) is not None:
return name2
if not strict and typ1.least_ancestor([typ2]) is not None:
return name1
return None
class Typechecker(object):
"""Typechecks a set of theories"""
def __init__(self, theories, world):
# type: (List[base.Theory], Dict[str, base.Theory]) -> None
self.world = world
self.theories = theories
self.theorynames = set(th.name for th in theories)
self.work = False
self.once = False
self.type_env = {} # type: Dict[str, Dict[str, CELLTYPE]]
def constrain_type(self, cell, typ):
# type: (CELLTYPE, str) -> None
"""Constrains the type set in a type cell"""
if cell['type'] is None:
cell['type'] = typ
self.work = True
else:
old_typ = cell['type']
if typ != old_typ:
cell['type'] = 'Scalar'
self.work = True
def set_nullable(self, cell):
# type: (CELLTYPE) -> None
"""Force type to be nullable"""
if not cell['nullable']:
cell['nullable'] = True
self.work = True
def type_cells(self, cell1, cell2, strict):
# type: (CELLTYPE, Union[str, CELLTYPE]) -> Optional[str]
"""Propagates type constraints between two type cells
Updates work if a change has been made.
:param cell1: type cell to constrain
:param cell2: type cell to constrain
:param strict: boolean, true if cell2 is from an external table and
cannot be changed.
:return: None if ok, the text of an error otherwise.
"""
if isinstance(cell2, six.string_types):
# Just fake the cells. Occurs for a table from a nonrecursive
# theory.
cell2 = {'type': 'Scalar', 'nullable': True}
if (cell1['nullable'] and not cell2.get('nullable', True)
and not strict):
cell2['nullable'] = True
self.work = True
if cell2.get('nullable', True) and not cell1['nullable']:
cell1['nullable'] = True
self.work = True
typ1 = cell1['type']
typ2 = cell2['type']
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)
# else: two unresolved constraints, we do nothing
return None
def type_constant(self, value, column):
# type: (Any, CELLTYPE) -> None
"""Types a constant and set the constraint"""
if value is None:
self.set_nullable(column)
elif isinstance(value, six.string_types):
self.constrain_type(column, 'Str')
elif isinstance(value, bool):
self.constrain_type(column, 'Bool')
elif isinstance(value, int):
self.constrain_type(column, 'Int')
elif isinstance(value, float):
self.constrain_type(column, 'Float')
else:
self.constrain_type(column, 'Scalar')
def reset_type_environment(self):
"""Reset the type environment for all variables in rules"""
self.type_env = {
rule.id: {
variable.name: {'type': None, 'nullable': False}
for variable in rule.variables()
}
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"""
def refresh_item(elt):
"""Refresh the type of a table's column"""
elt = {'name': elt} if isinstance(elt, six.string_types) else elt
elt['type'] = None
elt['nullable'] = False
return elt
for theory in self.theories:
theory.schema.map = {
k: [refresh_item(e) for e in row]
for (k, row) in six.iteritems(theory.schema.map)}
def type_facts(self, theory):
# type: (base.Theory) -> None
"""Types the facts taking the best plausible type from arguments"""
for (tablename, facts) in six.iteritems(theory.rules.facts):
type_row = theory.schema.map[tablename]
for fact in facts:
for (value, typ) in six.moves.zip(fact, type_row):
self.type_constant(value, typ)
def type_rule(self, theory, rule):
# type: (base.Theory, ast.Rule) -> None
"""One type iteration over a single rule"""
LOG.debug("Type rule %s", rule.id)
var_types = self.type_env[rule.id]
def type_atom(atom):
# type: (ast.Literal) -> 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]
for (arg, typ_col) in six.moves.zip(atom.arguments, tbl_schema):
if isinstance(arg, ast.Variable):
typ_var = var_types[arg.name]
err = self.type_cells(typ_var, typ_col, strict)
if err is not None:
raise exception.PolicyRuntimeException(
("Type error while typing variable '{}' "
"in {} in rule {}: {}").format(
arg.name, atom, rule.id, err)
)
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)
def type_all(self):
"""Iterative typechecker"""
self.reset_types()
self.reset_type_environment()
for theory in self.theories:
self.type_facts(theory)
self.work = True
self.once = True
while self.work:
LOG.debug("*** Z3 Type iteration")
self.work = False
for theory in self.theories:
for ruleset in theory.rules.rules.values():
for rule in ruleset:
self.type_rule(theory, rule)
self.once = False

446
congress/z3/z3theory.py Normal file
View File

@ -0,0 +1,446 @@
# 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.
#
# Conflict with flake8
# pylint: disable = bad-continuation
"""A theory that contains rules that must be treated by Z3."""
import time
import logging
import six
from congress.datalog import base
from congress.datalog import compile as ast
from congress.datalog import nonrecursive
from congress.datalog import ruleset
from congress.datalog import unify
from congress import exception
from congress.z3 import typechecker
from congress.z3 import z3types
# pylint: disable = ungrouped-imports
MYPY = False
if MYPY:
# pylint: disable = unused-import
from congress.datalog import topdown # noqa
from typing import Dict, Callable, Union, List, Any, Tuple # noqa
import z3 # noqa
Z3_RESULT = Tuple[Union[bool, List[List[z3.ExprRef]]],
List[ast.Variable],
List[z3types.Z3Type]]
LOG = logging.getLogger(__name__)
Z3_ENGINE_OPTIONS = {'engine': 'datalog'}
Z3OPT = z3types.z3
INTER_COMPILE_DELAY = 60.0
def irreducible_cycle(theories, cycles):
# type: (Dict[str, base.Theory], List[List[str]]) -> bool
"""Check that there is a true cycle not through Z3 theory
A cycle is irreducible if it contains at least one element which is not a
Z3Theory for which recursion is allowed. Cycles are represented by lists of
qualified table names.
"""
acceptables = [
th.name
for th in six.itervalues(theories)
if isinstance(th, Z3Theory)]
return any(fullname[:fullname.index(':')] not in acceptables
for cycle in cycles for fullname in cycle)
# TODO(pcregut): Object constants should evolve to use the type system
# rather than custom types.
def congress_constant(val):
"""Creates an object constant from a value using its type"""
if isinstance(val, six.string_types):
typ = ast.ObjectConstant.STRING
elif isinstance(val, int):
typ = ast.ObjectConstant.INTEGER
elif isinstance(val, float):
typ = ast.ObjectConstant.FLOAT
else:
val = str(val)
typ = ast.ObjectConstant.STRING
return ast.ObjectConstant(val, typ)
def retrieve(theory, tablename):
# type: (topdown.TopDownTheory, str) -> List[ast.Literal]
"""Retrieves all the values of an external table.
Performs a select on the theory with a query computed from the schema
of the table.
"""
arity = theory.schema.arity(tablename)
table = ast.Tablename(tablename, theory.name)
args = [ast.Variable('X' + str(i)) for i in range(arity)]
query = ast.Literal(table, args)
return theory.select(query)
class Z3Theory(nonrecursive.RuleHandlingMixin, base.Theory):
"""Theory for Z3 engine
Z3Theory is a datalog theory interpreted by the Z3 engine instead of
the usual congress internal engine.
"""
def __init__(self, name=None, abbr=None,
schema=None, theories=None, desc=None, owner=None):
super(Z3Theory, self).__init__(
name=name, abbr=abbr, theories=theories,
schema=ast.Schema() if schema is None else schema,
desc=desc, owner=owner)
LOG.info('z3theory: create %s', name)
self.kind = base.Z3_POLICY_TYPE
self.rules = ruleset.RuleSet()
self.dirty = False
self.z3context = None
Z3Context.get_context().register(self)
def select(self, query, find_all=True):
"""Performs a query"""
return self.z3context.select(self, query, find_all)
def arity(self, tablename, modal=None):
"""Arity of a table"""
return self.schema.arity(tablename)
def drop(self):
"""To call when the theory is forgotten"""
self.z3context.drop(self)
def _top_down_eval(self,
context, # type: topdown.TopDownTheory.TopDownContext
caller # type: topdown.TopDownTheory.TopDownCaller
):
# type: (...) -> bool
"""Evaluation entry point for the non recursive engine
We must compute unifiers and clear off as soon as we can
giving back control to the theory context.
Returns true if we only need one binding and it has been found,
false otherwise.
"""
raw_lit = context.literals[context.literal_index]
query_lit = raw_lit.plug(context.binding)
answers, bvars, translators = self.z3context.eval(self, query_lit)
if isinstance(answers, bool):
if answers:
return (context.theory._top_down_finish(context, caller)
and not caller.find_all)
return False
for answer in answers:
changes = []
for (val, var, trans) in six.moves.zip(answer, bvars, translators):
chg = context.binding.add(var, trans.to_os(val), None)
changes.append(chg)
context.theory._top_down_finish(context, caller)
unify.undo_all(changes)
if not caller.find_all:
return True
return False
class Z3Context(object):
"""An instance of Z3 defined first by its execution context"""
_singleton = None
def __init__(self):
self.context = Z3OPT.Fixedpoint()
self.context.set(**Z3_ENGINE_OPTIONS)
self.z3theories = {} # type: Dict[str, Z3Theory]
self.relations = {} # type: Dict[str, z3.Function]
# back pointer on all theories extracted from registered theory.
self.theories = None # type: Dict[str, topdown.TopDownTheory]
self.externals = set() # type: Set[Tuple[str, str]]
self.type_registry = z3types.TypeRegistry()
self.last_compiled = 0
def register(self, theory):
# type: (Z3Theory) -> None
"""Registers a Z3 theory in the context"""
if self.theories is None:
self.theories = theory.theories
theory.z3context = self
self.z3theories[theory.name] = theory
def drop(self, theory):
# type: (Z3Theory) -> None
"""Unregister a Z3 theory from the context"""
del self.z3theories[theory.name]
@staticmethod
def get_context():
# type: () -> Z3Context
"""Gives back the unique instance of this class.
Users should not use the class constructor but this method.
"""
if Z3Context._singleton is None:
Z3Context._singleton = Z3Context()
return Z3Context._singleton
def eval(self,
theory, # type: Z3Theory
query # type: ast.Literal
):
# type: (...) -> Z3_RESULT
"""Solves a query and gives back a raw result
Result is in Z3 ast format with a translator
"""
theories_changed = any(t.dirty for t in self.z3theories.values())
# TODO(pcregut): replace either with an option or find something
# better for the refresh of datasources.
needs_refresh = time.time() - self.last_compiled > INTER_COMPILE_DELAY
if theories_changed or needs_refresh:
# 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()
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 = []
for arg, typ_arg in six.moves.zip(query.arguments, typ_args):
if isinstance(arg, ast.Variable) and arg not in variables:
translators.append(
self.type_registry.get_translator(str(typ_arg.type)))
variables.append(arg)
return (answer, variables, translators)
def select(self, theory, query, find_all):
# type: (Z3Theory, ast.Literal, bool) -> List[ast.Literal]
"""Query a theory"""
(answer, variables, trans) = self.eval(theory, query)
pattern = [
variables.index(arg) if isinstance(arg, ast.Variable) else arg
for arg in query.arguments]
def plug(row):
"""Plugs in found values in query litteral"""
args = [
(congress_constant(trans[arg].to_os(row[arg]))
if isinstance(arg, int) else arg)
for arg in pattern]
return ast.Literal(query.table, args)
if isinstance(answer, bool):
return [query] if answer else []
if find_all:
result = [plug(row) for row in answer]
else:
result = [plug(answer[0])]
return result
def declare_table(self, theory, tablename):
"""Declares a new table in Z3 context"""
fullname = theory.name + ':' + tablename
if fullname in self.relations:
return
typ_args = theory.schema.types(tablename)
param_types = [
self.type_registry.get_type(str(tArg.type))
for tArg in typ_args]
param_types.append(Z3OPT.BoolSort())
relation = Z3OPT.Function(fullname, *param_types)
self.context.register_relation(relation)
self.relations[fullname] = relation
def declare_tables(self):
"""Declares all tables defined in Z3 context"""
for theory in six.itervalues(self.z3theories):
for tablename in theory.schema.map.keys():
self.declare_table(theory, tablename)
def declare_external_tables(self):
"""Declares tables from other theories used in Z3 context"""
def declare_for_lit(lit):
"""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:
self.externals.add((service, table))
for theory in six.itervalues(self.z3theories):
for rules in six.itervalues(theory.rules.rules):
for rule in rules:
for lit in rule.body:
declare_for_lit(lit)
for (service, table) in self.externals:
self.declare_table(self.theories[service], table)
def compile_facts(self, theory):
# type: (Z3Theory) -> None
"""Compiles the facts of a theory in Z3 context"""
for tname, facts in six.iteritems(theory.rules.facts):
translators = [
self.type_registry.get_translator(str(arg_type.type))
for arg_type in theory.schema.types(tname)]
fullname = theory.name + ':' + tname
z3func = self.relations[fullname]
for fact in facts:
z3args = (tr.to_z3(v, strict=True)
for (v, tr) in six.moves.zip(fact, translators))
z3fact = z3func(*z3args)
self.context.fact(z3fact)
def compile_atoms(self,
theory, # type: Z3Theory
head, # type: ast.Literal
body # type: List[ast.Literal]
):
# type: (...) -> Tuple[z3.Const, z3.ExprRef, List[z3.ExprRef]]
"""Compile a list of atoms belonging to a single variable scope
As it is used mainly for rules, the head is distinguished.
"""
variables = {} # type: Dict[str, z3.Const]
def compile_expr(expr, translator):
"""Compiles an expression to Z3"""
if isinstance(expr, ast.Variable):
name = expr.name
if name in variables:
return variables[name]
var = Z3OPT.Const(name, translator.type())
variables[name] = var
return var
elif isinstance(expr, ast.ObjectConstant):
return translator.to_z3(expr.name)
else:
raise exception.PolicyException(
"Expr {} not handled by Z3".format(expr))
def compile_atom(literal):
"""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
try:
z3func = self.relations[fullname]
z3args = (compile_expr(arg, tr)
for (arg, tr) in six.moves.zip(literal.arguments,
translators))
z3lit = z3func(*z3args)
return (Z3OPT.Not(z3lit) if literal.negated
else z3lit)
except KeyError:
raise exception.PolicyException(
"Z3: Relation %s not registered" % fullname)
z3head = compile_atom(head)
z3body = [compile_atom(atom) for atom in body]
# We give back variables explicitely and do not rely on declare_var and
# abstract. Otherwise rules are cluttered with useless variables.
z3vars = [v for v in six.itervalues(variables)]
return (z3vars, z3head, z3body)
def compile_rule(self, theory, rule):
# type: (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)
term1 = (z3head if z3body == []
else Z3OPT.Implies(Z3OPT.And(*z3body), z3head))
term2 = term1 if z3vars == [] else Z3OPT.ForAll(z3vars, term1)
self.context.rule(term2)
def compile_query(self, theory, literal):
# type: (Z3Theory, ast.Literal) -> z3.ExprRef
"""compiles a query litteral
:param theory: theory used as the context of the query
:param litteral: the query
:returns: an existentially quantified litteral in Z3 format.
"""
z3vars, z3head, _ = self.compile_atoms(theory, literal, [])
return z3head if z3vars == [] else Z3OPT.Exists(z3vars, z3head)
def compile_theory(self, theory):
# type: (Z3Theory) -> None
"""Compiles all the rules of a theory
:param theory: theory to compile. Will be marked clean after.
"""
self.compile_facts(theory)
for rules in six.itervalues(theory.rules.rules):
for rule in rules:
self.compile_rule(theory, rule)
theory.dirty = False
def compile_all(self):
"""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.last_compiled = time.time()
def typecheck(self):
"""Typechecker for rules defined"""
typer = typechecker.Typechecker(
self.z3theories.values(), self.theories)
typer.type_all()
def inject(self, theoryname, tablename):
# type: (str, str) -> None
"""Inject the values of an external table in the Z3 Context.
Loops over the literal retrieved from a standard query.
"""
theory = self.theories[theoryname]
translators = [
self.type_registry.get_translator(str(arg_type.type))
for arg_type in theory.schema.types(tablename)]
fullname = theory.name + ':' + tablename
z3func = self.relations[fullname]
for lit in retrieve(theory, tablename):
z3args = (tr.to_z3(v.name, strict=True)
for (v, tr) in six.moves.zip(lit.arguments, translators))
z3fact = z3func(*z3args)
self.context.fact(z3fact)
def synchronize_external(self):
"""Synchronize all external tables"""
for (theoryname, tablename) in self.externals:
self.inject(theoryname, tablename)

239
congress/z3/z3types.py Normal file
View File

@ -0,0 +1,239 @@
# Copyright 2018 Orange
#
# 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.
"""Type translators between Congress and Z3."""
import abc
import six
from congress import data_types
from congress import exception
try:
import z3
Z3_AVAILABLE = True
except ImportError:
Z3_AVAILABLE = False
z3 = None
MYPY = False
if MYPY:
# pylint: disable = unused-import
from typing import Any, Union, List, Optional # noqa
Z3OPT = z3
@six.add_metaclass(abc.ABCMeta)
class Z3Type(object):
"""Translate Openstack values to Z3"""
def __init__(self, name, type_instance):
self.name = name
self.type_instance = type_instance
@abc.abstractmethod
def to_z3(self, val, strict=False):
# type: (Any) -> z3.ExprRef
"""Transforms a value from OpenStack in a Z3 value"""
raise NotImplementedError
@abc.abstractmethod
def to_os(self, val):
# type: (z3.ExprRef) -> Any
"""Transforms a value from Z3 back to python"""
raise NotImplementedError
def type(self):
# type: () -> z3.SortRef
"""Gives back the Z3 type"""
return self.type_instance
def reset(self):
"""Reset internal state of type transformer"""
pass
class BoolType(Z3Type):
"""Transcode boolean in Z3"""
def __init__(self):
super(BoolType, self).__init__(u'Bool', z3.BoolSort())
def to_z3(self, val, strict=False):
return z3.BoolVal(val)
def to_os(self, val):
return val.decl().kind() == z3.Z3_OP_TRUE
class StringType(Z3Type):
"""Transcode strings in Z3"""
def __init__(self, name, size=16):
super(StringType, self).__init__(name, z3.BitVecSort(size))
self.map = {}
self.back = {}
def to_z3(self, val, strict=False):
if val in self.map:
return self.map[val]
code = len(self.map)
bvect = z3.BitVecVal(code, self.type_instance)
self.map[val] = bvect
self.back[code] = val
return bvect
def to_os(self, val):
return self.back[val.as_long()]
def reset(self):
self.map = {}
self.back = {}
class FiniteType(StringType):
"""Z3 Coding for data_types with a finite number of elements
This is the counterpart to data_types.CongressTypeFiniteDomain.
"""
def __init__(self, name, domain):
size = (len(domain) + 1).bit_length()
super(FiniteType, self).__init__(name, size)
self.domain = domain
def to_z3(self, val, strict=False):
if val in self.map:
return self.map[val]
if val not in self.domain and val is not None:
if strict:
raise exception.PolicyRuntimeException(
"Z3 Finite type: {} is not a value of {}".format(
val, self.name))
else:
val = '__OTHER__'
code = len(self.map)
bvect = z3.BitVecVal(code, self.type_instance)
self.map[val] = bvect
self.back[code] = val
return bvect
class IntType(Z3Type):
"""Transcode numbers in Z3"""
def __init__(self, name, size=32):
super(IntType, self).__init__(name, z3.BitVecSort(size))
self.map = {}
self.back = {}
def to_z3(self, val, strict=False):
return z3.BitVecVal(val, self.type_instance)
def to_os(self, val):
return val.as_long()
class DummyType(Z3Type):
"""Dummy type when Z3 not available"""
def to_z3(self, val, strict=False):
pass
def to_os(self, val):
pass
class TypeRegistry(object):
"""A registry of Z3 types and their translators"""
def __init__(self):
self.type_dict = {} # type: Dict[Str, Z3Type]
self.top_type = DummyType('dummy', None)
self.init()
def register(self, typ):
# type: (Z3Type) -> None
"""Registers a new Z3 type"""
self.type_dict[typ.name] = typ
def init(self):
"""Initialize the registry"""
if Z3_AVAILABLE:
self.top_type = StringType(u'Scalar', 34)
for typ in [self.top_type, StringType(u'Str', 32),
IntType(u'Int', 32), BoolType(),
StringType('IPAddress', 32),
StringType('IPNetwork', 32),
StringType('UUID', 32)]:
self.register(typ)
def get_type(self, name):
# type: (str) -> z3.SortRef
"""Return a Z3 type given a type name"""
return self.get_translator(name).type()
def get_translator(self, name):
# type: (str) -> Z3Type
"""Return the translator for a given type name"""
trans = self.type_dict.get(name, None)
if trans is None:
try:
congress_type = data_types.TypesRegistry.type_class(name)
except KeyError:
raise exception.PolicyRuntimeException(
"Z3 typechecker: Unknown congress type {}".format(name))
if issubclass(congress_type, data_types.CongressTypeFiniteDomain):
trans = FiniteType(name, congress_type.DOMAIN)
self.register(trans)
else:
raise exception.PolicyRuntimeException(
"Z3 typechecker: cannot handle type {}".format(name))
return trans
def reset(self):
# type: () -> None
"""Reset the internal tables of all types"""
for typ in six.itervalues(self.type_dict):
typ.reset()
def z3_to_array(expr):
# type: (z3.BoolRef) -> Union[bool, List[List[Any]]]
"""Compiles back a Z3 result to a matrix of values"""
def extract(item):
"""Extract a row"""
kind = item.decl().kind()
if kind == z3.Z3_OP_AND:
return [x.children()[1] for x in item.children()]
elif kind == z3.Z3_OP_EQ:
return [item.children()[1]]
else:
raise exception.PolicyRuntimeException(
"Bad Z3 result not translatable {}: {}".format(expr, kind))
kind = expr.decl().kind()
if kind == z3.Z3_OP_OR:
return [extract(item) for item in expr.children()]
elif kind == z3.Z3_OP_AND:
return [[item.children()[1] for item in expr.children()]]
elif kind == z3.Z3_OP_EQ:
return [[expr.children()[1]]]
elif kind == z3.Z3_OP_FALSE:
return False
elif kind == z3.Z3_OP_TRUE:
return True
else:
raise exception.PolicyRuntimeException(
"Bad Z3 result not translatable {}: {}".format(expr, kind))

View File

@ -136,6 +136,37 @@ function _install_congress_dashboard {
_congress_setup_horizon
}
function _install_z3 {
if [[ $USE_Z3_RELEASE != None ]]; then
mkdir -p $CONGRESS_Z3_DIR
pushd $CONGRESS_Z3_DIR
z3rel="z3-${USE_Z3_RELEASE}"
z3file="${z3rel}-x64-${os_VENDOR,,}-${os_RELEASE}"
url="https://github.com/Z3Prover/z3/releases/download/${z3rel}/${z3file}.zip"
if [ ! -f "${z3file}.zip" ]; then
wget "${url}" "${z3file}.zip" || true
fi
if [ ! -f "${z3file}.zip" ]; then
echo "Failed to download z3 release ${USE_Z3_RELEASE} for ${os_VENDOR}-${os_RELEASE}"
exit 1
fi
unzip -o -f "${z3file}.zip" "${z3file}/bin/python/z3/*" "${z3file}/bin/libz3.so"
dist_dir=$($PYTHON -c "import site; print(site.getsitepackages()[0])")
sudo cp -r "${z3file}/bin/python/z3" "${dist_dir}"
sudo mkdir -p "${dist_dir}/z3/lib"
sudo cp "${z3file}/bin/libz3.so" "${dist_dir}/z3/lib/libz3.so"
popd
else
git_clone $CONGRESS_Z3_REPO $CONGRESS_Z3_DIR $CONGRESS_Z3_BRANCH
pushd $CONGRESS_Z3_DIR
${PYTHON} scripts/mk_make.py --python
cd build
make
sudo make install
popd
fi
}
# create_congress_cache_dir() - Part of the _congress_setup_keystone() process
function create_congress_cache_dir {
# Create cache dir
@ -189,6 +220,10 @@ function install_congress {
if is_service_enabled horizon; then
_install_congress_dashboard
fi
if [[ $ENABLE_CONGRESS_Z3 == "True" ]] ; then
_install_z3
fi
}
# Start running processes, including screen

View File

@ -9,6 +9,7 @@ CONGRESS_DIR=$DEST/congress
CONGRESSCLIENT_DIR=$DEST/python-congressclient
CONGRESS_AUTH_CACHE_DIR=${CONGRESS_AUTH_CACHE_DIR:-/var/cache/congress}
CONGRESSDASHBOARD_DIR=$DEST/congress-dashboard
CONGRESS_Z3_DIR=$DEST/z3
# Support entry points installation of console scripts
if [[ -d $CONGRESS_DIR/bin/congress-server ]]; then
@ -44,6 +45,11 @@ CONGRESS_LIBRARY_DIR=$CONGRESS_CONF_DIR/library
# File path to predefined policy and rules
CONGRESS_PREDEFINED_POLICY_FILE=${CONGRESS_PREDEFINED_POLICY_FILE:-""}
# Flag for enabling Z3 in Congress
ENABLE_CONGRESS_Z3=$(trueorfalse False ENABLE_CONGRESS_Z3)
# Flag to indicate that we prefer to use a precompiled release
USE_Z3_RELEASE=${USE_Z3_RELEASE:-None}
TEMPEST_DIR=$DEST/tempest
TEMPEST_CONFIG_DIR=${TEMPEST_CONFIG_DIR:-$TEMPEST_DIR/etc}
TEMPEST_CONFIG=$TEMPEST_CONFIG_DIR/tempest.conf
@ -63,6 +69,10 @@ CONGRESSCLIENT_BRANCH=${CONGRESSCLIENT_BRANCH:-master}
CONGRESSDASHBOARD_REPO=${CONGRESSDASHBOARD_REPO:-${GIT_BASE}/openstack/congress-dashboard.git}
CONGRESSDASHBOARD_BRANCH=${CONGRESSDASHBOARD_BRANCH:-master}
# z3
CONGRESS_Z3_REPO=${CONGRESS_Z3_REPO:-https://github.com/Z3Prover/z3.git}
CONGRESS_Z3_BRANCH=${CONGRESS_Z3_BRANCH:-master}
enable_service congress congress-api congress-engine congress-datasources
if [[ $ENABLE_CONGRESS_AGENT == "True" ]] ; then
enable_service congress-agent

View File

@ -59,6 +59,12 @@ The ``ENABLE_CONGRESS_AGENT`` variable in ``local.conf`` controls the
availability of the config datasource and its agent in devstack. Set it to
``False`` to disable it (default value is ``True``).
To enable the use of Z3 as an alternate Datalog engine, the
``ENABLE_CONGRESS_Z3`` variable must be set to ``True`` in ``local.conf``.
You can use a pre-compiled release if your OS supports it (Ubuntu, Debian)
by setting ``USE_Z3_RELEASE`` to the number of an existing release
(eg. ``4.7.1``).
Separate install
--------------------
Install the following software, if you haven't already.
@ -71,6 +77,9 @@ Install the following software, if you haven't already.
On Ubuntu: console apt-get install default-jre
On Federa: console yum install jre
* z3 (optional): if you want to use z3, install it following the
instructions at https://github.com/Z3Prover/z3
* Additionally
.. code-block:: console

View File

@ -34,10 +34,12 @@ and *action*. A policy has the following fields:
b) action,
c) database,
d) materialized
e) z3
The default is *nonrecursive* and unless you are writing action
The default is *nonrecursive*, *z3* let you use another Datalog engine
instead of the internal engine and unless you are writing action
descriptions for use with ``simulate`` you should always use the
default.
default or *z3*.
======= ============================ ================================

View File

@ -491,6 +491,24 @@ ip_in_network(x, y) 2 True if IP x belongs to network y
========================= ======= =============================================
2.5 Z3 Datalog
--------------
As explained in the next section, rules are grouped in sets called policies.
You can create a policy of kind *z3*. Its rules will be evaluated with
Microsoft z3 automatic prover which contains a Datalog engine instead of
Congress internal engine.
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.
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.
3. Multiple Policies
====================

View File

@ -0,0 +1,13 @@
---
prelude: >
features:
- |
new policies with kind *z3* that will be executed with Microsoft z3 state
of the art automatic theorem prover.
issues:
- |
Support of z3 is still preliminary. No built-ins are supported yet.
upgrade:
- |
z3 must be installed separately. This can be done by devstack if ``ENABLE_CONGRESS_Z3``
is set to true.