From 44d365ff4c50fb9ee829ef5f830dfb6dd421eb9c Mon Sep 17 00:00:00 2001 From: Mark Mossberg Date: Fri, 5 May 2017 13:31:43 -0400 Subject: [PATCH] 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 | 19 +++++++++++++++++++ manticore/core/executor.py | 9 ++++----- manticore/core/state.py | 6 +++++- tests/test_state.py | 18 +++++++++--------- 4 files changed, 37 insertions(+), 15 deletions(-) create mode 100644 CHANGELOG.md diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 0000000..59664fd --- /dev/null +++ b/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. \ No newline at end of file diff --git a/manticore/core/executor.py b/manticore/core/executor.py index 5d97e3b..a24a3c6 100644 --- a/manticore/core/executor.py +++ b/manticore/core/executor.py @@ -560,8 +560,7 @@ class Executor(object): 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 @@ class Executor(object): 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 @@ class Executor(object): 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)) diff --git a/manticore/core/state.py b/manticore/core/state.py index 1ef20ea..804eeb1 100644 --- a/manticore/core/state.py +++ b/manticore/core/state.py @@ -95,7 +95,11 @@ class State(object): 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): diff --git a/tests/test_state.py b/tests/test_state.py index b00a6b2..fe018e9 100644 --- a/tests/test_state.py +++ b/tests/test_state.py @@ -43,28 +43,28 @@ class StateTest(unittest.TestCase): 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 @@ class StateTest(unittest.TestCase): 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 @@ class StateTest(unittest.TestCase): 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 )