From d7236e2d23614afea2e6797be8557af9d45df00d Mon Sep 17 00:00:00 2001 From: Owlz Date: Wed, 30 Mar 2016 20:12:43 -0400 Subject: [PATCH] Improving UnaryOp support and test cases --- pyState/Assign.py | 2 +- pyState/Subscript.py | 18 ++------- pyState/UnaryOp.py | 61 +++++++++++++++++++++++++++++ pyState/__init__.py | 5 ++- tests/test_function_String_index.py | 26 ++++++++++++ tests/test_pyState_UnaryOp.py | 32 +++++++++++++++ 6 files changed, 126 insertions(+), 18 deletions(-) create mode 100644 pyState/UnaryOp.py create mode 100644 tests/test_pyState_UnaryOp.py diff --git a/pyState/Assign.py b/pyState/Assign.py index 153b695..84a36b1 100644 --- a/pyState/Assign.py +++ b/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) diff --git a/pyState/Subscript.py b/pyState/Subscript.py index c960237..06dffaf 100644 --- a/pyState/Subscript.py +++ b/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" diff --git a/pyState/UnaryOp.py b/pyState/UnaryOp.py new file mode 100644 index 0000000..cde60c0 --- /dev/null +++ b/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() diff --git a/pyState/__init__.py b/pyState/__init__.py index 41eafa7..426320c 100644 --- a/pyState/__init__.py +++ b/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: diff --git a/tests/test_function_String_index.py b/tests/test_function_String_index.py index 898ac73..be12e79 100644 --- a/tests/test_function_String_index.py +++ b/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) diff --git a/tests/test_pyState_UnaryOp.py b/tests/test_pyState_UnaryOp.py new file mode 100644 index 0000000..23723d0 --- /dev/null +++ b/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 +