Functions (Part 1) #470

ThomasHaas · 2023-06-22T12:52:34Z

This PR introduces a Function class. Events are now part of a Function rather than a Thread.
However, a Thread inherits from Function, so events can be part of a thread if the function happens to be a thread.

While adding/parsing functions, I noticed that the boogie parser is a nightmare I needed to fix first. So most of this PR is now dedicated to cleaning up VisitorBoogie and its related components.
An overview of the changes:

VisitorBoogie and its related components are far simpler now
VisitorBoogie can parse in inline mode and no-inline mode (the former mode matches with what we are doing right now)
The parser currently runs once in inline mode and once without, generating proper functions rather than threads.
However, the generated functions are incomplete (contain placeholders) and unused in this PR. A future PR (Part 2?) will change this. For the purpose of reviewing this PR, code inside !inlineMode-conditionals can be disregarded and parts marked by "// TODO ---- Test Code ----" can be assumed to be commented out (those are for the future PR).
Issue Issues with Duplicated Labels #260 should be fixed.
Scope-prefixes reset per thread now, i.e., they start from 0: per thread. This was previously not the case because of the above issue with duplicate label names.
The parser creates no more unused dummy registers in functions/threads.

Thread inherits from Function

…on() if possible

Added Program.getFunctions() (unused for now)

…thod. Added function call events

Added Return event Moved all function related code into its own package (only temporarily) Generalized Function to take parameter names as input and generate "parameter registers".

Fixed outdated comments

…ents.

Added LlvmCmpXchg.setStructRegister (special case) Added missing transformExpressions implementation to lisa.RMW

Generalized Function.append

Added getScopedName(String) to VisitorBoogie

Reformatted boogie parser code

Made use of VisitorBoogie.addEvent when possible.

# Conflicts: # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/LkmmProcedures.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/LlvmProcedures.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/VisitorBoogie.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/EqualityAliasAnalysis.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/PTXFenceWithId.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/linux/LKMMLoad.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/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/llvm/LlvmAbstractRMW.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmCmpXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Simplifier.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/specification/AssertBasic.java

Made label-tracking context-aware so that different threads can have labels with the same name.

…on and parameter parsing.

Refactor/renaming Moved handling of abort() and reach_error() into StdProcedures/SvcompProcedures

Functions now get proper ids. Updated printer to include function/thread ids in the output.

…pe" declarations.

…rings)

# Conflicts: # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/boogie/LlvmFunctions.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/boogie/SmackPredicates.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/LkmmProcedures.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/PthreadsProcedures.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/StdProcedures.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/SvcompProcedures.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/VisitorBoogie.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/Register.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/Thread.java # dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java

dartagnan/src/main/java/com/dat3m/dartagnan/expression/type/FunctionType.java

hernanponcedeleon · 2023-06-29T12:22:25Z

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java

-    public void initThread(String name, int id){
-        if(!threads.containsKey(id)){
+    public void initThread(String name, int id) {
+        if(!functions.containsKey(id)){
            Skip threadEntry = EventFactory.newSkip();


entry sounds like a better name since this is not necessary a thread.

Not sure if it make sense in the current state of this PR, but shouldn't we at some point add FunctionEntry and FunctionExit nodes (i.e. events)?

entry sounds like a better name since this is not necessary a thread.

It is necessarily a thread that gets created. There is a separate initFunction method that creates functions.

Not sure if it make sense in the current state of this PR, but shouldn't we at some point add FunctionEntry and FunctionExit nodes (i.e. events)?

Why? I don't think functions need any of that, because (1) you can have a empty (= no body) functions and (2) we have a Return event to exit functions.

In a CFG you would normally have entry/exit nodes. The Return event is exactly what I had in mind (I wrote the comment before going over all changes). Not sure if having a specialized Entry extends Skip would make sense or bring any advantage.

Currently, all function bodies start with a $bb0 label. And I think this will also holds true for LLVM code.
At least for now, a dedicated entry node just has disadvantages if you allow for empty-bodied functions. Because on an empty function, f.appendEvent(e) would need to implicitly create an entry event before appending e.

Actually, now that I think about it, we will probably need a marker of sorts to distinguish between "empty body" and "no body". Maybe a dedicated FunctionEntry event could serve this purpose. But I would do this in a PR that does add proper support for functions (i.e. part 2 or 3, depending on how difficult it gets :)).

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractEvent.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/Lock.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/Unlock.java

Updated the name of parameters in ProgramBuilder methods Updated FunctionType.toString

hernanponcedeleon · 2023-06-29T16:47:09Z

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]>

ThomasHaas added 30 commits June 22, 2023 14:27

Added simple Function class + FunctionType (work-in-progress)

a92dbbd

Thread inherits from Function

Introduced Event.get/setFunction.

299520f

First pass to replaced usages of Event.getThread() by Event.getFuncti…

ba73013

…on() if possible

Replaced more usages of getThread() by getFunction().

3800320

Added Program.getFunctions() (unused for now)

Made Event.getCopy non-optional: all events have to implement this me…

e419aae

…thod. Added function call events

Added VoidType

6be1b83

Added Return event Moved all function related code into its own package (only temporarily) Generalized Function to take parameter names as input and generate "parameter registers".

Return event has now optional return value.

81516b9

Fixed outdated comments

Added Event.transformExpressions method and implemented it for all ev…

7492655

…ents.

Simplified SCCP using Event.transformExpressions

2d4a1be

Fix SCCP

38ef3e7

Added RegWriter.setResultRegister

4e1823c

Added LlvmCmpXchg.setStructRegister (special case) Added missing transformExpressions implementation to lisa.RMW

Fixed Function.new

88fc1a9

Improved Function.toString()

f2abf0e

Extendend EventFactory with new function call/return events.

f2f20f5

Added testing code for function parsing ( very hacky code)

0152c2a

Added test code to construct Return events.

585ff4d

Added AbortIf

0ce61f4

Generalized Function.append

Generated AbortIf for non-inlined functions

d353a04

Added getScopedName(String) to VisitorBoogie

Updated Boogie Parser to use getScopedName everywhere

a33d544

Reformatted boogie parser code

Added last missing call to getScopedName

321876d

Added utility functions to VisitorBoogie (in particular addEvent).

6f66ce8

Made use of VisitorBoogie.addEvent when possible.

Use VisitorBoogie.addEvent everywhere

b6b0d3f

More refactor/simplification of Boogie parsing

1fbdb72

Even more refactor/simplification of Boogie parsing

ef504f0

Fixup after merge

92d7a0e

Fixed Lkmm/LlvmProcedure creating unnecessary registers

7deabf0

Removed printing code for CI debugging

592acd0

Re-added support for 8/16-bit LLVM atomics

2f82320

More simplification in VisitorBoogie

fd00937

Made label-tracking context-aware so that different threads can have labels with the same name.

ThomasHaas added 3 commits June 26, 2023 13:48

Simplified & clarified Boogie function call handling

d60859b

Fixed accidental skip of "init mode" in VisitorBoogie

6350985

More simplifications in BoogieVisitor, mostly regarding thread creati…

acb38f7

…on and parameter parsing.

ThomasHaas changed the title ~~[DRAFT] Functions~~ [DRAFT] Functions (Part 1) Jun 27, 2023

ThomasHaas added 5 commits June 27, 2023 14:40

Fixed argument passing

01dfad0

Refactor/renaming Moved handling of abort() and reach_error() into StdProcedures/SvcompProcedures

Functions have no default body anymore.

012a791

Functions now get proper ids. Updated printer to include function/thread ids in the output.

Added VarDeclaration helper record to simplify parsing of "varName:ty…

a4dff82

…pe" declarations.

General cleanup (removed comments, fixed formatting, updated wrong st…

4241620

…rings)

Disabled printing

b81ade4

ThomasHaas changed the title ~~[DRAFT] Functions (Part 1)~~ Functions (Part 1) Jun 28, 2023

ThomasHaas added 3 commits June 28, 2023 16:23

Fixup!

bb206c4

Fixed wrong cast

0017365

hernanponcedeleon reviewed Jun 29, 2023

View reviewed changes

ThomasHaas added 3 commits June 29, 2023 16:12

Removed getResultRegister from Pthread Lock/Unlock

d6d5aac

Moved transformExpressions from Event into RegReader

08ec191

Added Precondition to Function.new

8f1ed41

Updated the name of parameters in ProgramBuilder methods Updated FunctionType.toString

ThomasHaas merged commit f6cd58a into development_rework Jun 29, 2023
1 check passed

ThomasHaas deleted the functions branch June 29, 2023 16:59

hernanponcedeleon mentioned this pull request Jul 15, 2023

Merge latest changes from rework #488

Merged

hernanponcedeleon mentioned this pull request Jul 26, 2023

Issues with Duplicated Labels #260

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Functions (Part 1) #470

Functions (Part 1) #470

ThomasHaas commented Jun 22, 2023 •

edited

Loading

hernanponcedeleon Jun 29, 2023

ThomasHaas Jun 29, 2023

hernanponcedeleon Jun 29, 2023

ThomasHaas Jun 29, 2023

ThomasHaas Jun 29, 2023

hernanponcedeleon commented Jun 29, 2023

Functions (Part 1) #470

Functions (Part 1) #470

Conversation

ThomasHaas commented Jun 22, 2023 • edited Loading

hernanponcedeleon Jun 29, 2023

Choose a reason for hiding this comment

ThomasHaas Jun 29, 2023

Choose a reason for hiding this comment

hernanponcedeleon Jun 29, 2023

Choose a reason for hiding this comment

ThomasHaas Jun 29, 2023

Choose a reason for hiding this comment

ThomasHaas Jun 29, 2023

Choose a reason for hiding this comment

hernanponcedeleon commented Jun 29, 2023

ThomasHaas commented Jun 22, 2023 •

edited

Loading