thomasjball/pyexz3

Python Exploration with Z3

pyexz3's Issues

make a cvc test directory

Let's keep a separate directory for tests that require CVC.

-- Tom

path

Hello author, I want to get all the paths of a program separately, which part of the code should I use? Or do you have any other suggestions? Looking forward to your reply

[Feature Request] Add support for strings via Z3-str2

Whenever you get a chance, can you please add support for strings? I'm not sure how much work it would be but it would be quite nice :) It is open-source https://github.com/z3str/Z3-str.

Could you tell me why this has only 1 path?

from symbolic.args import *

@symbolic(a=0xdeaddeaddeaddead,b=0xbeefbeefbeefbeef)
def expandKey(a,b):
    i=0;
    passkeyn=[a,b]

    expandedkey=[]
    while i<6:
        expandedkey=expandedkey+passkeyn
        i=i+1
        v1=passkeyn[0]
        v2=passkeyn[1]
        v3=(v1>>0x30)|(((v1>>0x20)&0xffff)<<0x10)|(((v1>>0x10)&0xffff)<<0x20)|((v1&0xffff)<<0x30)
        v4=(v2>>0x30)|(((v2>>0x20)&0xffff)<<0x10)|(((v2>>0x10)&0xffff)<<0x20)|((v2&0xffff)<<0x30)
        v5 = ((v4 & 0xFFFFFF8000000000) >> 39) | ((v3 << 25)&0xffffffffffffffff);
        v6 = ((v3 & 0xFFFFFF8000000000) >> 39) | ((v4 << 25)&0xffffffffffffffff);
        v1=(v5>>0x30)|(((v5>>0x20)&0xffff)<<0x10)|(((v5>>0x10)&0xffff)<<0x20)|(((v4 & 0xFFFFFF8000000000) >> 39)<<0x30)
        v2=(v6>>0x30)|(((v6>>32)&0xffff)<<0x10)|(((v6>>0x10)&0xffff)<<0x20)|(((v3 & 0xFFFFFF8000000000) >> 39)<<0x30)
        passkeyn=[v1,v2]
    expandedkey=expandedkey+passkeyn
    if expandedkey==[16045725885737590445, 13758425323549998831, 7044313620519854103485, 8215411798635391606653, 8245388070021240879798, 3384596836810669685695, 9287860625795901259255, 4527376222128629444341, 4093654381503457390331, 4647353382867023162077, 8665057901351565392853, 8816957627389395711965, 6783497306152038280055, 9291067819851303074799]:
        return 1
    return 2

Can PyExZ3 handle Hadoop MapReduce application?

Not all paths a found and some are listed multiple times

Before going into example I just want to emphesize that I have tinkered with the current code base to run it against the newest version of z3 (4.12.2) and python (3.11.4).
To do so I have changed all occurences of inspect.getargspec to inspect.getfullargspec
in symbolic/loader.py and symbolic/symbolic_types/symbolic_type.py

All tests except bignum are passing.

My example looks like the following:

def kolor(x,y):
  if y < x - 2 :
    return 7
  else :
    return 2

def zwierze(x,y):
  if y > 3 :
    return 10
  else:
    return 50

def czynnosc(x,y):
  if y < -x + 3 :
    return 100
  else :
    return 200

def yolo(a,b):
  return kolor(a,b)+zwierze(a,b)+czynnosc(a,b)

def expected_result():
  return [ 112, 157, 152, 217, 212, 257, 252]

#print (yolo(-2,4))

I have exected to find 7 paths with results like in the array returned by expected_result function but instead I got the following:

PyExZ3 (Python Exploration with Z3)
Exploring FILE.yolo
[('a', 0), ('b', 0)]
152
[('a', 8), ('b', 0)]
257
[('a', 0), ('b', 4)]
212
[('a', 0), ('b', 3)]
252
[('a', 8), ('b', 4)]
217
[('a', 0), ('b', -8)]
157
[('a', 8), ('b', 3)]
257
-------------------> FILE test failed <---------------------
Expected: {112: 1, 157: 1, 152: 1, 217: 1, 212: 1, 257: 1, 252: 1}, found: {152: 1, 257: 2, 212: 1, 252: 1, 217: 1, 157: 1}

Why am I getting 257 twice and why a path resulting in 112 is not found ?

bignum.py test failed

When I ran "python3 run_tests.py test", all tests passed except for test/bignum.py. Is that a bug from the code or something's wrong on my side?

What to do when some tests fails

I run this command to test as instructed

python run_tests.py test

I got success in every test except fp.py and bignum.py

Do you have any suggestions on what people should check or do if some of the tests fail?

Thank you

Input data type issue

Hello author,
I'm wondering if an input of type 'list' or 'string' is not generated.

Vagrant Box not found

Hi I'm looking for a tool for python SE. I'm using Mac and all stuffs in MacOS specific section seems to work well. However, the command vagrant up throws such an error:

==> linux: Box 'chef/debian-7.4' could not be found. Attempting to find and install...
linux: Box Provider: virtualbox
linux: Box Version: >= 0
The box 'chef/debian-7.4' could not be found or
could not be accessed in the remote catalog. If this is a private
box on HashiCorp's Atlas, please verify you're logged in via
vagrant login. Also, please double-check the name. The expanded
URL and error message are shown below:

URL: ["https://atlas.hashicorp.com/chef/debian-7.4"]
Error: The requested URL returned error: 404 Not Found

It seems that the Vagrant Box is somehow missing. I'm not familiar with Vagrant and can anybody tell me how to get access to that box?

Thanks!

Can't work on OS X with python version 3.4

Hi. I can't get it work on Py3.4 with my Mac.
I installed pyexz3 following the 'MacOS specific'.
Running this "python3 pyexz3.py test/loop.py" and I got:

Traceback (most recent call last):
File "pyexz3.py", line 10, in
from symbolic.explore import ExplorationEngine
File "/Users//Develop/PyExZ3/symbolic/explore.py", line 7, in
from .z3_wrap import Z3Wrapper
File "/Users//Develop/PyExZ3/symbolic/z3_wrap.py", line 7, in
from z3 import *
ImportError: bad magic number in 'z3': b'\x03\xf3\r\n'

I have tried to run it under Py2.7, but got another error.
I would appreciate any help. Thanks.

How to add the constraint in the path when the judgment statement is included in the loop module?