- Python version: 3.6 and pip
- lxml --> pip install lxml
- python z3 library
- numpy --> pip install numpy
- create a tempLocation directory.
- When executing this program in VSCode, relative paths used in our code depends on where you open VSCode(Working Directory).
- Working directory is Precis/
- Usage: Instrumenter.exe --solution=<> --test-project-name=<> --test-file-name=<> --PUT-name=<> --post-condition=<>
- Note: solution needs to be path!
- Example: Instrumenter.exe --solution=$your dir of Stack$/Stack/Stack.sln --test-project-name=StackTest --test-file-name=StackContractTest.cs --PUT-name=PUT_PushContract --post-condition=true
Everything we pull, git changes linux line endings to windows; figure out configuration to no do that
-
Learners/feature_synthesis.py:
GenerateDerivedFeatures
generates a list of tuples of Z3 values now, need to make it return a list of feature vectors. -
*** Make a base Scorer class that can extended***: the scorer base class can be extended by classes such as EntropyScore, MaxConjunctScore
-
Data/feature_vector.py: Why
range(len(values) - 1)
before?
Before, values contains test label at the end, so the actual values don't include the last one. Now we have the constructor with additional fieldtestLabel
, so it should berange(len(values))
now. -
Teacher/houdini.py:
f.varZ3[i]
out of range
It comes from 1, if the inputvalues
are all actual values (withouttestLabel
) are we userange(len(values) - 1)
, then we will miss the value at the end. If we change it torange(len(values))
we should be good. -
Data/feature_vector.py:
valuesZ3
should beFalse
but print isTrue
Note!!! In z3py,BoolVal('False')
returnsTrue
, butBoolVal(False)
returnsFalse
. We should initialize with bool value rather than string. -
Leaner/houdini.py:
substitute()
doesn't work. The reason is that beforePrecisFeature
is initialized with string of variable name, which makes no sense for derived features such asNew_Count != Old_Count
. Now, we added new fieldisDerived
in constructor ofPrecisFeature
, whenisDerived
isTrue
, we setPrecisFeature
with a Z3 expression direcetly, if not then we use string of variable name and string of variable type to initialize the feature.