Skip to content

Commit

Permalink
Added abs built-in function
Browse files Browse the repository at this point in the history
  • Loading branch information
bannsec committed Apr 7, 2016
1 parent 17dedb5 commit 5ecbedd
Show file tree
Hide file tree
Showing 3 changed files with 101 additions and 1 deletion.
2 changes: 1 addition & 1 deletion WhatIsImplemented.md
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ Example:


# Built-in
* abs (Not Implemented)
* abs (Fully Implemented)
* all (Not Implemented)
* any (Not Implemented)
* ascii (Not Implemented)
Expand Down
57 changes: 57 additions & 0 deletions pyState/functions/abs.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
from pyObjectManager.Int import Int
from pyObjectManager.Real import Real
from pyObjectManager.BitVec import BitVec
from pyObjectManager.String import String
import pyState
import logging
import z3

logger = logging.getLogger("pyState:functions:abs")


def handle(state,call,obj,ctx=None):
"""
Simulate abs funcion
"""
ctx = ctx if ctx is not None else state.ctx

# Resolve the object
objs = state.resolveObject(obj,ctx=ctx)

# Resolve calls if we need to
retObjs = [x for x in objs if type(x) is pyState.ReturnObject]
if len(retObjs) > 0:
return retObjs

retList = []

# Loop through all possible inputs
for obj in objs:

s = obj.state.copy()

obj.setState(s)

if type(obj) not in [Int, Real, BitVec]:
err = "handle: This shouldn't happen. Possibly a target program bug? Got obj type {0}".format(type(obj))
logger.error(err)
raise Exception(err)

oldObj = obj.getZ3Object()

newObj = obj.getZ3Object(increment=True)

# Add a little z3 If statement to mimic abs() call
s.addConstraint(
newObj ==
z3.If(
oldObj > 0,
oldObj,
-oldObj
)
)

retList.append(obj.copy())

# Return all options
return retList
43 changes: 43 additions & 0 deletions tests/test_function_abs.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
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
from pyObjectManager.Int import Int
from pyObjectManager.Real import Real
from pyObjectManager.BitVec import BitVec
from pyObjectManager.List import List

test1 = """
x = 10
y = -10
a = abs(x)
b = abs(y)
c = abs(10)
d = abs(-10)
"""

def test_funcion_abs():
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('a') == 10
assert pg.completed[0].state.any_int('b') == 10
assert pg.completed[0].state.any_int('c') == 10
assert pg.completed[0].state.any_int('d') == 10




0 comments on commit 5ecbedd

Please sign in to comment.