FilesExpand file tree

master

/

pyexz3_function.py

Copy path

Blame

More file actions

Blame

More file actions

Latest commit

 

History

History

History

59 lines (47 loc) · 2.37 KB

master

/

pyexz3_function.py

Copy path

Top

File metadata and controls

• Code
• Blame

59 lines (47 loc) · 2.37 KB

Raw

Copy raw file

Download raw file

Open symbols panel

Edit and raw actions

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

32

33

34

35

36

37

38

39

40

41

42

43

44

45

46

47

48

49

50

51

52

53

54

55

56

57

58

59

import logging

from optparse import OptionParser

from RelativeTesting.symbolic.loader import *

from RelativeTesting.symbolic.explore import ExplorationEngine

def pyexz3_function(file_path, test_case_count, constraint_input):

sys.path = [os.path.abspath(os.path.join(os.path.dirname(__file__)))] + sys.path

sys.path.append(os.path.join(os.path.dirname(__file__), 'RelativeTesting'))

print(sys.path)

usage = "usage: %prog [options] <path to a *.py file>"

parser = OptionParser(usage=usage)

parser.add_option("-l", "--log", dest="logfile", action="store", help="Save log output to a file", default="")

parser.add_option("-s", "--start", dest="entry", action="store", help="Specify entry point", default="")

parser.add_option("-g", "--graph", dest="dot_graph", action="store_true",

help="Generate a DOT graph of execution tree")

parser.add_option("-m", "--max-iters", dest="max_iters", type="int", help="Run specified number of iterations",

default=0)

parser.add_option("--cvc", dest="cvc", action="store_true", help="Use the CVC SMT solver instead of Z3",

default=False)

parser.add_option("--z3", dest="cvc", action="store_false", help="Use the Z3 SMT solver")

(options, args) = parser.parse_args()

print("options", options)

if not (options.logfile == ""):

logging.basicConfig(filename=options.logfile, level=logging.DEBUG)

solver = "cvc" if options.cvc else "z3"

filename = os.path.abspath(file_path)

# Get the object describing the application

app = loaderFactory(filename, options.entry)

print("entry", options)

if not app:

print("Unable to load %s" % filename)

return False

# Which file is being explored now

print("Exploring " + app.getFile() + "." + app.getEntry())

result = None

try:

engine = ExplorationEngine(app.createInvocation(), constraint_input, solver=solver, solution_limit=test_case_count)

generatedInputs, returnVals, path, gpt_ans = engine.explore(options.max_iters)

# check the result

result = app.executionComplete(returnVals)

except ImportError as e:

# createInvocation can raise this

logging.error(e)

return False

if result == None or result == True:

return {"PyXZ3": generatedInputs, "ChatGPT": gpt_ans}

else:

return False