initial project files and strucutre.
- Apr 13, 2024
-
-
Maximilian Brokamp authored
-
Maximilian Brokamp authored
Added option to also print output into csv
-
Maximilian Brokamp authored
-
- Apr 03, 2024
-
-
Maximilian Brokamp authored
-
Maximilian Brokamp authored
-
Maximilian Brokamp authored
-
Maximilian Brokamp authored
add option for klee to not use any abbreviations ("--smtlib-abbreviation-mode=none) when generating smtlib formulas
-
Maximilian Brokamp authored
when the execution path is printed after a BB match, the last basic block will not get printed, because no instruction from it got executed at that point. Also reformatted option printing to look better/more consistent
-
Maximilian Brokamp authored
Addition of experimental option to add an extra clause to the CNF generated by stp to make the model count mroe accurate
-
- Apr 01, 2024
-
-
Maximilian Brokamp authored
-
Maximilian Brokamp authored
-
Maximilian Brokamp authored
-
Maximilian Brokamp authored
-
Maximilian Brokamp authored
removed all the unecessary and commented parts of the main CMakeLists.txt that were due to coping the file from KLEE.
-
Maximilian Brokamp authored
changed disclaimer in header file
-
Maximilian Brokamp authored
When a new state is created, the call stack of the parent state will now be deep copied. The previous version where only the last node is copied, led to problems in tracking the exeuction path, after the function the last node represented was exited. Function addCall now has a parameter to distinguis between functions for which the excution is tracked (with a DiffEntry) and untracked (without a DiffEntry)
-
Maximilian Brokamp authored
Also removed old debug code
-
- Mar 20, 2024
-
-
Maximilian Brokamp authored
Added Option to only output constraint matches, for which the patched constraint has more posible solutions as the unpatched constraint. Changed option to terminate after the specified number of iterations, to now termiate after a given time Changed option the default for option ouput constraints to be true
-
Maximilian Brokamp authored
-
- Mar 14, 2024
-
-
Maximilian Brokamp authored
-> changed how getMatchingLine works -> ExecutionPathNode and CallStackNode now also track the matchingline from the other code -> the end last line of an llvm function is now computed correctly New features: -> added -> callStack comparison -> unmatched CData with Types new_constraint and state_creation now get delted before output -> unmatched Constraints are added to the output -> added option to only match constraints for specific functions
-
Maximilian Brokamp authored
when comparing types of an allocation, the diff function now checks if one type is the renamed version of the other (check is done solely with the type names)
-
Maximilian Brokamp authored
changed how Basic Blocks get handled in the annotation writer and how the address is red in buildInstructionToLineTable. The line number of a Basic Block is now allways the one before the line of the first instruction. Before this the lines were the same, which lead to problems in the lineTable, which uses lines as a key.
-
- Mar 12, 2024
-
-
Maximilian Brokamp authored
Changed Implementation of ExecutionPathNode and CallStackNode to use ref<T> class (copied from KLEE) to easier manage the refferences. Call Stack Node now points to the first and last BBs that were executed in the current context, making it easier to only compare the Execution path for the current context (and ignoring any calls executed)
-
- Mar 11, 2024
-
-
Maximilian Brokamp authored
Added check for matching Execution Path to compare Function. Added more statistics to the output file. Fixed a bug where unmatched constraints were safed in the wrong map, leading to them not beein considered in future matches.
-
- Mar 08, 2024
-
-
Maximilian Brokamp authored
Added struct ExecutionPathNode. Added tracking of Execution paths (through tree of ExecutionPathNodes) Fixed bug int tryFindMatch where Constraints were entered in the wrong ConstraintMap
-
Maximilian Brokamp authored
Added option to only output constraints that have an equal/unequal model count. cleaned up main.cpp (removed dead and debugging code) changed a few logging locations.
-
- Mar 07, 2024
-
-
Maximilian Brokamp authored
Added Function getInstruction to obtain the correct Instruction ptr for each asmLine. changed FunctionDiff entries to allways contains an entrie for each BB to ensure the llvm Instruction pointer can allways be obtained by the asmLine
-
- Mar 06, 2024
-
-
Maximilian Brokamp authored
ConstraintComparator now keeps track of every not matched Constraint and at least the last constraint for each execution state in KLEE.
-
- Mar 04, 2024
-
-
Maximilian Brokamp authored
Added new Data Strucuture that holds the ConstraintRefs as well as tracks refferences to it. This will make sure only the necessary constraints that might be needed in the future are safed, while simultaneosly keeping track of multiple constraints per execution state. Currently in development and not workint and compiling.
-
- Feb 27, 2024
-
-
Maximilian Brokamp authored
Changed Model count to be returned as base and power instead of one number (did constantly overflow the 64 bit int) changed the name of optoins. Added printing to output file.
-
Maximilian Brokamp authored
This checks for overy combination of BBs if they are completely the same. Added possibility to delete DiffMap of Function and reset the status to match. Usefull if turns out after the comparison that all basic blocks were the same Also fixed some minor bugs.
-
Maximilian Brokamp authored
- changed input options (now the bitcode files are given directly as an option and the parent directory) - modified debug output - changed the bitcode files used comparison from the input files to the versions modified by klee. This is necessry for the assembly lines that klee outputs to match those in spa - removed not necessary functions from KleeManager class
-
- Feb 21, 2024
-
-
Maximilian Brokamp authored
Implemented main analysis loop, that handels incomming constraints from both klee instances, checks if they match, if calculates the model coung, and if not adds them to a list of unmatched constraitns. It was necessary to restrcuture the DiffEntry classes again (DiffEntry is no template function anymore). In the current state the program compiles, but no testing has been done, if the implementation is correct (probably not :) )
-
- Feb 19, 2024
-
-
Maximilian Brokamp authored
Added GetMatchingLine function to BitcodeDiff struct. This checks for a given line number what the corresponding line in the other bitcode file is. Modified behaviour of addMatch(Inst, Inst) to only add diff entries for the instructions, if the line offset differs from the offset of corresponding BasicBlock. Added addMatch() call for Instructions in FunctionDiffEngine
-
Maximilian Brokamp authored
Added waitInit() Function to klee manager, that waits for an initial message in the Shared memory queue before continuing. fixed name of klee output file to contain the instance name. Until now the filename of both instances only had the name "_out", leading to the log of one instance not beeing saved.
-
Maximilian Brokamp authored
fixed BitcodeDiff struct and Bitcode DiffBuilder, so that the diff correctly acutally contains all found differnces. Added printStream Function to DiffEntries to display found differences. temporary removed logging to logfile, due to crashes during logging.
-
- Feb 09, 2024
-
-
Maximilian Brokamp authored
Changed default logfile name from spa to spa.log to avoid issues with .gitignore excluding the folder called spa
-
Maximilian Brokamp authored
-
Maximilian Brokamp authored
The Code is largely based on the llvm-diff tools. With some changes to how the comparison of Instructions work and a complete change in the output Format. The code is currently functional, but the comparision in some aspects is not complete right now, mainly in the way different BasicBlocks are chosen as matching togehter between versions. Other changes: - Added Build Type variable in Config to allow DEBUG code to be excluded in production builds - removed some not needed parts of the main CMake file - added cmd option that allows to specifically call the Bitcode comparison features, without providing all the input
-
- Jan 28, 2024
-
-
Maximilian Brokamp authored
-
Maximilian Brokamp authored
-
Maximilian Brokamp authored
-
- Jan 19, 2024
-
-
Maximilian Brokamp authored
Added Opening, Handling and closing of klee porcesses by SPA. Destruction currently not completely bug free
-
- Jan 15, 2024
-
-
Maximilian Brokamp authored
-
- Dec 29, 2023
-
-
Maximilian Brokamp authored
basic input checking and the structure of some classes for getting and handling path constraints.
-
- Dec 21, 2023
-
-
Maximilian Brokamp authored
Currently the program does nothing
-