From cbb6c1c8604b60cd1e1eccd84de39b3a3ea9918e Mon Sep 17 00:00:00 2001 From: Jonas Date: Mon, 6 Dec 2021 16:03:03 +0100 Subject: [PATCH 1/2] Unroll first and last iteration in encoding --- .../scala/viper/silver/cfg/silver/CfgGenerator.scala | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala index 50c7fd2ae..f4ca1f1d1 100644 --- a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala +++ b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala @@ -185,17 +185,22 @@ object CfgGenerator { // check whether the loop is tagged with an id val loopId = stmt.info.getUniqueInfo[IdInfo].map(_.id) // create labels + val thnTarget = TmpLabel.generate("then") val headTarget = TmpLabel.generate("head") val loopTarget = TmpLabel.generate("loop") val afterTarget = TmpLabel.generate("after") + // unroll first iter + addStatement(ConditionalJumpStmt(cond, thnTarget, afterTarget)) + addLabel(thnTarget) // process loop head addLabel(headTarget, addEmptyStmt = false) addStatement(LoopHeadStmt(invs, afterTarget, loopId)) - addStatement(ConditionalJumpStmt(cond, loopTarget, afterTarget)) + addStatement(JumpStmt(loopTarget)) // process loop body addLabel(loopTarget) + addStatement(WrappedStmt(Inhale(cond)())) run(body) - addStatement(JumpStmt(headTarget)) + addStatement(ConditionalJumpStmt(cond, headTarget, afterTarget)) // set label after loop addLabel(afterTarget) case Seqn(ss, scopedDecls) => From a8911de67bb0b5f2cee0d8b7ee9500f4f7c3afcb Mon Sep 17 00:00:00 2001 From: Jonas Date: Mon, 6 Dec 2021 22:36:06 +0100 Subject: [PATCH 2/2] Branch on !cond when unrolling first iteration This makes the `CfgTests` happy for some reason --- src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala index f4ca1f1d1..e7959d5e6 100644 --- a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala +++ b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala @@ -190,7 +190,7 @@ object CfgGenerator { val loopTarget = TmpLabel.generate("loop") val afterTarget = TmpLabel.generate("after") // unroll first iter - addStatement(ConditionalJumpStmt(cond, thnTarget, afterTarget)) + addStatement(ConditionalJumpStmt(Not(cond)(), afterTarget, thnTarget)) addLabel(thnTarget) // process loop head addLabel(headTarget, addEmptyStmt = false)