CORD-1570: Several bug fixes, expanded unit tests for security refactoring
Change-Id: Ied8dca916d3c22a252f6de38a65ef1b20c9d639d
diff --git a/lib/xos-genx/tests/optimize_test.py b/lib/xos-genx/tests/optimize_test.py
index ce15bf4..af40575 100644
--- a/lib/xos-genx/tests/optimize_test.py
+++ b/lib/xos-genx/tests/optimize_test.py
@@ -1,70 +1,78 @@
import unittest
from xosgenx.jinja2_extensions.fol2 import FOL2Python
-import pdb
+import vimpdb
class XProtoOptimizeTest(unittest.TestCase):
def setUp(self):
self.f2p = FOL2Python()
+ self.maxDiff=None
def test_constant(self):
input = 'True'
- output = self.f2p.hoist_constants(input)
+ output = self.f2p.hoist_outer(input)
self.assertEqual(output, input)
def test_exists(self):
- input = {'exists': ['x',{'|':['x','y']}]}
+ input = {'exists': ['X',{'|':['X.foo','y']}]}
- output = self.f2p.hoist_constants(input)
- expected = {'|': ['y', {'exists': ['x', 'x']}]}
+ output = self.f2p.hoist_outer(input)
+ expected = {'|': ['y', {'&': [{'not': 'y'}, {'exists': ['X', 'X.foo']}]}]}
self.assertEqual(output, expected)
- def test_forall(self):
- input = {'forall': ['x',{'|':['x','y']}]}
+ def test_exists_implies(self):
+ input = {'exists': ['Foo', {'&': [{'=': ('Foo.a', '1')}, {'->': ['write_access', {'=': ('Foo.b', '1')}]}]}]}
- output = self.f2p.hoist_constants(input)
- expected = {'|': ['y', {'forall': ['x', 'x']}]}
+ output = self.f2p.hoist_outer(input)
+ expected = {'|': [{'&': ['write_access', {'exists': ['Foo', {'&': [{'=': ['Foo.a', '1']}, {'=': ['Foo.b', '1']}]}]}]}, {'&': [{'not': 'write_access'}, {'exists': ['Foo', {'=': ['Foo.a', '1']}]}]}]}
+ self.assertEqual(output, expected)
+
+ def test_forall(self):
+ input = {'forall': ['X',{'|':['X.foo','y']}]}
+
+ output = self.f2p.hoist_outer(input)
+ expected = {'|': ['y', {'&': [{'not': 'y'}, {'forall': ['X', 'X.foo']}]}]}
self.assertEqual(output, expected)
def test_exists_embedded(self):
- input = {'|':['True',{'exists': ['x',{'|':['x','y']}]}]}
+ input = {'&':['True',{'exists': ['X',{'|':['X.foo','y']}]}]}
- output = self.f2p.hoist_constants(input)
- expected = {'|': ['True', {'|': ['y', {'exists': ['x', 'x']}]}]}
+ output = self.f2p.hoist_outer(input)
+ expected = {'|': ['y', {'&': [{'not': 'y'}, {'exists': ['X', 'X.foo']}]}]}
self.assertEqual(output, expected)
def test_exists_equals(self):
- input = {'|':['True',{'exists': ['x',{'|':['x',{'=':['y','z']}]}]}]}
+ input = {'&':['True',{'exists': ['X',{'|':['X.foo',{'=':['y','z']}]}]}]}
- output = self.f2p.hoist_constants(input)
- expected = {'|': ['True', {'|': [{'=': ['y', 'z']}, {'exists': ['x', 'x']}]}]}
+ output = self.f2p.hoist_outer(input)
+ expected = {'|': [{'=': ['y', 'z']}, {'&': [{'not': {'=': ['y', 'z']}}, {'exists': ['X', 'X.foo']}]}]}
self.assertEqual(output, expected)
def test_exists_nested_constant(self):
- input = {'|':['True',{'exists': ['x',{'|':['y',{'=':['y','x']}]}]}]}
+ input = {'&':['True',{'exists': ['X',{'|':['y',{'=':['y','X.foo']}]}]}]}
- output = self.f2p.hoist_constants(input)
- expected = {'|': ['True', {'|': ['y', {'exists': ['x', {'=': ['y', 'x']}]}]}]}
+ output = self.f2p.hoist_outer(input)
+ expected = {'|': ['y', {'&': [{'not': 'y'}, {'exists': ['X', {'=': ['False', 'X.foo']}]}]}]}
self.assertEqual(output, expected)
def test_exists_nested(self):
- input = {'exists': ['x',{'exists':['y',{'=':['y','x']}]}]}
+ input = {'exists': ['X',{'exists':['Y',{'=':['Y.foo','X.foo']}]}]}
- output = self.f2p.hoist_constants(input)
- expected = {'exists': ['x', {'exists': ['y', {'=': ['y', 'x']}]}]}
- self.assertEqual(output, expected)
+ output = self.f2p.hoist_outer(input)
+ expected = input
+ self.assertEqual(input, output)
def test_exists_nested2(self):
- input = {'exists': ['x',{'exists':['y',{'=':['z','y']}]}]}
+ input = {'exists': ['X',{'exists':['Y',{'=':['Z','Y']}]}]}
- output = self.f2p.hoist_constants(input)
- expected = {'exists': ['y', {'=': ['z', 'y']}]}
+ output = self.f2p.hoist_outer(input)
+ expected = {'exists': ['Y', {'=': ['Z', 'Y']}]}
self.assertEqual(output, expected)
def test_exists_nested3(self):
- input = {'exists': ['x',{'exists':['y',{'=':['z','x']}]}]}
+ input = {'exists': ['X',{'exists':['Y',{'=':['Z','X']}]}]}
- output = self.f2p.hoist_constants(input)
- expected = {'exists': ['x', {'=': ['z', 'x']}]}
+ output = self.f2p.hoist_outer(input)
+ expected = {'exists': ['X', {'=': ['Z', 'X']}]}
self.assertEqual(output, expected)