Misonijnik/refactor #1

S1eGa · 2022-12-27T10:22:23Z

Summary:

Checklist:

The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.
The PR is divided into a logical sequence of commits OR a single commit is sufficient.
There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).
Each commit has a meaningful message documenting what it does.
All messages added to the codebase, all comments, as well as commit messages are spellchecked.
The code is commented OR not applicable/necessary.
The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).
There are test cases for the code you added or modified OR no such test cases are required.

[feat] Add LI object addresses concretizations

[tempfix] Add SkipNotLazyInitialized

…ger entity, that can create such these KType's.

…ld, as type can be changed dynamically, e.g. during first write into malloc'ed memory.

…bjects. Fixed type creation for C++ types, fixed tests for types and added for alignment.

WIP Prepared BlueprintSolver models recomputation, implemented BlueprintSolver::computeValidity, added few tests for LI. Added Executor::makeArray() function Added check for address during LI (that we can allocate such objects in memory). Added test for this check. Slight improvements in API of ConcretizationManager. Speed up of executeMemoryOperation procedure by changing to check. Fix for check before lazy object initialization (evaluate -> simplifyExpr). Fix tests for LI. Added check if address can reference to any memory location after resolve without LI. operations from AddressSpace now return lists of MemoryObjects's IDs. Will be useful in work with symbolisc sizes. executeMemoryOperation: inline replaced with mass to fix seeding mode. Improved naming construction for makeArray(). Symbolic sizes. Constant sizes of Array's replaced with ref<Expr>. Fixed unittests. Implented queries in BlueprintSolver and additional query to get minimal possible value in SolverImpl WIP. Implemented functions to make sizes recomputations. Added dependency in IndependentElementSet between size and address of arrays with symbolic sizes. Lazy initialization now use objects of symbolic size. Added state updating during execution. Fixed state updates. Added address generator. WIP WIP WIP [feat] Separate `compare` and `equals` [fix] ValidityCore API Fixes [fix] ValidityCore API Fixes. Added simple test for objects of symbolic size. WIP. Fixed outOfBound case check in execMO, fixed pathOS test. Completed implementations of requests in BlueprintSolver, added verification that assignments from queries contain all symcretes. Fixed bug with adding constraint in ConcretizationManager. WIP toUnique function renamed to trygetWeight and moved to TimingSolver Added tests, added resolveOneIfUnique method to find meomeryo object for symcrete address. Still have failing tests (WIP). Test fixes Unnecessary commit: changed logic for solver to investigate perfomance regression in TwoObjectsInitialization.c test. Slighlty optimized getMinimalUnsignedValue function. Rewrited allcoate function in Executor: now we are trying to optimize sum of sizes instead of single size. Fixed query printing in smt2 notation Fixed naming of variables in SMT2 notation. Fixed error handling during lazy initialization Fixed model receiving in memory allocation. Added bound for symbolic sizes to model malloc's behavior. WIP. Fixed expression widths in computeMinimalUnsignedValue. Added forks during memory allocations to model NULL result of malloc during huge allocations. WIP. Fix perfomance, bug in MO tracking. WIP WIP. Fixes for ConcretizationManager. Fixed output for smt2 loggers, updating ConstraintManager for klee_prefer_cex. Fixed tests. Separated options for constant and symbolic sizes. Changed ObjectState copying for new MemoryObject. Extending constantValues array after ObjectState recomputation (possibly buggy area). WIP. Arrays for constant objects replaced with constant arrays. [feat] Add read optimization WIP. Sparse structure. WIP. Incomplete sparse structure. WIP. Implemented iterator for sparse stotage. Optimized bounds check pointer for case with equals sizes WIP. Better bound approximation during computation of minimal unsigned value. Slightly optimized minimiztion function: now to find right border we can make a binary search WIP. Implemented check function for SolverBlueprint. One more optimization added for computeMinimalUnsignedValue --- we can use values from solver when move right borders to left in binary searches. WIP. Fix for Independent solver. Retracted changes with value optimization for binary search. Added caching in SolverBlueprint.

The implementation is based on KLEE-float. Supported llvm math intrinsic functions related to floating-point. Added ENABLE_FP and FP_RUNTIME options to CMake. Provided an ability to switch between Z3Builder implementations. Building KLEE without -DCMAKE_ENABLE_FLOATING_POINT does not change the core. Changed scripts and github actions to launch fp-tests.

Use `createCachedExpr`

…iable for stdin buffer size to ktests. Disabled tests for now broken klee-replay and klee-zesti (unused).

Implement getc, fgetc, fread, fgets, getchar, gets, putc, fputc, fwrite, fputs, putchar, puts

(cherry picked from commit 99c522b)

[feat] Add releaseStates

ocelaiwo added 5 commits November 26, 2022 11:35

[feat] Add pointer support in KTest

f94df87

[chore] Update .gitignore

5b8035a

[extra] Add constraint dumping

0b60746

[refactor] Change test generation procedure

b2d9288

[fix] Fix getRange in Solver

1f353e1

S1eGa force-pushed the misonijnik/refactor branch 2 times, most recently from 975eb21 to 35b6fc8 Compare December 27, 2022 12:10

ocelaiwo and others added 21 commits February 1, 2023 09:05

[feat] Add lazy initialization

dfc5f9e

[feat] Add GuidedSearcher

9fdd9e9

[extra] Add state logging

2156d49

[feat] Add Expr::toString

200818a

[feat] Add finObjects

cbc2e66

[feat] Separate compare and equals

abf5127

[feat] Add API for validity cores

8f8ee2d

[feat] Add read optimization

cb0e2dd

[refactor] Add makeArray

9aecf98

[feat] Add concretization manager and solver

c5f5f21

[feat] Add LI object addresses concretizations

Add conflict detector to simplifyExpr function

1a2d57d

Add HashConsing to expessions

73b2088

[test] Show elapsed wall time for each test

0fcb374

[tempfix] Change address resolution predicate to its old ver

4c180a8

[tempfix] Add SkipNotLazyInitialized

Implemented classes for types in type system. Added handling TypeMana…

6bcd3c1

…ger entity, that can create such these KType's.

Integrated type system. ObjectStates own type of memory, that they ho…

9e7f292

…ld, as type can be changed dynamically, e.g. during first write into malloc'ed memory.

Added type system support for C and (partially) C++ languages.

8b89755

Added tests.

6670807

Fixed __ctype_b_loc type and removed fix for skipped objects.

9945abc

Added constaints for pointers: for alignment and size of underlying o…

57bf059

…bjects. Fixed type creation for C++ types, fixed tests for types and added for alignment.

[fix] Consider all symbolic pointers during setInitializationGraph

be904e6

S1eGa force-pushed the misonijnik/refactor branch from 35b6fc8 to 865b96f Compare February 12, 2023 19:27

S1eGa and others added 20 commits February 13, 2023 01:18

Bug fixes. Explicit logic choose for solver.

ee85923

Add build script and github action

23cabdf

[fix] KLEE floating-point support

c28af33

Use `createCachedExpr`

Integrate sanitizer

42c216a

Prepared KLEE for launching it with POSIX runtime. Added symbolic var…

888c82d

…iable for stdin buffer size to ktests. Disabled tests for now broken klee-replay and klee-zesti (unused).

Add timeouts

882c2fb

Added possibility of installing as a library and launching as a function

2ef2dcf

Several fixes for utbot

2ac84b5

Add interactive mode

1301313

Add intrinsic replacement for 'sqrt'

f02b748

Fix typo

a0c1551

Add TimeoutPerTest for generation tests for project

fc3a3b0

Add support stdin/stdout with interactive mode

6b344df

Implement getc, fgetc, fread, fgets, getchar, gets, putc, fputc, fwrite, fputs, putchar, puts

add constraint

5b37cdb

Inline asm external call

c14b7e7

(cherry picked from commit 99c522b)

[fix] Fix iterator dereferencing over last block in a function

8ce5d92

Add support fopen and add counter of read/write bytes in files

b6f044c

[feat] Add check instruction coverage

aa84667

[feat] Add releaseStates

[tempfix] Write addresses of MOs in KTest

f0abdbc

S1eGa force-pushed the misonijnik/refactor branch from 865b96f to f0abdbc Compare February 12, 2023 22:22

Attempted to add probe to choose theory.

f7a4733

S1eGa force-pushed the misonijnik/refactor branch from 5afd543 to f7a4733 Compare February 14, 2023 16:07

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Misonijnik/refactor #1

Misonijnik/refactor #1

S1eGa commented Dec 27, 2022

Misonijnik/refactor #1

Are you sure you want to change the base?

Misonijnik/refactor #1

Conversation

S1eGa commented Dec 27, 2022

Summary:

Checklist: