Skip to content

Introduce Tool.USVM in ContestEstimator, implement runUsvmGeneration - #2666

Merged
IlyaMuravjov merged 4 commits into
usvm_competitions_2024from
ilya_m/contest-usvm-tool
Oct 27, 2023
Merged

Introduce Tool.USVM in ContestEstimator, implement runUsvmGeneration#2666
IlyaMuravjov merged 4 commits into
usvm_competitions_2024from
ilya_m/contest-usvm-tool

Conversation

@IlyaMuravjov

Copy link
Copy Markdown
Collaborator

First implementation of runUsvmGeneration, not fully finished. This PR is needed for work synchronization.

@IlyaMuravjovIlyaMuravjov added ctg-enhancement New feature, improvement or change request comp-contest-estimator Issue is related to contest estimator labels Oct 27, 2023
@IlyaMuravjov
IlyaMuravjovforce-pushed the ilya_m/contest-usvm-tool branch from 557009b to 0695ab5CompareOctober 27, 2023 10:20
@IlyaMuravjov
IlyaMuravjov merged commit b0d671e into usvm_competitions_2024Oct 27, 2023
@IlyaMuravjov
IlyaMuravjov deleted the ilya_m/contest-usvm-tool branch October 27, 2023 15:18
EgorkaKulikov pushed a commit that referenced this pull request Nov 1, 2023
…tion` (#2666)
* Add `Tool.USVM` in `ContestEstimator`, implement `runUsvmGeneration`
* Remove redundant TODO
* Bump UtBot dependencies version to match USVM dependencies
* Use `UTestExecutionResult.trace` instead of `JcCoverage`
EgorkaKulikov added a commit that referenced this pull request Dec 8, 2023
* Introduce `Tool.USVM` in `ContestEstimator`, implement `runUsvmGeneration` (#2666)
* Add `Tool.USVM` in `ContestEstimator`, implement `runUsvmGeneration`
* Remove redundant TODO
* Bump UtBot dependencies version to match USVM dependencies
* Use `UTestExecutionResult.trace` instead of `JcCoverage`
* Bump ksmt version to `0.5.13`
* Hacks similar to contest 2023 ones (#2676)
* Initial implementations of the adapter from JcExecution to UtExecution (#2677)
* Some awful attempts
* Initially implemented a converter of UTestInst to UtModel
* Refactor JcToUtModelConverter basing on UTestInst2UtModel converter
* Some steps to implement JcToUtExecutionConverter
* Implement minimalistic jc to ut execution conversion, enable codegen
* Some improvements
* DeepMapper for models is used
* Corrections
* Some improvements to JcToUtModelConverter
* Further improvements to JcToUtModelConverter
* Another converter little improvement
* Improve `UtExecutionFailure` creation
* Finish implementing `JcToUtModelConverter`
* Refactor nullability in `JcToUtModelConverter` and `JcToUtExecutionConverter`
* First version of JC to UT converters without overusing `Descriptor2ValueConverter`
* Processed forgotten call method expression
* Make conversion more class-friendly (do not fail if one method cause failure)
* Make it possible to use samples in ContestEstimator
* Tested on all primitives
* contrflow tests added
* More test classes added
* Add `build/output/test/samples` to `utbot-junit-contest` test projects
* Steps to avoid duplicating statements
* Make it working correct on IntExamples.max
* Remove OptimizeImportsProcessor (seems it was not called, but a source of bugs)
* Process UTestStaticMethodCall
* Comment out includes for IDE related projects in `settings.gradle.kts`
* Avoid using burningwave to export modules on Java 8
* Fix review comments
* Fix review comments
---------
Co-authored-by: IlyaMuravjov <muravjovilya@gmail.com>
* Supporting arrays classId in Contests (#2680)
* Try to get classId from arrays with JacoDb
* Fix a bug
* Add primitive arrays to a list
* Very simple UtAssembleModel improver (#2678)
* Very simple UtAssembleModel improver
* Use `IdentityHashMap`-based cache when mapping `UtModel`s
* Improve checks for `UtAssembleModel`s created with `createInstance` method
---------
Co-authored-by: IlyaMuravjov <muravjovilya@gmail.com>
* Fix class name argument in the setField method (#2681)
Fix setField class name argument
* Fix test generation for nested classes (#2684)
* Improver `UTestRunner` initialization and shutdown (#2683)
* Add summarization for usvm-sbft (#2682)
* Add summarization for usvm-sbft
* Add summary setting to the setOption method and do small refactoring
* Use usvm samples instead of UtBot ones (#2685)
* Fix fieldId creation for UtCompositeModel (#2686)
* A tempopary hack for void TypeName processing
* A proper solution for void TypeName processing
* Add all arrays as test classes for converters
* Add samples from types
* Add samples from ternary
* Add processing of usvmExistingButNullString (#2689)
add processing of existingButNullString
* Fix classloader problem and correct class lists (exclude missing classes & classes compiled with Java 17)
* Include usvm via GitHub packages (#2687)
* Include usvm via GitHub packages
* Improve gradle script for utbot-junit-contest
* Upgrade usvm version
* Add invokes into samples
* Add several new classes to samples - Yuri said that it is enough
* Fix enum converter and add sample from enums
* Remove non-relevant TODO
* Improve `UTestValueDescriptor` to `UtModel` conversion and state change asserts generation (#2691)
* Fix compilation after USVM update (jvm-instrumentation-persistent-descriptors)
* Make `JcToUtModelConverter` construct `UtCompositeModel.origin` and assign same id to `stateBefore` and `stateAfter` models that describe same object
* Adapt `ExecutionStateAnalyzer` to deal with absence of `refId` in USVM descriptors for classes, enums, and throwables
* Adapt `ExecutionStateAnalyzer` to deal with `UtAssembleModel`s with `origin`
* Replace `UtAssembleModel`s that only use reflection with `UtCompositeModel`s, improve `constModel` for `UtArrayModel`
* Update usvm version
* Fix `constructConstArrayModelMapper` for empty arrays
* Remove non-relevant TODO
* Use jacodb with `classpathWithApproximations`
* Reduce concrete execution timeout to 1 second
* Remove redundant TODO
* Replace generics with bounds when converting to ut models
* Correct JacoDb classpath
* Correct JacoDb classpath
* Update jacodb (#2694)
* Update approximations version
* Update usvm version
* Make JcMachine's budget distributing strategy and refactor (#2695)
* SBFT'24 An attempt to support UTestGlobalMock in converters (#2690)
* An attempt to support UTestGlobalMock in converters
* Apply review fixes
* Corrected valueModels for global constructors mocks
* Introduce and use `JcMachine.analyzeAsync` in `ContestUsvm` (#2696)
* Make USVM descriptor to UtModel cache consider state kind (initial or final) (#2697)
* Update gradle script to run tests properly
* Update usvm version
* Remove strange hack to discuss later
* Add support for correct generation of inner tests
* Update usvm version
* Avoid set fields not present in `UTest` (for `UtCompositeModel`) (#2698)
* Use classpathWithApproximations
* Fix bug in `assertEquals` for `String` in codegen
* Add timeout execution conversion
* Improve logging time spent on concrete and conversion
* Make logger group repeated exceptions (e.g. "(x100) message")
* Better log `JcType.classId` fails
* Add notice about `usvmVersion` being outdated
* Actualise `JcTestExecutor`
* Update usvm version
* Fix invalid `UTestCyclicReferenceDescriptor`
* Automatically remove uncompilable test methods (#2699)
* Update path selector strategy
* Add a copy of #2627 into competitions branch
* Update approximations version
* Use symbolic result instead of concrete if it is better (#2700)
* Avoid class initialization when we evaluate ClassId
* Revert "Avoid class initialization when we evaluate ClassId"
This reverts commit 62f25ad.
* Avoid class initialization when we evaluate ClassId
* Create mocks in output values (#2701)
* Update `JcTestExecutor` to resolve mocks
* Remove approximations specific methods filter
* Update versions
* Update usvm version
* Workaround to deal with `UTestMethodCall` where `instance` is a mock
* Solver type changed
* Handle `UTestSetFieldStatement` where `instance` is a mock
* Hack for Random mocks (#2702)
* Add cast when `mock()` is called on anonymous class (e.g. `(CaseFormat) mock(Class.forName("com.google.common.base.CaseFormat$3"))`)
* Improve logging for `JcField.fieldId` failures
* Update approximations version
* jc-test-resolver: better handling of strings and classes, class constants
* Update lists as in benchmark
* Fallback to symbolic result when `runner.executeAsync()` throws exception
* Fix the list
* Fallback to symbolic result when `jcToUtExecutionConverter.convert` throws exception due to incomplete concrete result
* Fix codegen for `String(char[])` calls (use string literals when possible)
* Ignore static fields in `UTestObjectDescriptor`
* Usvm competitions 2024: jacodb persistence (#2703)
* Use jacodb persistence
* Update usvm version
* Usvm distribution for the contest (#2704)
* Add types sorting
* Drop crashed executions (#2705)
* Fix classpath (#2706)
* Avoid `<clinit>` call in `JcField.fieldId`
* Add timeout for all test with exceptions
* Removed Soot initialization (#2707)
* Disabled Soot initialization for usvm competition
* Changed logging messages for jacodb initialization
* Update usvm version
* Remove irrelevant require
* Initialize JacoDB and stat executor before starting contest, stop caching machine (#2708)
* Count "ensure JacoDB is initialized and executor is started" in force termination timeout
* Initialize JacoDB and stat executor before starting contest, stop caching machine
* Updated usvm version
* Add `maxUnknownCoverageExecutionsPerMethodPerResultType` to `settings.properties`
* Update Z3 native files paths to work with ksmt 0.5.13
* Update RD in all projects
* Update Run IDEA task to use :utbot-intellij-main
* Complete most `usvm-sbft-merge` TODOs
* Uncomment `include`s for `intellij` projects in `settings.gradle.kts`
* Add `addTestMethodMarkers` ut setting
* Revert contest hacks
* Make contest use `Tool.UtBot` by default
* Update tool settings for summary
* Update gradle properties in yml scripts
* Temporary creds
* Revert temporary creds
* Some todos in TestFrameworkManager
* bissquit: configure debug env
* add pers token
* add secret
* add token to all gradle runs
* replace ro_token by github_token
* add permissions
* change to write permissions
* return PACKAGES_RO_TOKEN var
* remove debug
* Further update of yml scripts
* Correct usvm version to fix compilation
* Disable four tests
---------
Co-authored-by: Egor Kulikov <egor.k.kulikov@gmail.com>
Co-authored-by: Kirill Shishin <73890886+tepa46@users.noreply.github.com>
Co-authored-by: Kirill Shishin <shishin_ka@mail.ru>
Co-authored-by: Yury Kamenev <yurkam447@gmail.com>
Co-authored-by: Valentyn Sobol <napster_1997@mail.ru>
Co-authored-by: Sergey Pospelov <sergeypospelov59@gmail.com>
Co-authored-by: Egor Vasiliev 00665613 <egor.vasiliev@huawei.com>
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

comp-contest-estimatorIssue is related to contest estimatorctg-enhancementNew feature, improvement or change request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant

@IlyaMuravjov