implement single return invariant (diamond shaped procedures) #178

ailrst · 2024-02-16T05:29:48Z

Adds return statement and ensures a procedure always has exactly one return statement (which may not always be reachable).

To simplify this we also make the entryBlock and returnBlock of a procedure always defined. The returnBlock must contain a return, and the entryBlock is assumed to have no blocks that jump to it.

If a procedure is constructed with no blocks then it consists of an empty entryBlock that jumps directly to the returnBlock.
Adds internalBlocks containing the mutable block list
Now Procedure.blocks returns entryBlock ++ internalBlocks ++ returnBlock.
Removes all the cruft maintaining the entry and return blocks and creating them from the added blocks in case they are removed: they are now not allowed to be removed.
Adds Procedure.hasImplementation method to define whether the procedure is a stub.
the addBlock and removeBlock methods on procedure ensure that the only return statement in the procedure is the one in the return block by:
1. When a block is added its return call is replaced with a GoToReturn(returnBlock) (where gotoReturn is a subclass of GoTo that only allows one target that cannot be changed).
2. When a block is removed its return call is replaced with a Return again.

make the presence of begin and end block invariant in procedure

l-kent · 2024-02-29T00:26:48Z

src/main/scala/ir/IR_Dsl.scala

You've duplicated this since it was moved

l-kent · 2024-02-29T23:57:35Z

src/main/scala/ir/IRCursor.scala

  // TODO: this method doesn't require aftercall blocks only have 1 incoming jump 
  def isAfterCall : Boolean = p.incomingJumps.nonEmpty && p.incomingJumps.forall(_.isAfterCall)

  def begin: CFGPosition = p
  def end: CFGPosition = p.jump

+extension (p: Command)
+  def isReturn: Boolean = p.parent.parent.returnBlock.jump eq p


shouldn't this just be replaced entirely since we can match on Return now

l-kent · 2024-03-01T00:01:15Z

src/test/scala/SystemTests.scala

-        case (false , false, true) => "Test passed"
-        case (_, _, false) => "Prover error: unknown result: " + boogieResult
+        case (false, false, true) => "Test passed"
+        case (_, _, false) => "Prover error: unknown result"


Why change this, this was useful

This was probably unintentionally removed in a merge

l-kent · 2024-03-01T00:03:22Z

What's the point of mandating empty entry blocks? Doesn't this just make Procedure completely redundant as a node in the CFG? It doesn't really make sense to have both?

ailrst · 2024-03-01T01:12:25Z

Rather than requiring it has no statements I think its more important to require it has no incoming (intraprocedural) jumps and only one outgoing jump.

The entry block cannot be added/removed/replaced like the rest of the blocks which makes the everything simpler because it can't be undefined, but means you can't just visit it and replace it, or add blocks before it, so its simpler and more consistent to have the entry and exit be "outside the implementation" and somewhat immutable. E.g. now setting the 'entry block' is linking the control flow rather than setting a field in procedure, which is consistent with any other control flow modification. The main thing I was thinking of was if the entry block was the head of the loop you might have to adapt the loop reducing algorithm or special case the entry block.
Yes it makes the procedure cfg node somewhat redundant from the perspective of analyses, I think its useful to have the entry/exit symmetry at the block level, as you've said ideally the iterator works at the block level not over the 3 levels of the heirarchy. I'm hesitant to remove the procedure node from the cfg though because it might make the code more convoluted but I haven't really looked at it.

l-kent · 2024-03-01T01:14:09Z

Looking at removing Procedure from the CFG sounds like a good idea to me

# Conflicts: # src/main/scala/analysis/SSAForm.scala # src/main/scala/ir/Program.scala # src/main/scala/ir/Statement.scala

l-kent · 2024-03-11T23:36:02Z

src/test/scala/LiveVarsAnalysisTests.scala

    val procs = program.procs
-    assert(liveVarAnalysisResults(procs("main")) == Map(R30 -> TwoElementTop))
-    assert(liveVarAnalysisResults(procs("callee1")) == Map(R0 -> TwoElementTop, R30 -> TwoElementTop))
-    assert(liveVarAnalysisResults(procs("callee2")) == Map(R1 -> TwoElementTop, R30 -> TwoElementTop))
+    // assert(liveVarAnalysisResults(procs("main")) == Map(R30 -> TwoElementTop))
+    assert(liveVarAnalysisResults(procs("callee1")) == Map(R0 -> TwoElementTop))
+    assert(liveVarAnalysisResults(procs("callee2")) == Map(R1 -> TwoElementTop))
  }


Do we want to remove R30 from these? It makes sense to still consider it 'live' since it is called in a Return?

l-kent · 2024-03-11T23:41:29Z

We probably need to figure out more broadly how this should relate to non-returning procedures, and how they should be handled in the analyses (which generally do not account for their existence).

ailrst · 2024-06-04T04:56:24Z

We probably need to figure out more broadly how this should relate to non-returning procedures, and how they should be handled in the analyses (which generally do not account for their existence).

I think to address this we might add a "Halt" statement, and just have an analysis determine for each procedure if all paths reach a halt statement or non-returning call. I don't think it necessarily interacts with this PR, because we don't want a single halt per-procedure in the same way we do returns for backwards analysis.

Otherwise, I think this PR is overcomplicated. I like having a fixed entry and return block, but the automatic rewriting of Returns into jumps to the exit block is unneccessary. It would make more sense to just have an analysis find all the returns and rewrite the procedure into a diamond shape, and have an invariant checker make sure this stays the case through subsequent transforms.

l-kent · 2024-06-04T05:01:49Z

Is the idea that the 'halt' statement would follow a non-returning call? This could just be an 'assume false' then, but it could be made its own special type for ease of matching.

I agree that automatically rewriting returns like this is more complicated than necessary, and what you now suggest sounds like a better approach.

l-kent · 2024-06-07T00:15:07Z

I think that creating a new Return class is a good idea though. It's worth making a simpler PR that just does that part of it.

ailrst force-pushed the return-statement branch from 37e4c14 to b19358c Compare February 28, 2024 05:54

ailrst added 2 commits February 28, 2024 17:06

make single return invariant in procedure

ec59de9

make the presence of begin and end block invariant in procedure

fix test

58a7f90

ailrst force-pushed the return-statement branch from b19358c to 58a7f90 Compare February 28, 2024 07:07

ailrst marked this pull request as ready for review February 28, 2024 07:16

l-kent reviewed Feb 29, 2024

View reviewed changes

src/main/scala/ir/IR_Dsl.scala Outdated

Copy link

Contributor

l-kent Feb 29, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You've duplicated this since it was moved

ailrst reacted with thumbs up emoji

fix param analysis

9ca9d90

ailrst force-pushed the return-statement branch from 4153965 to 9ca9d90 Compare February 29, 2024 01:25

l-kent reviewed Feb 29, 2024

View reviewed changes

l-kent reviewed Mar 1, 2024

View reviewed changes

Merge branch 'staging' into return-statement

e1ab3e0

# Conflicts: # src/main/scala/analysis/SSAForm.scala # src/main/scala/ir/Program.scala # src/main/scala/ir/Statement.scala

l-kent changed the base branch from staging to main March 11, 2024 23:30

l-kent reviewed Mar 11, 2024

View reviewed changes

clean up, fixing merge, making IDESolver use Return

b705702

ailrst changed the title ~~implement single return invariant~~ implement single return invariant (diamond shaped procedures) Jun 4, 2024

ailrst closed this Jun 11, 2024

ailrst mentioned this pull request Jun 11, 2024

Implement return statement and diamond shaped procedures #219

Open

This pull request was closed.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

implement single return invariant (diamond shaped procedures) #178

implement single return invariant (diamond shaped procedures) #178

ailrst commented Feb 16, 2024 •

edited

Loading

l-kent Feb 29, 2024

l-kent Feb 29, 2024

l-kent Mar 1, 2024

ailrst Mar 1, 2024

l-kent commented Mar 1, 2024

ailrst commented Mar 1, 2024

l-kent commented Mar 1, 2024

l-kent Mar 11, 2024

l-kent commented Mar 11, 2024

ailrst commented Jun 4, 2024

l-kent commented Jun 4, 2024

l-kent commented Jun 7, 2024

implement single return invariant (diamond shaped procedures) #178

implement single return invariant (diamond shaped procedures) #178

Conversation

ailrst commented Feb 16, 2024 • edited Loading

l-kent Feb 29, 2024

Choose a reason for hiding this comment

l-kent Feb 29, 2024

Choose a reason for hiding this comment

l-kent Mar 1, 2024

Choose a reason for hiding this comment

ailrst Mar 1, 2024

Choose a reason for hiding this comment

l-kent commented Mar 1, 2024

ailrst commented Mar 1, 2024

l-kent commented Mar 1, 2024

l-kent Mar 11, 2024

Choose a reason for hiding this comment

l-kent commented Mar 11, 2024

ailrst commented Jun 4, 2024

l-kent commented Jun 4, 2024

l-kent commented Jun 7, 2024

ailrst commented Feb 16, 2024 •

edited

Loading