Merge "Z3 engine as an alternative Datalog engine"
This commit is contained in:
commit
5c43a61a02
|
@ -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):
|
||||
|
|
|
@ -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.
|
||||
|
||||
|
|
|
@ -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": {
|
||||
|
|
|
@ -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"))
|
||||
|
|
|
@ -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
|
|
@ -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)
|
|
@ -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)
|
|
@ -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,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
|
|
@ -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)
|
|
@ -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))
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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*.
|
||||
|
||||
|
||||
======= ============================ ================================
|
||||
|
|
|
@ -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
|
||||
====================
|
||||
|
|
|
@ -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.
|
Loading…
Reference in New Issue