private Context translateWhile ( WyilFile . Stmt . While stmt , Context context ) { WyilFile . Decl . FunctionOrMethod declaration = ( WyilFile . Decl . FunctionOrMethod ) context . getEnvironment ( ) . getParent ( ) . enclosingDeclaration ; // Translate the loop invariant and generate appropriate macro translateLoopInvariantMacros ( stmt , declaration , context . wyalFile ) ; // Rule 1. Check loop invariant on entry checkLoopInvariant ( "loop invariant may not hold on entry" , stmt , context ) ; // Rule 2. Check loop invariant preserved. On entry to the loop body we // must havoc all modified variables. This is necessary as such // variables should retain their values from before the loop. LoopScope scope = new LoopScope ( ) ; Context beforeBodyContext = context . newLoopScope ( scope ) . havoc ( stmt . getModified ( ) ) ; beforeBodyContext = assumeLoopInvariant ( stmt , beforeBodyContext ) ; Pair < Expr , Context > p = translateExpressionWithChecks ( stmt . getCondition ( ) , null , beforeBodyContext ) ; Expr trueCondition = p . first ( ) ; beforeBodyContext = p . second ( ) . assume ( trueCondition ) ; Context afterBodyContext = translateStatementBlock ( stmt . getBody ( ) , beforeBodyContext ) ; // Join continue contexts together since they must also preserve the // loop invariant afterBodyContext = joinDescendants ( beforeBodyContext , afterBodyContext , scope . continueContexts ) ; checkLoopInvariant ( "loop invariant may not be restored" , stmt , afterBodyContext ) ; // Rule 3. Assume loop invariant holds. Context exitContext = context . havoc ( stmt . getModified ( ) ) ; exitContext = assumeLoopInvariant ( stmt , exitContext ) ; Expr falseCondition = invertCondition ( translateExpression ( stmt . getCondition ( ) , null , exitContext . getEnvironment ( ) ) , stmt . getCondition ( ) ) ; exitContext = exitContext . assume ( falseCondition ) ; // // Finally, need to join any break contexts exitContext = joinDescendants ( context , exitContext , scope . breakContexts ) ; // return exitContext ; }
Translate a While statement .