Merge latest changes from rework #488
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Updated to Java 17
Initial prototype for rework
Updated Event to have SourceLocation metadata
Improved documentation. Renamed ParseId back to OriginalId (not all programs are constructed by a parser).
Add Metadata
Simplified Filter code.
Refactored Tags
Rename INonDet.getType() to .getNonDetType()
…n,BigInteger,BigInteger)
CTLZ retains its operand type
[Rework] ExprInterface.getType()
Add Program.addConstant(INonDet) Add ProgramBuilder.newConstant(IntegerType,boolean) Add ProgramEncoder.encodeNondeterministicBounds() Add INonDet.setMin(BigInteger) Add INonDet.setMax(BigInteger) Add INonDet.setSourceName(String) Replace INonDet(int,IntegerType,boolean,BigInteger,BigInteger) with INonDet(int,IntegerType,boolean) Fix IllegalFormatConversionException in INonDet.toString()
* Renamed RegReaderData to RegReader Updated RegReader to return a set of (new) Register.Read objects. Updated all the users of RegReader Made MemEvent a RegReader. * Removed dead comments Updated some comments Simplified DynamicPureLoopCutting code Simplified ExecutionModel code * Improved Join.toString "Fixed" a problem in ExecutionModel * Removed unnecessary "implements RegReader" from Store and Xchg Replaced (few) tabs by whitespaces * Fixed Xchg not returning correct address dependencies. Added warnings when encountering reads of uninitialized registers in an execution.
* Renamed RegReaderData to RegReader Updated RegReader to return a set of (new) Register.Read objects. Updated all the users of RegReader Made MemEvent a RegReader. * Removed dead comments Updated some comments Simplified DynamicPureLoopCutting code Simplified ExecutionModel code * Improved Join.toString "Fixed" a problem in ExecutionModel * Removed unnecessary "implements RegReader" from Store and Xchg Replaced (few) tabs by whitespaces * Renamed Event to AbstractEvent * Introduced Event interface Renamed old abstract Event class to AbstractEvent Updated all code to work over the Event interface * Made RegReader and RegWriter extend new Event interface * Fixed Xchg not returning correcte address dependencies. Added warnings when encountering reads of uninitialized registers in an execution.
Renamed RMWFetchOpBase.java to RMWOpResultBase to clearly communicate that it is more generally usable.
Rmw base classes & refactor
# Conflicts: # .github/workflows/maven.yml # dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprSimplifier.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/VisitorBoogie.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/lisa/RMW.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/AtomOp.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/FenceWithId.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/RedOp.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/tso/Xchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/RMWAbstract.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicAbstract.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicCmpXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicFetchOp.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicLoad.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicStore.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicThreadFence.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMFence.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLoad.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLock.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMStore.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMUnlock.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/RMWAddUnless.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/RMWCmpXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/RMWFetchOp.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/RMWOp.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/RMWOpAndTest.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/RMWOpReturn.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/RMWXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmAbstractRMW.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmCmpXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmRMW.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/visitors/EventVisitor.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/CoreCodeVerification.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadCondJumps.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Simplifier.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SparseConditionalConstantPropagation.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorBase.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorIMM.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPTX.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorRISCV.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorTso.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertBasic.java
* Remove BExpr.isFalse(), BExpr.isTrue() Remove BConst.FALSE, BConst.TRUE * Remove IExpr.getBase() * Remove IExpr.isInteger() and .isBV() * Remove usage of IExpr * Register is no IExpr * Add encoding of boolean data * fixup! Fix GTE in makeGreaterOrEqual * Add ExpressionFactory.makeCast(Expression,Type) Rename .makeBoolean(Expression) into makeBooleanCast
Added functions + function-specific events (e.g. Return and Call) Simplified BoogieVisitor and related parsing classes.
* Made FunctionType constructible via TypeFactory Added new Normalizer class to allow for normalization/canonicalization of object instances * Simplified ProgramBuilder and made it more robust Fixed PTX litmus test that referenced undefined threads. * Added ProgramBuilder factory methods All parser visitors now create a ProgramBuilder with correct source language and target architecture set. * Threads now always require a function type (automatically provided by the ProgramBuilder) * Added SymbolTable class (just a HashMap with String keys for now). Improved function validation done by ProgramBuilder. * Added VisitorBoogie.getOrNewEndOfScopeLabel and ProgramBuilder.getEndOfThreadLabel * Transformed helper classes to records and moved them to VisitorBoogie. * Removed VisitorBoogie.currentThread * Added Event.replaceAllUsages Use Event.replaceAllUsages in Compilation of pthread_create Removed matcher annotation events * Reworked pthread_create/join handling to more closely reflect their real semantics.
Added proper type checks and conversions to avoid implicit casts: * Outline EncodingContext.makeVariable(String,Type) * SmackPredicates create integer casts * Start expects boolean register * RMWCmpXchgBase expects boolean register * Add Function.getOrNewRegister(String,Type) * Assertions use boolean registers * AtomicCmpXchg uses boolean registers * Add type-safety * Remove ambiguously-typed integer value factories. * Fix type-unsafe assignments in LKMM-related parser and compiler * Fix type-unsafe assignments in LKMMAddUnless and LKMMOpAndTest * Fix model value parser in WitnessGraph Fix type-unsafe assignments in VisitorLitmusLISA * Fixup --------- Co-authored-by: Thomas Haas <[email protected]>
* Add Inlining * Fixes Proper renaming in Inlining Deep copy of DirectFunctionCall * Inlining does not skip entry * Function is an Expression * Function expressions are used in the parser. Pthread_create and join are parsed and calls to them are generated as expected outside of inline mode. * Simplified/Generalized parsing of special functions. * Add LlvmCmpXchg.setStructRegister(int,Register) * Add ThreadCreation * Simplified Pthread.Start event * Some fixes in ThreadCreation pass * Reworked ThreadCreation * Made VisitorBoogie recognize more functions as user-declared Added new Events for passing parameters across threads, and updated ThreadCreation pass to generate them. Updated CoreCodeVerification to recognize new threading-related events. Updated inlining pass to generate annotations around inlined calls. * Made VisitorBoogie recognize more functions as user-declared Updated Alias analysis to recognize new threading-related events Refactor/renaming * Added Event.replaceBy(List<Event>) Added new thread events to EventFactory Updated ThreadCreation to not generate Pthread events Fixed issue in ExecutionModel with boolean valued memory accesses. * Added proper tid propagation to ThreadCreation (temporary solution) * Added .bpl files for three more unit tests. These tests run correctly with the new ThreadCreation pass, but still fail without, so they are disabled for now. * Some refactoring * Added handling for thread-local variables. Added new thread_local.c unit test * Proper naming of generated dummy registers for thread creation * Improved printing of threads. Better automatic naming for nameless threads. * Fixed minor issue with undefined initialize function * Improvements in ThreadCreation * Moved static memory initialization from the parser into a pass. * Removed thread creation from parser (commented out for testing) Adding logging to ThreadCreation * Added parsing error when encountering main without body. Adding missing StaticMemoryInitializer pass into ProcessingManager * Enabled 3 more unit tests. First cleanup pass of Parser code (removing inline mode). * Full cleanup of Boogie parser * Deleted now unused Pthread events * Fixed ExecutionModel not recognizing new ThreadArgument event (this caused only warnings, but no semantic errors). * Various Refactoring * Fixed accidental bug * Implemented first set of feedback changes. * Removed unused code. Added FIXME for recursion handling --------- Co-authored-by: Thomas Haas <[email protected]>
* Add IntrinsicsInlining * Added new nondet_loop.c code + unit test. --------- Co-authored-by: Thomas Haas <[email protected]>
* Various minor fixes: - Add OIds in ThreadCreation - Copy metadata from call statements into marker events when inlining. - Fixed ExecutionModel printing warnings for ThreadArguments - Renamed FunCall/FunRet to FunCallMarker/FunReturnMarker to distinguish them from proper call/return events. - Made more internals of AbstractEvent private. * Fixed ExecutionStatus to work with boolean registers. * Removed unnecessary usages of ExecutionStatus. Use boolean type register for ExecutionStatus whenever possible. * Improved logging * Changed ExecutionGraphVisualizer to also create nodes for threading-related events. Increased weighting of po-edges * Added handling of pthread_exit * Changed heuristic to detect whether Smack created static initialization. Avoid creating memory for procedure address constants. * Refactoring. RelationAnalysis now logs #Relations and #Axioms
|
Do you wanna keep the |
Ohhh I fix it locally, but forgot to push. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR simply merges the current status of
development_rework(minus the code in the prototype folder and the LLVM grammar and parser) intodevelopment. The code has already been reviewed (see #470 , #471, #475, #478, #479, #481, #483, #485, #487).