Repository: pysmt/pysmt
Pull request #310 (2016-08-24 18:04:38)

Assertions protecting FNodeContent.payload access
All methods in FNode that access the payload now check that the FNode
instance is of the correct type, e.g.:

FNode.symbol_name() checks that FNode.is_symbol()

This prevents from accessing the payload in a spurious way. Since this
has an impact on every access to the payload, it has been implemented as
an assertion, and can be disabled by running the interpreter with -O.


Patch:
diff --git a/pysmt/fnode.py b/pysmt/fnode.py
index 29140ae..41ccaee 100644
--- a/pysmt/fnode.py
+++ b/pysmt/fnode.py
@@ -532,14 +532,17 @@ class FNode(object):
 
     def symbol_type(self):
         """Return the type of the Symbol."""
+        assert self.is_symbol()
         return self._content.payload[1]
 
     def symbol_name(self):
         """Return the name of the Symbol."""
+        assert self.is_symbol()
         return self._content.payload[0]
 
     def constant_value(self):
         """Return the value of the Constant."""
+        assert self.is_constant()
         if self.node_type() == BV_CONSTANT:
             return self._content.payload[0]
         return self._content.payload
@@ -581,6 +584,7 @@ class FNode(object):
         return bitstr
 
     def array_value_index_type(self):
+        assert self.is_array_value()
         return self._content.payload
 
     def array_value_get(self, index):
@@ -612,10 +616,12 @@ class FNode(object):
 
     def function_name(self):
         """Return the Function name."""
+        assert self.is_function_application()
         return self._content.payload
 
     def quantifier_vars(self):
         """Return the list of quantified variables."""
+        assert self.is_quantifier()
         return self._content.payload
 
     def algebraic_approx_value(self, precision=10):


Test patch:
diff --git a/pysmt/test/test_formula.py b/pysmt/test/test_formula.py
index 50d9534..7f815cd 100644
--- a/pysmt/test/test_formula.py
+++ b/pysmt/test/test_formula.py
@@ -90,6 +90,45 @@ class TestFormulaManager(TestCase):
         c = self.mgr.Symbol("c")
         self.assertEqual(c.symbol_type(), BOOL, "Default Symbol Type is not BOOL")
 
+
+    def test_payload_assertions(self):
+        s = self.mgr.Symbol("x")
+        c = self.mgr.Int(0)
+
+        with self.assertRaises(AssertionError):
+            c.symbol_name()
+
+        with self.assertRaises(AssertionError):
+            c.symbol_type()
+
+        with self.assertRaises(AssertionError):
+            s.bv_width()
+
+        with self.assertRaises(AssertionError):
+            s.bv_extract_start()
+
+        with self.assertRaises(AssertionError):
+            s.bv_extract_end()
+
+        with self.assertRaises(AssertionError):
+            s.bv_rotation_step()
+
+        with self.assertRaises(AssertionError):
+            s.bv_extend_step()
+
+        with self.assertRaises(AssertionError):
+            s.bv_extract_end()
+
+        with self.assertRaises(AssertionError):
+            s.constant_value()
+
+        with self.assertRaises(AssertionError):
+            s.array_value_index_type()
+
+        with self.assertRaises(AssertionError):
+            s.function_name()
+
+
     def test_and_node(self):
         n = self.mgr.And(self.x, self.y)
         self.assertIsNotNone(n)