Improving UnaryOp support and test cases

pyState/Assign.py

@@ -118,7 +118,7 @@ def handle(state,element):
             ret += _handleAssignString(state.copy(),target,value)
 
         else:
-            err = "Don't know how to assign type {0} at line {1} col {2}".format(type(value),value.lineno,value.col_offset)
+            err = "Don't know how to assign type {0}".format(type(value))
             logger.error(err)
             raise Exception(err)
 

pyState/Subscript.py

@@ -66,11 +66,7 @@ def _handleSlice(state,sub_object,sub_slice):
 
     if type(lower) not in [int,type(None)]:
         if lower.isStatic():
-            lower = lower.value
-
-        # Check if it's a variable that only has one possibility
-        elif type(lower) in [Int, BitVec] and len(state.any_n_int(lower,2)) == 1:
-            lower = state.any_int(lower)
+            lower = lower.getValue()
 
         else:
             err = "_handleSlice: Don't know how to handle symbolic lower slice integers at the moment"
@@ -84,11 +80,7 @@ def _handleSlice(state,sub_object,sub_slice):
 
     if type(upper) not in [int,type(None)]:
         if upper.isStatic():
-            upper = upper.value
-
-        # Check if it's a variable that only has one possibility
-        elif type(upper) in [Int, BitVec] and len(state.any_n_int(upper,2)) == 1:
-            upper = state.any_int(upper)
+            upper = upper.getValue()
 
         else:
             err = "_handleSlice: Don't know how to handle symbolic upper slice integers at the moment"
@@ -102,11 +94,7 @@ def _handleSlice(state,sub_object,sub_slice):
 
     if type(step) not in [int,type(None)]:
         if step.isStatic():
-            step = step.value
-
-        # Check if it's a variable that only has one possibility
-        elif type(step) in [Int, BitVec] and len(state.any_n_int(step,2)) == 1:
-            step = state.any_int(step)
+            step = step.getValue()
 
         else:
             err = "_handleSlice: Don't know how to handle symbolic step slice integers at the moment"

pyState/UnaryOp.py

@@ -0,0 +1,61 @@
+import logging
+import z3
+import ast
+import pyState
+from pyObjectManager.Int import Int
+from pyObjectManager.Real import Real
+from pyObjectManager.BitVec import BitVec
+from copy import deepcopy
+
+logger = logging.getLogger("pyState:UnaryOp")
+
+def handle(state,element,ctx=None):
+    """
+    Input:
+        state = State object
+        element = ast.UnaryOp element to parse
+        (optional) ctx = context to resolve UnaryOp in if not current
+    Action:
+        Parse out the element with respect to the state
+    Returns:
+        pyObjectManager object representing this UnaryOp
+    """
+    ctx = state.ctx if ctx is None else ctx
+
+    assert type(state) == pyState.State
+    assert type(element) == ast.UnaryOp
+
+    op = element.op
+    target = state.resolveObject(element.operand)
+
+    if type(target) not in [Int, Real, BitVec]:
+        err = "handle: unable to resolve UnaryOp target type '{0}'".format(type(target))
+        logger.error(err)
+        raise Exception(err)
+
+    # Get a new variable
+    t,args = pyState.duplicateSort(target)
+    newVar = state.getVar("tempUnaryOp",varType=t,kwargs=args)
+    newVar.increment()
+
+    if type(op) == ast.USub:
+        state.addConstraint(newVar.getZ3Object() == -target.getZ3Object())
+
+    elif type(op) == ast.UAdd:
+        state.addConstraint(newVar.getZ3Object() == target.getZ3Object())
+
+    elif type(op) == ast.Not:
+        state.addConstraint(newVar.getZ3Object() == z3.Not(target.getZ3Object()))
+
+    elif type(op) == ast.Invert:
+        err = "handle: Invert not implemented yet"
+        logger.error(err)
+        raise Exception(err)
+
+    else:
+        # We really shouldn't get here...
+        err = "handle: {0} not implemented yet".format(type(op))
+        logger.error(err)
+        raise Exception(err)
+
+    return newVar.copy()

pyState/__init__.py

@@ -2,7 +2,7 @@
 import ast
 import logging
 from copy import copy, deepcopy
-import pyState.BinOp, pyState.Pass, pyState.While, pyState.Break, pyState.Subscript, pyState.For, pyState.ListComp
+import pyState.BinOp, pyState.Pass, pyState.While, pyState.Break, pyState.Subscript, pyState.For, pyState.ListComp, pyState.UnaryOp
 import random
 import os.path
 import importlib
@@ -865,7 +865,8 @@ def resolveObject(self,obj,parent=None,ctx=None,varType=None,kwargs=None):
         elif t == ast.UnaryOp:
             # TODO: Not sure if there will be symbolic UnaryOp objects... This wouldn't work for those.
             logger.debug("resolveObject: Resolving UnaryOp type object")
-            return ast.literal_eval(obj)
+            #return ast.literal_eval(obj)
+            return pyState.UnaryOp.handle(self,obj,ctx=ctx)
 
 
         else:

tests/test_function_String_index.py

@@ -26,6 +26,32 @@
 x = s.index('a')
 """
 
+test3 = """
+s = pyState.String(10)
+x = -1
+if s[3] == "a":
+    x = s.index('a')
+"""
+
+def test_function_String_Index_PartiallySymbolic():
+    b = ast.parse(test3).body
+    p = Path(b,source=test3)
+    pg = PathGroup(p)
+
+    pg.explore()
+
+    # Every index should be a possibility
+    assert len(pg.completed) == 5
+
+    indexes = []
+    # Make sure we got all of them
+    for path in pg.completed:
+        indexes.append(path.state.any_int('x'))
+
+    assert set(indexes) == set(range(4)).union({-1})
+
+
+
 def test_function_String_Index_Symbolic():
     b = ast.parse(test2).body
     p = Path(b,source=test2)

tests/test_pyState_UnaryOp.py

@@ -0,0 +1,32 @@
+import sys, os
+myPath = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, myPath + '/../')
+
+import logging
+import Colorer
+logging.basicConfig(level=logging.DEBUG,format='%(name)s - %(levelname)s - %(message)s', datefmt='%m/%d/%Y %I:%M:%S %p')
+
+
+import ast
+import z3
+from pyPath import Path
+from pyPathGroup import PathGroup
+import pytest
+
+test1 = """
+x = -1
+y = -x
+z = +x
+"""
+
+def test_pySym_UnaryOp_Simple():
+    b = ast.parse(test1).body
+    p = Path(b,source=test1)
+    pg = PathGroup(p)
+
+    pg.explore()
+    assert len(pg.completed) == 1
+    assert pg.completed[0].state.any_int('x') == -1
+    assert pg.completed[0].state.any_int('y') == 1
+    assert pg.completed[0].state.any_int('z') == -1
+