Skip to content

Commit

Permalink
Added built-in len function
Browse files Browse the repository at this point in the history
  • Loading branch information
bannsec committed Mar 31, 2016
1 parent aeaeb09 commit 43cabae
Show file tree
Hide file tree
Showing 2 changed files with 56 additions and 0 deletions.
19 changes: 19 additions & 0 deletions pyState/functions/len.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
from pyObjectManager.Int import Int

def handle(state,call,obj):
"""
Simulate len funcion
"""
# Resolve the object
obj = state.resolveObject(obj)

# Just calling the length function on the object..
l = obj.length()

i = state.getVar("tmpLenValue",ctx=1, varType=Int)
i.increment()

# Tell Z3 about our value
state.addConstraint(i.getZ3Object() == l)

return i.copy()
37 changes: 37 additions & 0 deletions tests/test_function_len.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
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 = """
s = "abcd"
l = [x for x in s] + [1,2]
x = len(s)
y = len(l)
"""


def test_function_len():
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') == 4
assert pg.completed[0].state.any_int('y') == 6

0 comments on commit 43cabae

Please sign in to comment.