about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Collapse)Author
2024-05-02Refine support for stdio captureNguyễn Gia Phong
2024-03-05Relax revision combination checkNguyễn Gia Phong
2024-03-05Hack up brute-force decision tree constructionNguyễn Gia Phong
2024-03-05Clean up interfacesNguyễn Gia Phong
Psychic now extract patch number directly from meta conditions. Previously it was under the assumption that a patch is triggered by multiple choices. Now we allow a patch to have multiple hunks and the possibility to combine multiple patches. Internally, the code relevant diff test generation is moved under Differentiator.
2024-03-05Revert orphaned changesNguyễn Gia Phong
2024-03-05Handle conjoined metaconstraintsNguyễn Gia Phong
2024-03-05Move differentiator to separate moduleNguyễn Gia Phong
2024-03-05Execute concrete programs more eagerlyNguyễn Gia Phong
2024-03-05Implement detection of implicit return via pointerNguyễn Gia Phong
2024-03-05Implement return value detectionNguyễn Gia Phong
Values returned after reaching patch location from functions in the specified source file are now automatically accounted for differential test generation.
2024-03-05Handle revisited meta sym var when generate env varNguyễn Gia Phong
I still have no clue in some cases why they are seen more than once.
2024-03-05Retire external symbilic diffNguyễn Gia Phong
2024-03-05Implement native path condition combinationNguyễn Gia Phong
2024-03-05Fix metavar detection false negativeNguyễn Gia Phong
2024-03-05Fallback on UBNguyễn Gia Phong
This is not benefitting off UBSan, but there are too many moving parts now that a common denominator is needed for me to mentally keep track of things. (Yes, it's embarrassing that I commit less often working on software engineering research software, now I'm paying the price.)-;
2024-03-05Support 1-byte metavariablesNguyễn Gia Phong
2024-03-05Add search heuristic for patch locationsNguyễn Gia Phong
2024-03-05Avoid resolving combined SMT formulaeNguyễn Gia Phong
2024-03-05Half-bake decision clusteringNguyễn Gia Phong
2024-03-05Conclude concrete execution implNguyễn Gia Phong
2024-03-05Lay ground work for concrete executionNguyễn Gia Phong
2024-03-05Clone state more completelyNguyễn Gia Phong
2024-03-05Implement differentiator extractionNguyễn Gia Phong
2024-03-05Save exited states' formulaNguyễn Gia Phong
2024-03-05Receive instrumented revision numberNguyễn Gia Phong
2024-03-05Implement differencial test structureNguyễn Gia Phong
2024-02-29Add support to fully concretise objects if modified externallyMartin Nowack
Propagate ExternalCallPolicy to allow user-based selection.
2024-02-29Support external call concretisation policies for referenced objectsMartin Nowack
Provide an additional argument to select the concretisation policy. Fix a bug where the concretisation of a shared memory object was visible across different states by retrieving a writable object state first.
2024-02-29Refactor `ObjectState::flushToConcreteStore` to use `toConstant`Martin Nowack
Use existing `Executor::toConstant()` function to transform a symbolic byte of an `ObjectState` to its concrete representation. This will also add constraints if required.
2024-02-29Use correctly constrained constants if the memory object is fully symbolicMartin Nowack
Before, only partially symbolic variables have been concretized. Now, every object that is not fully concrete is concretized correctly this includes fully symbolic objects.
2024-02-29Correctly update symbolic variables that have been changed externallyMartin Nowack
Before, external changes to symbolic variables have not been propagated back to their internal representation. Do a byte-by-byte comparison and update object state if required.
2024-02-27Small refactorings and reformatting in callExternalFunctionCristian Cadar
2024-02-27Simplified callExternalFunction by using toConstant instead of getValueCristian Cadar
2024-02-27Extend toConstant() to take an additional boolean argument that decides ↵Cristian Cadar
whether the expression is concretised. Also changed a C string argument to std::string.
2024-02-27This commit fixes the concretization of arguments following an external call ↵Cristian Cadar
with symbolic arguments. It also introduces a new external call policy, where the symbolic inputs are left unconstrained following such a call, useful for certain external calls such as printf.
2024-02-19Rename --ptree-batch-size to --exec-tree-batch size, and ↵Cristian Cadar
--compress-execution-tree to --compress-exec-tree. Fix an incorrect reference to --write-exec-tree.
2024-02-17Fixed incorrect reference in ExternalCallWarningsCristian Cadar
2024-02-16drop llvm 9 and 10Daniel Schemmel
2024-02-08Mention default value in help text for `--strip-all` and `--strip-debug`MartinNowack
Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com> (cherry picked from commit 5d61fb6114bafbf67c59899d15e397684d4ceb28)
2024-02-08Use `std::` namespace for `uint64_t`MartinNowack
Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com> (cherry picked from commit 5d9af025ee5a01b1650f11ed0612a10357a98308)
2024-02-08Disable unsupported passes for newer LLVM versionsMartin Nowack
Similar functionality needs to be added using a new pass manager
2024-02-08Add support to `aligned_alloc` generated by LLVMMartin Nowack
Handle like `memalign` for now.
2024-02-08Add support for `Intrinsic::get_rounding` for LLVM 16Martin Nowack
`Intrinsic::flt_rounds` got removed
2024-02-08Use APIs of newer LLVM versions instead of unsupported onesMartin Nowack
2024-02-08Add support for opaque pointersMartin Nowack
2024-02-08Refactor invocation of old pass manager into legacy functionMartin Nowack
2024-01-30Change `GetConstraintLog` to work with `std::string`s instead of `char*`sDaniel Schemmel
2024-01-30Avoid generating array names in solver builders that could accidently collideMartin Nowack
If an array name ended with a number, adding a number-only suffix could generate the same name used as part of the solvers. In the specific testcase `val_1` became solver array `val_111` which collided with array `val_11` that became `val_111` as well. Using an `_` as prefix for the suffix, solves that problem in general, i.e. `val_1` becomes `val_1_11` and `val_11` becomes `val_11_1`. Fixes #1668
2024-01-30Modify getValueFromSeeds() to include more functionality and simplify its ↵Cristian Cadar
callers
2024-01-30Make Assignment::evaluate be constCristian Cadar