From c5f633dfa2bca74bea6e28bf5dc418a4f58eb4a5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre=20Cr=C3=A9gut?= Date: Tue, 10 Jul 2018 09:36:08 +0200 Subject: [PATCH] Z3 engine as an alternative Datalog engine Basic structure for the integration of Z3 into Congress. Defines a Z3Theory as an alternative to nonrecursive theories. Defines a Z3Context for executing Z3Theory content. Z3 must be installed manually and is not in the requirements devstack will install Z3 if ENABLE_CONGRESS_Z3 is set. Limitations: * No built-ins * Typechecking does not support sub-typing (will be done later through built-ins). Partially-implements: blueprint alternative-engine-z3 Change-Id: I87ff439a3ed4a3e83c78c98add7d94275f716a01 --- congress/datalog/base.py | 1 + congress/datalog/nonrecursive.py | 38 +- congress/library_service/library_service.py | 2 +- congress/policy_engines/agnostic.py | 20 +- congress/tests/z3/__init__.py | 0 congress/tests/z3/test_typechecker.py | 234 +++++++++ congress/tests/z3/test_z3theory.py | 433 +++++++++++++++++ congress/tests/z3/test_z3types.py | 184 ++++++++ congress/tests/z3/z3mock.py | 181 +++++++ congress/z3/__init__.py | 0 congress/z3/typechecker.py | 275 +++++++++++ congress/z3/z3theory.py | 446 ++++++++++++++++++ congress/z3/z3types.py | 239 ++++++++++ devstack/plugin.sh | 35 ++ devstack/settings | 10 + doc/source/install/index.rst | 9 + doc/source/user/api.rst | 6 +- doc/source/user/policy.rst | 18 + .../notes/z3-engine-30c0d0fb93ea7a52.yaml | 13 + 19 files changed, 2123 insertions(+), 21 deletions(-) create mode 100644 congress/tests/z3/__init__.py create mode 100644 congress/tests/z3/test_typechecker.py create mode 100644 congress/tests/z3/test_z3theory.py create mode 100644 congress/tests/z3/test_z3types.py create mode 100644 congress/tests/z3/z3mock.py create mode 100644 congress/z3/__init__.py create mode 100644 congress/z3/typechecker.py create mode 100644 congress/z3/z3theory.py create mode 100644 congress/z3/z3types.py create mode 100644 releasenotes/notes/z3-engine-30c0d0fb93ea7a52.yaml diff --git a/congress/datalog/base.py b/congress/datalog/base.py index 4ab9ba778..65b56cde3 100644 --- a/congress/datalog/base.py +++ b/congress/datalog/base.py @@ -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): diff --git a/congress/datalog/nonrecursive.py b/congress/datalog/nonrecursive.py index 0aff45c0f..0399fe128 100644 --- a/congress/datalog/nonrecursive.py +++ b/congress/datalog/nonrecursive.py @@ -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. diff --git a/congress/library_service/library_service.py b/congress/library_service/library_service.py index e77c6ae48..4a0d6ac8d 100644 --- a/congress/library_service/library_service.py +++ b/congress/library_service/library_service.py @@ -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": { diff --git a/congress/policy_engines/agnostic.py b/congress/policy_engines/agnostic.py index bda2e4c27..740ae1d80 100644 --- a/congress/policy_engines/agnostic.py +++ b/congress/policy_engines/agnostic.py @@ -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__) @@ -621,6 +623,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) @@ -684,14 +692,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] @@ -1216,7 +1227,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")) diff --git a/congress/tests/z3/__init__.py b/congress/tests/z3/__init__.py new file mode 100644 index 000000000..e69de29bb diff --git a/congress/tests/z3/test_typechecker.py b/congress/tests/z3/test_typechecker.py new file mode 100644 index 000000000..f02e743da --- /dev/null +++ b/congress/tests/z3/test_typechecker.py @@ -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 diff --git a/congress/tests/z3/test_z3theory.py b/congress/tests/z3/test_z3theory.py new file mode 100644 index 000000000..d8bdc119e --- /dev/null +++ b/congress/tests/z3/test_z3theory.py @@ -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) diff --git a/congress/tests/z3/test_z3types.py b/congress/tests/z3/test_z3types.py new file mode 100644 index 000000000..86f1941e1 --- /dev/null +++ b/congress/tests/z3/test_z3types.py @@ -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) diff --git a/congress/tests/z3/z3mock.py b/congress/tests/z3/z3mock.py new file mode 100644 index 000000000..a2531737d --- /dev/null +++ b/congress/tests/z3/z3mock.py @@ -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 diff --git a/congress/z3/__init__.py b/congress/z3/__init__.py new file mode 100644 index 000000000..e69de29bb diff --git a/congress/z3/typechecker.py b/congress/z3/typechecker.py new file mode 100644 index 000000000..a74951099 --- /dev/null +++ b/congress/z3/typechecker.py @@ -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 diff --git a/congress/z3/z3theory.py b/congress/z3/z3theory.py new file mode 100644 index 000000000..8481f55c7 --- /dev/null +++ b/congress/z3/z3theory.py @@ -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) diff --git a/congress/z3/z3types.py b/congress/z3/z3types.py new file mode 100644 index 000000000..d99284886 --- /dev/null +++ b/congress/z3/z3types.py @@ -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)) diff --git a/devstack/plugin.sh b/devstack/plugin.sh index 0c03cd40c..78c8858d0 100755 --- a/devstack/plugin.sh +++ b/devstack/plugin.sh @@ -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 diff --git a/devstack/settings b/devstack/settings index 8050d677d..bf98d4870 100644 --- a/devstack/settings +++ b/devstack/settings @@ -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 diff --git a/doc/source/install/index.rst b/doc/source/install/index.rst index 3e451f346..2952a68d8 100644 --- a/doc/source/install/index.rst +++ b/doc/source/install/index.rst @@ -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 diff --git a/doc/source/user/api.rst b/doc/source/user/api.rst index b155fa458..7fcbf7cb8 100644 --- a/doc/source/user/api.rst +++ b/doc/source/user/api.rst @@ -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*. ======= ============================ ================================ diff --git a/doc/source/user/policy.rst b/doc/source/user/policy.rst index c6e029994..bc1533da9 100644 --- a/doc/source/user/policy.rst +++ b/doc/source/user/policy.rst @@ -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 ==================== diff --git a/releasenotes/notes/z3-engine-30c0d0fb93ea7a52.yaml b/releasenotes/notes/z3-engine-30c0d0fb93ea7a52.yaml new file mode 100644 index 000000000..621968033 --- /dev/null +++ b/releasenotes/notes/z3-engine-30c0d0fb93ea7a52.yaml @@ -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.