Various fixes/cleanup #487
Conversation
- 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.
Use boolean type register for ExecutionStatus whenever possible.
…elated events. Increased weighting of po-edges
dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractEvent.java
Show resolved
Hide resolved
| @@ -89,10 +87,9 @@ public void generateGraphOfExecutionModel(Writer writer, String graphName, Execu | |||
| } | |||
|
|
|||
| private boolean ignore(EventData e) { | |||
| return !e.getEvent().hasMetadata(SourceLocation.class) && !e.isInit(); | |||
| return false; // We ignore no events for now. | |||
There was a problem hiding this comment.
isn't this affection our current witness generation?
There was a problem hiding this comment.
Yes, it affects it. The only events that have no source location are the two events used to start/end a thread.
I think we should print them, despite them not having a source location.
You should probably run the code to look at both the new logging output and the generated witnesses.
If you dislike anything about that, I can change it.
There was a problem hiding this comment.
I thought we were ignoring everything instead of not ignoring anything. I will do some manual testing tomorrow and check
There was a problem hiding this comment.
Some addresses get a null representation in graphviz witnesses, see e.g. ticketlock with -DACQ2RX
There was a problem hiding this comment.
Hmm, the NULL entries should already have been there before.
It seems we simply do not construct init events for the members of the lock variable, cause Smack fails to init properly.
That problem should already exist on development.
While debugging, I noticed that we now do create a lot of memory objects related to smack internals.
I will try to fix this.
There was a problem hiding this comment.
I fixed both issues. We now assume that Smack generated correct static initialization code IFF it generated at least one init value. This might be wrong if there is the possibility that Smack generates some but not all initialization of a memory object (i.e., it generates partial initialization).
| case "pthread_mutex_destroy": | ||
| // TODO: These are skipped for now | ||
| VisitorBoogie.logger.warn( | ||
| "Skipped call to {} because the function is not supported right now.", funcName); | ||
| return true; | ||
| case "pthread_exit": | ||
| final Expression retVal = (Expression) ctx.call_params().exprs().expr(0).accept(visitor); | ||
| visitor.addEvent(EventFactory.newFunctionReturn(retVal)); |
There was a problem hiding this comment.
is it true that a pthread_exit acts simply as a function return?
There was a problem hiding this comment.
In principle it is reversed: a return acts as a pthread_exit I believe. Not that it really matters: both terminate the thread and produce a value that can be read by pthread_join.
Edit: There seems to be a slight difference in practice in that return unwinds the stack while pthread_exit does not, so that scope-allocated stuff is not automatically freed in the latter case (only relevant for C++ I believe?). Either way, semantically return and pthread_exit are identical.
Avoid creating memory for procedure address constants.
RelationAnalysis now logs #Relations and #Axioms
|
LGTM |
Add proper functions #470 Generic Registers #471 Rmw base classes #475 Type Safety #478 Parsing & thread creation #479 Unit tests for thread creation #481 Move memory initialization, inlining, and thread creation from the parser to processing passes #483 Inlining of nondet_int #485 Various fixes/cleanup #487 --------- Co-authored-by: Thomas Haas <[email protected]> Co-authored-by: René Pascal Maseli <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>
This PR adds minor fixes and cleanup:
ExecutionStatusis printed asnot_exec(...)instead ofstatus(...)to more clearly convey its semantics.ExecutionStatusnow can assign to boolean registers. If possible, compilation schemes were updated to use boolean registers. Also, in many cases theExecutionStatuswas removed from compilation cause it served no purpose (it was dead code).DirectFunctionCall.copy()where metadata was not copied over. This causedSourceLocationinformation to get lost.Inliningpass preserves more metadata when inlining code. TheFunCallandFunRetcode annotations have been renamed toFunCallMarkerandFunReturnMarkerto better distinguish them from actual calls/returns.ThreadCreationnow assignsOriginalId(which was previously done after parsing).RelationAnalysiswas cleaned up.ExecutionModelwould complain about uninitialized registers if they were assigned by aThreadArgument.