Skip to content

Commit 053b1e2

Browse files
gauravparthagauravpartha
authored
Merge pull request #411 from viperproject/exhale_no_reordering
Remove three-phase exhale: No reordering of conjuncts during exhale.
2 parents 41a7535 + 1ee52f7 commit 053b1e2

6 files changed

Lines changed: 93 additions & 225 deletions

File tree

‎silver‎

‎src/main/scala/viper/carbon/modules/ExhaleModule.scala‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,4 @@ trait ExhaleModule extends Module with ExhaleComponent with ComponentRegistry[Ex
4040
*/
4141
def exhale(exp: Seq[(sil.Exp, PartialVerificationError)], havocHeap: Boolean = true, isAssert: Boolean = false
4242
, statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt
43-
44-
def currentPhaseId: Int
4543
}

‎src/main/scala/viper/carbon/modules/PermModule.scala‎

Lines changed: 0 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -40,24 +40,8 @@ trait PermModule extends Module with CarbonStateComponent {
4040
*/
4141
def permissionPositive(permission: Exp, zeroOK : Boolean = false): Exp
4242

43-
4443
def conservativeIsPositivePerm(e: sil.Exp): Boolean
4544

46-
/**
47-
* The number of phases during exhale.
48-
*/
49-
def numberOfPhases: Int
50-
51-
/**
52-
* The ID of the phase that this expression should be exhaled in.
53-
*/
54-
def isInPhase(e: sil.Exp, phaseId: Int): Boolean
55-
56-
/**
57-
* A short description of a given phase.
58-
*/
59-
def phaseDescription(phase: Int): String
60-
6145
/**
6246
* The current mask.
6347
*/

‎src/main/scala/viper/carbon/modules/impls/DefaultExhaleModule.scala‎

Lines changed: 44 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -29,9 +29,7 @@ class DefaultExhaleModule(val verifier: Verifier) extends ExhaleModule {
2929

3030
def name = "Exhale module"
3131

32-
override def reset = {
33-
currentPhaseId = -1
34-
}
32+
override def reset = { }
3533

3634
override def start(): Unit = {
3735
register(this)
@@ -48,35 +46,24 @@ class DefaultExhaleModule(val verifier: Verifier) extends ExhaleModule {
4846
wandModule.tempCurState = tempState
4947
initStmtWand = initStmt
5048
}
51-
var tempState: StateRep = wandModule.tempCurState.asInstanceOf[StateRep]
52-
49+
val tempState: StateRep = wandModule.tempCurState.asInstanceOf[StateRep]
5350

54-
val originalPhaseId = currentPhaseId // needed to get nested exhales (e.g. from unfolding expressions) correct
55-
val phases = for (phase <- 1 to numberOfPhases) yield {
56-
currentPhaseId = phase - 1
57-
val stmts = exps map (e => exhaleConnective(e._1.whenExhaling, e._2, currentPhaseId, havocHeap,
58-
statesStackForPackageStmt, insidePackageStmt, isAssert = isAssert, currentStateForPackage = tempState))
59-
if (stmts.children.isEmpty) {
60-
Statements.EmptyStmt
61-
} else {
51+
val exhaleStmt = exps map (e => exhaleConnective(e._1.whenExhaling, e._2, havocHeap,
52+
statesStackForPackageStmt, insidePackageStmt, isAssert = isAssert, currentStateForPackage = tempState))
6253

63-
Comment(s"Phase $phase: ${phaseDescription(currentPhaseId)}") ++ stmts: Stmt
64-
}
65-
}
6654
val assumptions = MaybeCommentBlock("Free assumptions",
6755
exps map (e => allFreeAssumptions(e._1)))
6856

69-
currentPhaseId = originalPhaseId
7057
stateModule.replaceState(curState)
7158

7259
if ((exps map (_._1.isPure) forall identity) || !havocHeap || isAssert) {
7360
// if all expressions are pure, then there is no need for heap copies
7461
// if this is a translation of an Assert statement, there is also no need for heap copies
75-
initStmtWand ++ phases ++ assumptions
62+
initStmtWand ++ exhaleStmt ++ assumptions
7663
} else {
7764
beginExhale ++
7865
initStmtWand ++
79-
phases ++
66+
exhaleStmt ++
8067
assumptions ++
8168
Comment("Finish exhale") ++
8269
endExhale
@@ -89,7 +76,7 @@ class DefaultExhaleModule(val verifier: Verifier) extends ExhaleModule {
8976
* @param currentStateForPackage The temporary state connected to current statement being evaluated inside package statement
9077
* Access to the current state is needed during translation of an exhale during packaging a wand
9178
*/
92-
private def exhaleConnective(e: sil.Exp, error: PartialVerificationError, phase: Int, havocHeap: Boolean = true,
79+
private def exhaleConnective(e: sil.Exp, error: PartialVerificationError, havocHeap: Boolean = true,
9380
statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false,
9481
isAssert: Boolean , currentStateForPackage: StateRep): Stmt = {
9582

@@ -98,41 +85,41 @@ class DefaultExhaleModule(val verifier: Verifier) extends ExhaleModule {
9885

9986
e match {
10087
case sil.And(e1, e2) =>
101-
exhaleConnective(e1, error, phase, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage) ::
102-
exhaleConnective(e2, error, phase, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage) ::
88+
exhaleConnective(e1, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage) ::
89+
exhaleConnective(e2, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage) ::
10390
Nil
10491
case sil.Implies(e1, e2) =>
10592
if(insidePackageStmt){
106-
val res = If(wandModule.getCurOpsBoolvar() ==> translateExpInWand(e1), exhaleConnective(e2, error, phase, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage), Statements.EmptyStmt)
93+
val res = If(wandModule.getCurOpsBoolvar() ==> translateExpInWand(e1), exhaleConnective(e2, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage), Statements.EmptyStmt)
10794
val unionStmt = wandModule.updateUnion()
10895
res ++ unionStmt
10996
}
11097
else
111-
If(translateExpInWand(e1), exhaleConnective(e2, error, phase, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage), Statements.EmptyStmt)
98+
If(translateExpInWand(e1), exhaleConnective(e2, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage), Statements.EmptyStmt)
11299
case sil.CondExp(c, e1, e2) =>
113100
if(insidePackageStmt)
114101
If(wandModule.getCurOpsBoolvar(),
115-
If(translateExpInWand(c), exhaleConnective(e1, error, phase, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage),
116-
exhaleConnective(e2, error, phase, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage)),
102+
If(translateExpInWand(c), exhaleConnective(e1, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage),
103+
exhaleConnective(e2, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage)),
117104
Statements.EmptyStmt) ++
118105
// The union state should be updated because the union state calculated inside exhaleExt (let's call it state U') is inside the then part of if(c){}
119106
// and outside the if condition c is not satisfied we still evaluate expressions and check definedness in U' without knowing any assumption about it
120107
wandModule.updateUnion()
121108
else
122-
If(translateExpInWand(c), exhaleConnective(e1, error, phase, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage),
123-
exhaleConnective(e2, error, phase, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage))
109+
If(translateExpInWand(c), exhaleConnective(e1, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage),
110+
exhaleConnective(e2, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage))
124111
case sil.Let(declared,boundTo,body) if !body.isPure =>
125112
{
126113
val u = env.makeUniquelyNamed(declared) // choose a fresh binder
127114
env.define(u.localVar)
128115
Assign(translateLocalVar(u.localVar),translateExpInWand(boundTo)) ::
129-
exhaleConnective(body.replace(declared.localVar, u.localVar),error,phase, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage) ::
116+
exhaleConnective(body.replace(declared.localVar, u.localVar),error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage) ::
130117
{
131118
env.undefine(u.localVar)
132119
Nil
133120
}
134121
}
135-
case fa@sil.Forall(vars, _, body) if isInPhase(e, phase) && fa.isPure =>
122+
case fa@sil.Forall(vars, _, body) if fa.isPure =>
136123
//GP: the definedness check for foralls is in another branch, hence we must take unfoldings of e
137124
// into account here (otherwise they would be ignored)
138125
{
@@ -141,7 +128,7 @@ class DefaultExhaleModule(val verifier: Verifier) extends ExhaleModule {
141128

142129
val renamedBody = Expressions.instantiateVariables(body, vars.map(_.localVar), varsFresh.map(_.localVar))
143130

144-
val exhaleStmt : Stmt = exhaleConnective(renamedBody, error, phase, havocHeap, statesStackForPackageStmt,
131+
val exhaleStmt : Stmt = exhaleConnective(renamedBody, error, havocHeap, statesStackForPackageStmt,
145132
insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage)
146133

147134
Seqn(Seq (
@@ -154,62 +141,53 @@ class DefaultExhaleModule(val verifier: Verifier) extends ExhaleModule {
154141
}
155142
))
156143
}
157-
case sil.Unfolding(_, body) if !insidePackageStmt && isInPhase(e, phase) => {
144+
case sil.Unfolding(_, body) if !insidePackageStmt => {
158145
val checks = components map (_.exhaleExpBeforeAfter(e, error))
159146
val stmtBefore = (checks map (_._1())).toList
160147

161148
val stmtBody =
162-
exhaleConnective(body, error, phase, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert,
149+
exhaleConnective(body, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert,
163150
currentStateForPackage = currentStateForPackage)
164151

165152
val stmtAfter = (checks map (_._2())).toList
166153

167154
(stmtBefore ++ stmtBody ++ stmtAfter)
168155
}
169-
case _ if isInPhase(e, phase) => {
156+
case _ => {
170157
if(insidePackageStmt){ // handling exhales during packaging a wand
171158
// currently having wild cards and 'constraining' expressions are not supported during packaging a wand.
172-
if(!permModule.getCurrentAbstractReads().isEmpty)
159+
if(!permModule.getCurrentAbstractReads().isEmpty) {
173160
sys.error("Abstract reads cannot be used during packaging a wand.") // AG: To be changed to unsupportedFeatureException
174-
else
175-
if(permModule.containsWildCard(e))
176-
sys.error("Wild cards cannot be used during packaging a wand.") // AG: To be changed to unsupportedFeatureException
161+
}
162+
163+
if(permModule.containsWildCard(e)) {
164+
sys.error("Wild cards cannot be used during packaging a wand.") // AG: To be changed to unsupportedFeatureException
165+
}
166+
167+
val exhaleExtStmt = wandModule.exhaleExt(statesStackForPackageStmt, currentStateForPackage, e, wandModule.getCurOpsBoolvar(), error = error, havocHeap = havocHeap) // executing the exhale statement
168+
val addAssumptions = (statesStackForPackageStmt(0).asInstanceOf[StateRep].boolVar := statesStackForPackageStmt(0).asInstanceOf[StateRep].boolVar && currentStateForPackage.boolVar) // adding needed assumptions to states boolean variables
169+
val equateHps = wandModule.exchangeAssumesWithBoolean(equateHeaps(statesStackForPackageStmt(0).asInstanceOf[StateRep].state, heapModule), statesStackForPackageStmt(0).asInstanceOf[StateRep].boolVar)
170+
val assertTransfer: Stmt = // if it is an assert statement we transfer the permissions from temp state to ops state
171+
if(isAssert && !e.isPure) {
172+
val curState = stateModule.state
173+
stateModule.replaceState(statesStackForPackageStmt(0).asInstanceOf[StateRep].state)
174+
val stmt: Stmt = wandModule.exhaleExt(currentStateForPackage :: Nil, statesStackForPackageStmt(0).asInstanceOf[StateRep], e, wandModule.getCurOpsBoolvar(), error = error)
175+
stateModule.replaceState(curState)
176+
stmt
177+
}
177178
else
178-
// This could is called many times in different phases to handle wildcards and constraining,
179-
// this code for exhaling inside a magic wand should be called only once (in phase 0, in this case)
180-
if(phase == 0) {
181-
var exhaleExtStmt = wandModule.exhaleExt(statesStackForPackageStmt, currentStateForPackage, e, wandModule.getCurOpsBoolvar(), error = error, havocHeap = havocHeap) // executing the exhale statement
182-
val addAssumptions = (statesStackForPackageStmt(0).asInstanceOf[StateRep].boolVar := statesStackForPackageStmt(0).asInstanceOf[StateRep].boolVar && currentStateForPackage.boolVar) // adding needed assumptions to states boolean variables
183-
var equateHps = wandModule.exchangeAssumesWithBoolean(equateHeaps(statesStackForPackageStmt(0).asInstanceOf[StateRep].state, heapModule), statesStackForPackageStmt(0).asInstanceOf[StateRep].boolVar)
184-
var assertTransfer: Stmt = // if it is an assert statement we transfer the permissions from temp state to ops state
185-
if(isAssert && !e.isPure) {
186-
val curState = stateModule.state
187-
stateModule.replaceState(statesStackForPackageStmt(0).asInstanceOf[StateRep].state)
188-
val stmt: Stmt = wandModule.exhaleExt(currentStateForPackage :: Nil, statesStackForPackageStmt(0).asInstanceOf[StateRep], e, wandModule.getCurOpsBoolvar(), error = error)
189-
stateModule.replaceState(curState)
190-
stmt
191-
}
192-
else
193-
Nil
194-
if (!havocHeap)
195-
exhaleExtStmt ++ addAssumptions ++ equateHps ++ assertTransfer
196-
else
197-
exhaleExtStmt ++ addAssumptions ++ assertTransfer
198-
}else {
199179
Nil
200-
}
201-
202-
}else{
180+
if (!havocHeap)
181+
exhaleExtStmt ++ addAssumptions ++ equateHps ++ assertTransfer
182+
else
183+
exhaleExtStmt ++ addAssumptions ++ assertTransfer
184+
} else {
203185
invokeExhaleOnComponents(e, error)
204186
}
205187
}
206-
case _ =>
207-
Nil // nothing to do in this phase
208188
}
209189
}
210190

211-
var currentPhaseId: Int = -1
212-
213191
private def invokeExhaleOnComponents(e: sil.Exp, error: PartialVerificationError) : Stmt = {
214192
val checks = components map (_.exhaleExpBeforeAfter(e, error))
215193
val stmtBefore = checks map (_._1())

‎src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -917,7 +917,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
917917

918918
(before _ , after _ )
919919
}
920-
case pap@sil.PredicateAccessPredicate(loc@sil.PredicateAccess(args, predicateName), _) if duringUnfold && currentPhaseId == 0 =>
920+
case pap@sil.PredicateAccessPredicate(loc@sil.PredicateAccess(args, predicateName), _) if duringUnfold =>
921921
val oldVersion = LocalVar(Identifier("oldVersion"), predicateVersionType)
922922
val newVersion = LocalVar(Identifier("newVersion"), predicateVersionType)
923923
val curVersion = translateExp(loc)

0 commit comments

Comments
 (0)
⚡