From da81e355b80a613aa843ca00ad61ed28cbbd1b42 Mon Sep 17 00:00:00 2001
From: Yan <yan@users.noreply.github.com>
Date: Wed, 15 Feb 2017 13:35:40 -0500
Subject: [PATCH] Fix symbolic argv (#12)

* Proxy ArrayStore's 'name' property to the underlying Array
* Make setup_stack() repeatable
* Re-initialize the stack if any of the environment was symbolicated
* Encorporate name proxy test to ArrayStore
* Use issymbolic()
---
 manticore/core/smtlib/expression.py |  4 ++++
 manticore/manticore.py              | 33 ++++++++++++++++++-----------
 manticore/models/linux.py           |  6 ++++++
 test/test_smtlibv2.py               |  6 +++++-
 4 files changed, 36 insertions(+), 13 deletions(-)

diff --git a/manticore/core/smtlib/expression.py b/manticore/core/smtlib/expression.py
index eda8d10..dd03fd6 100644
--- a/manticore/core/smtlib/expression.py
+++ b/manticore/core/smtlib/expression.py
@@ -590,6 +590,10 @@ class ArrayStore(ArrayOperation):
     def array(self):
         return self.operands[0]
 
+    @property
+    def name(self):
+        return self.operands[0].name
+
     @property
     def index(self):
         return self.operands[1]
diff --git a/manticore/manticore.py b/manticore/manticore.py
index 5745f6c..f615ef7 100644
--- a/manticore/manticore.py
+++ b/manticore/manticore.py
@@ -24,6 +24,12 @@ from utils import gdb, qemu
 logger = logging.getLogger('MANTICORE')
 
 
+def issymbolic(value):
+    '''
+    Helper to determine whether a value read from memory is symbolic.
+    '''
+    return isinstance(value, Expression)
+
 
 def makeDecree(args):
     constraints = ConstraintSet()
@@ -37,23 +43,32 @@ def makeDecree(args):
     model.input.transmit(initial_state.symbolicate_buffer('+'*14, label='RECEIVE'))
     return initial_state
 
-def makeLinux(program, arguments, environment, concrete_start = ''):
+def makeLinux(program, argv, env, concrete_start = ''):
     logger.info('Loading program %s', program)
 
     constraints = ConstraintSet()
-    model = linux.SLinux(constraints, program, argv=arguments, envp=environment, symbolic_files=('symbolic.txt'))
+    model = linux.SLinux(constraints, program, argv=argv, envp=env,
+            symbolic_files=('symbolic.txt'))
     initial_state = State(constraints, model)
 
     if concrete_start != '':
         logger.info('Starting with concrete input: {}'.format(concrete_start))
 
-    for i in xrange(len(arguments)):
-        arguments[i] = initial_state.symbolicate_buffer(arguments[i], label='ARGV%d' % (i+1), string=True)    
+    for i, arg in enumerate(argv):
+        argv[i] = initial_state.symbolicate_buffer(arg, label='ARGV%d' % (i+1),
+                string=True)
 
-    for i in xrange(len(environment)):
-        environment[i] = initial_state.symbolicate_buffer(environment[i], label='ENV%d' % (i+1), string=True)    
+    for i, evar in enumerate(env):
+        env[i] = initial_state.symbolicate_buffer(evar, label='ENV%d' % (i+1),
+                string=True)
+
+    # If any of the arguments or environment refer to symbolic values, re-
+    # initialize the stack
+    if any(issymbolic(x) for val in argv + env for x in val):
+        model.setup_stack(initial_state.cpu, [program] + argv, env)
 
     model.input.transmit(concrete_start)
+
     #set stdin input...
     model.input.transmit(initial_state.symbolicate_buffer('+'*256, label='STDIN'))
 
@@ -120,12 +135,6 @@ def binary_type(path):
     else:
         raise NotImplementedError("Binary {} not supported.".format(path))
 
-def issymbolic(value):
-    '''
-    Helper to determine whether a value read from memory is symbolic.
-    '''
-    return isinstance(value, Expression)
-
 class Manticore(object):
 
     def __init__(self, binary_path, args = [], verbose = False):
diff --git a/manticore/models/linux.py b/manticore/models/linux.py
index 1009b39..7dab4a9 100644
--- a/manticore/models/linux.py
+++ b/manticore/models/linux.py
@@ -310,6 +310,7 @@ class Linux(object):
         cpu = self._mk_proc(arch)
         self.load(cpu, program)
         self._arch_reg_init(cpu, arch)
+        self._stack_top = cpu.STACK
         self.setup_stack(cpu, [program]+argv, envp)
 
 
@@ -475,6 +476,11 @@ class Linux(object):
          (0xc0000000)      < top of stack >              0   (virtual)
          ----------------------------------------------------------------------
         '''
+
+        # In case setup_stack() is called again, we make sure we're growing the
+        # stack from the original top
+        cpu.STACK = self._stack_top
+
         # TODO cpu.STACK_push_bytes() pls
         def push_bytes(data):
             cpu.STACK -= len(data)
diff --git a/test/test_smtlibv2.py b/test/test_smtlibv2.py
index 52fd894..a0efeca 100644
--- a/test/test_smtlibv2.py
+++ b/test/test_smtlibv2.py
@@ -133,9 +133,10 @@ class ExpressionTest(unittest.TestCase):
             self.assertTrue(self.solver.check(temp_cs))
 
     def testBasicArrayStore(self):
+        name = "bitarray"
         cs =  ConstraintSet()
         #make array of 32->8 bits
-        array = cs.new_array(32)
+        array = cs.new_array(32, name=name)
         #make free 32bit bitvector 
         key = cs.new_bitvec(32)
 
@@ -150,6 +151,9 @@ class ExpressionTest(unittest.TestCase):
         #1001 position of array can be 'B'
         self.assertTrue(self.solver.can_be_true(cs, array.select(1001) == 'B'))
 
+        #name is correctly proxied
+        self.assertEqual(array.name, name + "_1")
+
         with cs as temp_cs:
             #but if it is 'B' ...
             temp_cs.add(array.select(1001) == 'B')