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

@@ -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]

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):

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)

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')