diff --git a/pyObjectManager/List.py b/pyObjectManager/List.py index bb576e6..e9e151f 100644 --- a/pyObjectManager/List.py +++ b/pyObjectManager/List.py @@ -55,6 +55,7 @@ def increment(self): self.count += 1 # reset variable list if we're incrementing our count self.variables = [] + def append(self,var,kwargs=None): """ diff --git a/pyState/BinOp.py b/pyState/BinOp.py index c20c58e..ff0db20 100644 --- a/pyState/BinOp.py +++ b/pyState/BinOp.py @@ -6,6 +6,7 @@ from pyObjectManager.Real import Real from pyObjectManager.BitVec import BitVec from pyObjectManager.String import String +from pyObjectManager.List import List from copy import deepcopy logger = logging.getLogger("pyState:BinOp") @@ -105,6 +106,20 @@ def _handleStr(state,left,right,op): return s.copy() +def _handleList(state,left,right,op): + """ + Handle BinOp for List types + """ + assert type(left) is List + assert type(right) is List + + # Because Lists are just class abstractions, we can do this without touching Z3 + s = state.getVar("tempBinOpList",ctx=1,varType=List) + s.increment() + s.variables = left.copy().variables + right.copy().variables + return s.copy() + + def handle(state,element,ctx=None): """ Input: @@ -128,6 +143,9 @@ def handle(state,element,ctx=None): if type(left) == pyState.ReturnObject: return left + # Save a copy so that we don't lose it + left = left.copy() + logger.debug("BinOp: BinOp Left = {0}".format(left)) right = state.resolveObject(element.right,parent=element,ctx=ctx) @@ -135,6 +153,9 @@ def handle(state,element,ctx=None): if type(right) == pyState.ReturnObject: return right + # Save a copy so that we don't lose it + right = right.copy() + logger.debug("BinOp: BinOp Right = {0}".format(right)) op = element.op @@ -146,6 +167,9 @@ def handle(state,element,ctx=None): elif type(left) is String: return _handleStr(state,left,right,op) + elif type(left) is List: + return _handleList(state,left,right,op) + else: err = "BinOP: Don't know how to handle variable type {0}".format(type(left)) logger.error(err) diff --git a/tests/test_pyState_BinOp.py b/tests/test_pyState_BinOp.py index ed12a57..9d53d64 100644 --- a/tests/test_pyState_BinOp.py +++ b/tests/test_pyState_BinOp.py @@ -69,6 +69,20 @@ def test(x,y): s3 = "This " + "is " + "a " + "test" """ +test11 = """ +l = [1,2,3] + [4,5,6] +""" + +def test_pySym_BinOp_ListConcat(): + b = ast.parse(test11).body + p = Path(b,source=test11) + pg = PathGroup(p) + pg.explore() + + assert len(pg.completed) == 1 + assert pg.completed[0].state.any_list('l') == [1,2,3] + [4,5,6] + + def test_pySym_BinOp_StrConcat(): b = ast.parse(test10).body p = Path(b,source=test10)