about summary refs log tree commit diff homepage
path: root/lib/Core
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-08Use `std::` namespace for `uint64_t`MartinNowack
Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com> (cherry picked from commit 5d9af025ee5a01b1650f11ed0612a10357a98308)
2024-02-08Add support to `aligned_alloc` generated by LLVMMartin Nowack
Handle like `memalign` for now.
2024-02-08Use APIs of newer LLVM versions instead of unsupported onesMartin Nowack
2024-02-08Add support for opaque pointersMartin Nowack
2024-01-30Change `GetConstraintLog` to work with `std::string`s instead of `char*`sDaniel Schemmel
2024-01-30Modify getValueFromSeeds() to include more functionality and simplify its ↵Cristian Cadar
callers
2024-01-30Make Assignment::evaluate be constCristian Cadar
2024-01-30Removed --zero-seed-extension, and merge it with --allow-seed-extension. ↵Cristian Cadar
This reworked logic also fixes a buffer overflow which could be triggered during seed extension.
2024-01-30Refactored some code related to seeding.Cristian Cadar
2024-01-30On a symbolic allocation, retrieve size from a seed, if availableCristian Cadar
2024-01-30Concretize arguments to external function calls using seeds, if available. ↵Cristian Cadar
Added a test case.
2024-01-30Concretize constants using seed values, when available. Added two tests (w/ ↵Cristian Cadar
and w/o seed extension) based on FP concretization.