Merge latest changes from rework #497

Updated to Java 17

Initial prototype for rework

Updated Event to have SourceLocation metadata

…lasses.

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

…ype)

[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.

Program.getConstants() (rework)

* Replaced MemEvent by an interface MemoryEvent. The old MemEvent class is now AbstractMemoryEvent. * Removed MemoryEvent.canRace()

Updated MemoryEvent to return MemoryAccess (work-in-progress) Changed AbstractMemoryEvent to SingleAddressMemoryEvent, which now serves as a common implementation for all single-address memory events.

…ED_CAST

…ndle Init and Store

Remove IValue.ONE and .ZERO Remove EventFactory.newFakeCtrlDep(Register,Label) Change signatures of some parser helper methods

SCCP propagates constants over casts

…eIntegerCast(Expression,IntegerType,boolean)

[Prototype] Core memory events

Removed MemoryEvent.getMo()

…form of abstract base classes. Updated most language-level events to use the new event/common package instead of inheriting from core events (work-in-progress) Added MemoryCoreEvent interface (not used yet).

ExpressionFactory

…added MemoryOrder metadata attached

Minor fixes

# Conflicts: # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusX86.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/tso/Xchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractMemoryEvent.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Init.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Load.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/MemoryEvent.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Store.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/rmw/RMWStore.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/rmw/RMWStoreExclusive.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/AtomicXchg.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/LKMMLockRead.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLockWrite.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/RMWAbstract.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/SrcuSync.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/LlvmLoad.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/LlvmStore.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/Create.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/InitLock.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/Lock.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/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/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java

…ompilations) Reformatted files

Extended EventVisitor by visitMemCoreEvent Simplified SparseConditionalConstantPropagation again

Cleaned up formatting/commenting in compilation visitors.

Add MemoryAccess and MemoryCoreEvents

Added CustomStringify metadata (name is subject to change). Event.toString now uses the metadata of available and otherwise falls back to "defaultString"

…on-core code. This is temporarily used for debugging purposes.

Improved error message of CoreCodeVerification

Made VisitorLKMM compile LKMMFence down to a core-level Fence.

…se resp. StoreBase. This reduces code duplication

…imple stores). Made LKMMUnlock non-core. Enabled CoreCodeVerification.

Made CondJump, ExecutionStatus, EndAtomic, and RMWStore EventUsers Extended Event to be able to track users.

Cleaned up CondJumps usage "Label.getJumpSet"

Event printer & reduced core

Reduced usages of Event.setSuccessor and Event.getSuccessor to instead use Event.insertAfter if possible.

# Conflicts: # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractEvent.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/CondJump.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/EndAtomic.java

Added a new error raised by ProgramBuilder.addChild when accidentally adding an already added event.

…a new EventUser.moveUserReference helper function. Fixed CondJump automatically setting a thread on construction.

… under special circumstances. Added Event.forceDelete and replaced some usages by Event.tryDelete (work-in-progress)

Event user & more robust CFG handling

# Conflicts: # dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/ExecutionStatus.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/RMWAbstract.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/visitors/EventVisitor.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/wmm/analysis/RelationAnalysis.java

Merge development into development_rework

Renamed RMWFetchOpBase.java to RMWOpResultBase to clearly communicate that it is more generally usable.

…ed event names.

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

* Added FunctionProcessor interface. Transformed many ProgramProcessors to FunctionProcessors Moved ThreadCreation to after compilation and unrolling (can handle pthread_create in loops). * Included dat3m.h to some tests (+ regenerated their .bpl files). * Register now contains a Function rather than a functionId. Removed Register.NO_FUNCTION. * Renamed EventIdReassignment to IdReassignment. It now also reassigns function ids, making sure that threads get their Ids first. * Added Printer.Mode to only print threads, functions, or both. Also added short output for skipped init threads when printing.

Add proper control-flow dependencies between spawned threads and their spawners/creators

* Generalized ThreadCreation to allow dynmaic joining. * Cleaned up ThreadCreation's handling of pthread_join. Removed unsound propagation code. Removed must-rf edges related to pthread_join (hard to establish and exploit with dynamic thread joins).

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Merge latest changes from rework #497

Merge latest changes from rework #497

Commits on May 12, 2023

Commits on May 13, 2023

Commits on May 16, 2023

Commits on May 17, 2023

Commits on May 19, 2023

Commits on May 21, 2023

Commits on May 26, 2023

Commits on May 27, 2023

Commits on Jun 2, 2023

Commits on Jun 5, 2023

Commits on Jun 6, 2023

Commits on Jun 7, 2023

Commits on Jun 8, 2023

Commits on Jun 9, 2023

Commits on Jun 12, 2023

Commits on Jun 13, 2023

Commits on Jun 15, 2023

Commits on Jun 18, 2023

Commits on Jun 19, 2023

Commits on Jun 20, 2023

Commits on Jun 21, 2023

Commits on Jun 22, 2023

Commits on Jun 24, 2023

Commits on Jun 25, 2023

Commits on Jun 28, 2023

Commits on Jun 29, 2023

Commits on Jul 4, 2023

Commits on Jul 5, 2023

Commits on Jul 11, 2023

Commits on Jul 13, 2023

Commits on Jul 15, 2023

Commits on Jul 27, 2023

Commits on Jul 28, 2023

Commits on Aug 3, 2023

Commits on Aug 8, 2023