Formalize API for constraining a State (#232)

* Rename state.add to state.constrain

* Update all uses of state.constrain

* Rm check param

* Added changelog

* Update changelog

* Update

* Minor clean

CHANGELOG.md

@@ -0,0 +1,19 @@
+# Change Log
+
+The format is based on [Keep a Changelog](http://keepachangelog.com/).
+
+## [Unreleased](https://github.com/trailofbits/manticore/compare/0.1.0...HEAD)
+
+### Added
+- `State.constrain`
+
+### Changed
+- Command line verbosity: `--verbose` -> `-v` (up to `-vvvv`)
+
+### Fixed
+- Linux model fixes: syscalls, ELF loading
+- x86 and ARM fixes
+
+## 0.1.0 - 2017-04-24
+
+Initial public release.

manticore/core/executor.py

@@ -560,8 +560,7 @@ def fork(self, current_state, symbolic, vals, setstate=None):
 
         children = []
         if len(vals) == 1:
-            constraint = symbolic == vals[0]
-            current_state.add(constraint, check=True) #We already know it's sat
+            current_state.constrain(symbolic == vals[0])
             setstate(current_state, vals[0])
             #current_state._try_simplify()
         else:
@@ -572,7 +571,7 @@ def fork(self, current_state, symbolic, vals, setstate=None):
 
             for new_value in vals:
                 with current_state as new_state:
-                    new_state.add(symbolic == new_value, check=False) #We already know it's sat
+                    new_state.constrain(symbolic == new_value)
                     #and set the PC of the new state to the concrete pc-dest
                     #(or other register or memory address to concrete)
                     setstate(new_state, new_value) 
@@ -755,14 +754,14 @@ def setstate(state, val):
 
                     children = []
                     with current_state as new_state:
-                        new_state.add(e.constraint==False)
+                        new_state.constrain(e.constraint==False)
                         if solver.check(new_state.constraints):
                             self.putState(new_state)
                             children.append(new_state.co)
 
                     with current_state as new_state:
                         children.append(new_state.co)
-                        new_state.add(e.constraint)
+                        new_state.constrain(e.constraint)
                         self.newerror(new_state.cpu.PC)
                         self.generate_testcase(new_state, "Symbolic Memory Exception: " + str(e))
 

manticore/core/state.py

@@ -95,7 +95,11 @@ def execute(self):
         self.last_pc = trace_item
         return result
 
-    def add(self, constraint, check=False):
+    def constrain(self, constraint):
+        '''Constrain state.
+
+        :param manticore.core.smtlib.Bool constraint: Constraint to add
+        '''
         self.constraints.add(constraint)
 
     def abandon(self):

tests/test_state.py

@@ -43,28 +43,28 @@ def setUp(self):
     def test_solve_one(self):
         val = 42
         expr = BitVecVariable(32, 'tmp')
-        self.state.add(expr == val)
+        self.state.constrain(expr == val)
         solved = self.state.solve_one(expr)
         self.assertEqual(solved, val)
 
     def test_solve_n(self):
         expr = BitVecVariable(32, 'tmp')
-        self.state.add(expr > 4)
-        self.state.add(expr < 7)
+        self.state.constrain(expr > 4)
+        self.state.constrain(expr < 7)
         solved = self.state.solve_n(expr, 2)
         self.assertEqual(solved, [5,6])
 
     def test_solve_n2(self):
         expr = BitVecVariable(32, 'tmp')
-        self.state.add(expr > 4)
-        self.state.add(expr < 100)
+        self.state.constrain(expr > 4)
+        self.state.constrain(expr < 100)
         solved = self.state.solve_n(expr, 5)
         self.assertEqual(len(solved), 5)
 
     def test_policy_one(self):
         expr = BitVecVariable(32, 'tmp')
-        self.state.add(expr > 0)
-        self.state.add(expr < 100)
+        self.state.constrain(expr > 0)
+        self.state.constrain(expr < 100)
         solved = self.state.concretize(expr, 'ONE')
         self.assertEqual(len(solved), 1)
         self.assertIn(solved[0], xrange(100))
@@ -74,7 +74,7 @@ def test_state(self):
         initial_state = State(constraints, FakeModel())
 
         arr = initial_state.symbolicate_buffer('+'*100, label='SYMBA')
-        initial_state.add(arr[0] > 0x41)
+        initial_state.constrain(arr[0] > 0x41)
         self.assertTrue(len(initial_state.constraints.declarations) == 1 ) 
         with initial_state as new_state:
 
@@ -85,7 +85,7 @@ def test_state(self):
             self.assertTrue(len(initial_state.constraints.declarations) == 1 ) 
             self.assertTrue(len(new_state.constraints.declarations) == 1 ) 
 
-            new_state.add(arrb[0] > 0x42)
+            new_state.constrain(arrb[0] > 0x42)
 
 
             self.assertTrue(len(new_state.constraints.declarations) == 2 )