diff --git a/src/main/scala/uclid/SymbolicSimulator.scala b/src/main/scala/uclid/SymbolicSimulator.scala index da502b717..9a6afad2d 100644 --- a/src/main/scala/uclid/SymbolicSimulator.scala +++ b/src/main/scala/uclid/SymbolicSimulator.scala @@ -1868,7 +1868,7 @@ class SymbolicSimulator (module : Module) { case AssignStmt(lhss,rhss) => val es = rhss.map(i => evaluate(i, symbolTable, frameTable, frameNumber, scope)); return simulateAssign(lhss, es, symbolTable, label) - case BlockStmt(vars, stmts) => + case BlockStmt(vars, stmts, _ ) => val declaredVars = vars.flatMap(vs => vs.ids.map(v => (v, vs.typ))) val initSymbolTable = symbolTable val localSymbolTable = declaredVars.foldLeft(initSymbolTable) { @@ -1929,7 +1929,7 @@ class SymbolicSimulator (module : Module) { } case AssignStmt(lhss,rhss) => return lhss.map(lhs => lhs.ident).toSet - case BlockStmt(vars, stmts) => + case BlockStmt(vars, stmts, _) => val declaredVars : Set[Identifier] = vars.flatMap(vs => vs.ids.map(id => id)).toSet return writeSets(stmts) -- declaredVars case IfElseStmt(e,then_branch,else_branch) => diff --git a/src/main/scala/uclid/UclidMain.scala b/src/main/scala/uclid/UclidMain.scala index 1874ceeae..fe5f4d38a 100644 --- a/src/main/scala/uclid/UclidMain.scala +++ b/src/main/scala/uclid/UclidMain.scala @@ -390,7 +390,7 @@ object UclidMain { val newInitDecl = initAccDecls match { case Some(initAcc) => initModuleDecls match { case Some(initMod) => List(InitDecl(BlockStmt(List[BlockVarsDecl](), - List(initAcc.asInstanceOf[InitDecl].body, initMod.asInstanceOf[InitDecl].body)))) + List(initAcc.asInstanceOf[InitDecl].body, initMod.asInstanceOf[InitDecl].body), true))) case None => List(initAcc) } case None => initModuleDecls match { @@ -468,6 +468,9 @@ object UclidMain { passManager.addPass(new ModuleTypeChecker()) // optimisation, has previously been called passManager.addPass(new SemanticAnalyzer()) + // reorder statements if necessary. + // Pass MUST be run after variable renamers + //passManager.addPass(new BlockSorter()) // known bugs in the following passes if (config.enumToNumeric) passManager.addPass(new EnumTypeAnalysis()) if (config.enumToNumeric) passManager.addPass(new EnumTypeRenamer("BV")) diff --git a/src/main/scala/uclid/lang/ASTVisitorUtils.scala b/src/main/scala/uclid/lang/ASTVisitorUtils.scala index 3469b5cd7..023d24c98 100644 --- a/src/main/scala/uclid/lang/ASTVisitorUtils.scala +++ b/src/main/scala/uclid/lang/ASTVisitorUtils.scala @@ -177,6 +177,48 @@ class ExprRewriter(name: String, rewrites : Map[Expr, Expr]) } } +// used to rewrite only the read expressions +class ReadSetExprRewriter(name: String, rewrites : Map[Expr, Expr]) + extends ASTRewriter(name, new ExprRewriterPass(rewrites)) +{ + def rewriteExpr(e : Expr, context : Scope) : Expr = { + e match { + case OperatorApplication(OldOperator(), _) => e + case OperatorApplication(HistoryOperator(), _) => e + case _ => visitExpr(e, context).get + } + } + + def rewriteStatements(stmts : List[Statement], context : Scope) : List[Statement] = { + return stmts.flatMap(visitStatement(_, context)) + } + + def rewriteStatement(stmt : Statement, context : Scope) : Option[Statement] = { + visitStatement(stmt, context) + } + + // do nothing for the LHS + override def visitLhs(lhs: Lhs, context: Scope): Option[Lhs] = Some(lhs) + + override def visitOperatorApp(opapp : OperatorApplication, context : Scope) : Option[Expr] = { + + opapp match { + case OperatorApplication(HistoryOperator(), _) => { + Some(opapp) + } + case OperatorApplication(OldOperator(), _) => Some(opapp) + case _ => { + val opAppP = visitOperator(opapp.op, context).flatMap((op) => { + pass.rewriteOperatorApp(OperatorApplication(op, opapp.operands.map(visitExpr(_, context + opapp)).flatten), context) + }) + return ASTNode.introducePos(true, true, opAppP, opapp.position) } + } + } + +} + + + // This class has been modified to handle the abstract class: ModifiableEntity. class OldExprRewriterPass(rewrites : Map[ModifiableEntity, Identifier]) extends RewritePass { diff --git a/src/main/scala/uclid/lang/ASTVistors.scala b/src/main/scala/uclid/lang/ASTVistors.scala index 7db3684ab..f8a54db15 100644 --- a/src/main/scala/uclid/lang/ASTVistors.scala +++ b/src/main/scala/uclid/lang/ASTVistors.scala @@ -1991,7 +1991,7 @@ class ASTRewriter (_passName : String, _pass: RewritePass, setFilename : Boolean log.debug("visitBlockStatement\n{}", Utils.join(blkStmt.toLines, "\n")) val contextP = context + blkStmt.vars val varsP = blkStmt.vars.map(v => visitBlockVars(v, contextP)).flatten - val blkStmtP1 = BlockStmt(varsP, blkStmt.stmts.flatMap(st => visitStatement(st, contextP))) + val blkStmtP1 = BlockStmt(varsP, blkStmt.stmts.flatMap(st => visitStatement(st, contextP)), blkStmt.isProcedural) val blkStmtP = pass.rewriteBlock(blkStmtP1, context) return ASTNode.introducePos(setPosition, setFilename, blkStmtP, blkStmt.position) } diff --git a/src/main/scala/uclid/lang/BlockFlattener.scala b/src/main/scala/uclid/lang/BlockFlattener.scala index 85915e37d..05f76d7c9 100644 --- a/src/main/scala/uclid/lang/BlockFlattener.scala +++ b/src/main/scala/uclid/lang/BlockFlattener.scala @@ -40,6 +40,8 @@ package uclid package lang import com.typesafe.scalalogging.Logger +import java.util.jar.Attributes.Name + class BlockVariableRenamerPass extends RewritePass { def renameVarList (vars : List[(Identifier, Type)], context : Scope) : List[(Identifier, Identifier, Type)] = { @@ -63,7 +65,7 @@ class BlockVariableRenamerPass extends RewritePass { val rewriter = new ExprRewriter("BlockVariableRenamerPass:Block", rewriteMap) val statementsP = rewriter.rewriteStatements(blkStmt.stmts, context + blkStmt.vars) val varsP = varTuples.map(p => BlockVarsDecl(List(p._2), p._3)) - Some(BlockStmt(varsP, statementsP)) + Some(BlockStmt(varsP, statementsP, blkStmt.isProcedural)) } override def rewriteProcedure(proc : ProcedureDecl, context : Scope) : Option[ProcedureDecl] = { val argTuples = renameVarList(proc.sig.inParams, context) @@ -138,10 +140,65 @@ class BlockFlattenerPass extends RewritePass { val stmtsP = rewriter.rewriteStatements(blk.stmts, context + blk.vars) (stmtsP, varDecls) } + + def addConcurrentVars (blkStmt : BlockStmt, context: Scope) : BlockStmt = { + val filteredStmts = blkStmt.stmts.filter(_.isInstanceOf[BlockStmt]) + + if(filteredStmts.size != blkStmt.stmts.size) + logger.debug("BlockFlattener: block contains blk statements and other statements") + + val nonSequentialBlockCount = filteredStmts.count(_.asInstanceOf[BlockStmt].isProcedural == false) + logger.debug("Number of blocks: " + filteredStmts.size.toString()) + + if(!blkStmt.isProcedural && filteredStmts.size >1) + { + val reads = filteredStmts.foldLeft(Set.empty[Identifier]) { + (acc, blk) => { + val readSet = StatementScheduler.readSets(blk.asInstanceOf[BlockStmt].stmts, context) + acc ++ readSet + } + }.filter(id => context.map.contains(id) && context.map(id).isInstanceOf[Scope.StateVar] && !id.name.startsWith("__ucld")) + + val writes = filteredStmts.foldLeft(Set.empty[Identifier]) { + (acc, blk) => { + val writeSet = StatementScheduler.writeSets(blk.asInstanceOf[BlockStmt].stmts, context) + acc ++ writeSet + } + }.filter(id => context.map.contains(id) && context.map(id).isInstanceOf[Scope.StateVar]) + + // create new vars. We only need new variables for the reads that are also written to + // because there should only be + // one write to a variable in a concurrent block. Blocks with more than one write will have been + // caught earlier + val varPairs: Map[Expr, Expr] = + reads.intersect(writes).map( + id => (id.asInstanceOf[Expr] -> NameProvider.get("block_" + id.toString()).asInstanceOf[Expr])).toMap + logger.debug("New vars: " + varPairs.toString()) + + val rewriter = new ReadSetExprRewriter("BlockFlattener:Rewrite", varPairs) + val stmtsP = rewriter.rewriteStatements(blkStmt.stmts, context + blkStmt.vars) + + // create variable declarations for the new read variables. + val vars = varPairs.map(p => BlockVarsDecl(List(p._2.asInstanceOf[Identifier]), context.map(p._1.asInstanceOf[Identifier]).asInstanceOf[Scope.StateVar].typ)) + // create assign statements for the new variables + val readVarAssigns = varPairs.map(p => AssignStmt(List(LhsId(p._2.asInstanceOf[Identifier])), List(p._1.asInstanceOf[Expr]))).toList + + // new block statement + val blkStmtP = BlockStmt(blkStmt.vars ++ vars, readVarAssigns ++ stmtsP, blkStmt.isProcedural) + logger.debug("New block statement:\n" + blkStmtP.toString()) + blkStmtP + } + else{ + blkStmt + } + } + override def rewriteBlock(blkStmt : BlockStmt, context : Scope) : Option[Statement] = { logger.debug("==> [%s] Input:\n%s".format(analysis.passName, blkStmt.toString())) val init = (List.empty[Statement], Map.empty[Identifier, Type]) - val (stmtsP, mapOut) = blkStmt.stmts.foldLeft(init) { + + val blkStmtP = addConcurrentVars(blkStmt, context) + val (stmtsP, mapOut) = blkStmtP.stmts.foldLeft(init) { (acc, st) => { val (stP, mapOut) = st match { case blk : BlockStmt => renameBlock(blk, context, acc._2) @@ -150,8 +207,9 @@ class BlockFlattenerPass extends RewritePass { (acc._1 ++ stP, mapOut) } } + val vars = mapOut.map(p => BlockVarsDecl(List(p._1), p._2)) - val result = BlockStmt(blkStmt.vars ++ vars, stmtsP) + val result = BlockStmt(blkStmtP.vars ++ vars, stmtsP, blkStmt.isProcedural) logger.debug("<== Result:\n" + result.toString()) Some(result) } @@ -170,6 +228,8 @@ class BlockFlattener() extends ASTRewriter(BlockFlattener.getName(), new BlockFl override val repeatUntilNoChange = true } + + object Optimizer { var index = 0 def getName() : String = { diff --git a/src/main/scala/uclid/lang/LoopUnroller.scala b/src/main/scala/uclid/lang/LoopUnroller.scala index b5b78efba..f817d13db 100644 --- a/src/main/scala/uclid/lang/LoopUnroller.scala +++ b/src/main/scala/uclid/lang/LoopUnroller.scala @@ -61,7 +61,7 @@ class ForLoopRewriterPass(forStmtsToRewrite: Set[ForStmt]) extends RewritePass { rewriter.rewriteStatement(st.body, ctx) } val stmts = (low to high).foldLeft(List.empty[Statement])((acc, i) => acc ++ rewriteForValue(i).toList) - Some(BlockStmt(List.empty, stmts)) + Some(BlockStmt(List.empty, stmts, true)) } else { Some(st) } diff --git a/src/main/scala/uclid/lang/MacroRewriter.scala b/src/main/scala/uclid/lang/MacroRewriter.scala index dc4e1e890..ba77cc648 100644 --- a/src/main/scala/uclid/lang/MacroRewriter.scala +++ b/src/main/scala/uclid/lang/MacroRewriter.scala @@ -81,7 +81,7 @@ class MacroReplacerPass(macroId : Identifier, newMacroBody : BlockStmt) extends case _ => } } - BlockStmt(st.vars, leftStmts) + BlockStmt(st.vars, leftStmts, false) } } diff --git a/src/main/scala/uclid/lang/ModSetAnalysis.scala b/src/main/scala/uclid/lang/ModSetAnalysis.scala index 21e49c5fa..c967747e3 100644 --- a/src/main/scala/uclid/lang/ModSetAnalysis.scala +++ b/src/main/scala/uclid/lang/ModSetAnalysis.scala @@ -64,7 +64,7 @@ class ModSetRewriterPass() extends RewritePass { * @param modSetMap The modifies set map inferred by the ModSetAnalysis pass. Should contain a map from procedures to thier inferred modifies sets. */ def getStmtModSet(stmt: Statement, modSetMap: Map[Identifier, Set[ModifiableEntity]], varIdSet: Set[Identifier], locVarIdSet: Set[Identifier]): Set[ModifiableEntity] = stmt match { - case BlockStmt(vars, stmts) => { + case BlockStmt(vars, stmts,_) => { val locVarIdSetP = vars.foldLeft(locVarIdSet)((acc, bvd) => acc ++ bvd.ids.toSet) stmts.foldLeft(Set.empty[ModifiableEntity])((acc, stmt) => acc ++ getStmtModSet(stmt, modSetMap, varIdSet, locVarIdSetP)) } diff --git a/src/main/scala/uclid/lang/ModularProductProgram.scala b/src/main/scala/uclid/lang/ModularProductProgram.scala index 76866bad2..6c1dbb544 100644 --- a/src/main/scala/uclid/lang/ModularProductProgram.scala +++ b/src/main/scala/uclid/lang/ModularProductProgram.scala @@ -113,7 +113,7 @@ class ModularProductProgramPass extends RewritePass { def findRequiredActivationVariables(stmts: List[Statement], currentScope: Int, context: Scope): Unit = { if(!stmts.isEmpty) { stmts.head match { - case BlockStmt(vars, blockstmts) => + case BlockStmt(vars, blockstmts, _ ) => findRequiredActivationVariables(blockstmts, currentScope, context + vars) case IfElseStmt(_, ifblock, elseblock) => val activationVarsDecl1 = createActivationVariables(k,helperObj.mapOfActivationVariables,helperObj.maxScope+1) @@ -228,7 +228,7 @@ class ModularProductProgramPass extends RewritePass { case WhileStmt(_, body, _) => collectRenamedVariablesFromBlockVars(body.asInstanceOf[BlockStmt].vars) collectRenamedVariablesFromBlockBody(body.asInstanceOf[BlockStmt].stmts) - case BlockStmt(vars, blockstmts) => + case BlockStmt(vars, blockstmts, _) => collectRenamedVariablesFromBlockVars(vars) collectRenamedVariablesFromBlockBody(blockstmts) case _ => @@ -309,7 +309,7 @@ class ModularProductProgramPass extends RewritePass { addDeclarationsToMap(maxblock, body.asInstanceOf[BlockStmt].vars) collectInsideBlockVarsUtil(body.asInstanceOf[BlockStmt].stmts) - case BlockStmt(vars, blockstmts) => + case BlockStmt(vars, blockstmts, _) => maxblock += 1 addDeclarationsToMap(maxblock, vars) @@ -491,8 +491,8 @@ class ModularProductProgramPass extends RewritePass { val renamedExpression = getRenamedExpr(expr, context, k) val newAssumeStatement = AssumeStmt(renamedExpression, id) ASTNode.introducePos(true, true, newAssumeStatement, stmts.head.position) - val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssumeStatement.asInstanceOf[Statement])) - val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) + val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssumeStatement.asInstanceOf[Statement]),true) + val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt()),true) val modularStmt = IfElseStmt(andCondition, trueBlockStmt, falseBlockStmt) newbody += modularStmt } @@ -505,8 +505,8 @@ class ModularProductProgramPass extends RewritePass { val renamedExpression = getRenamedExpr(expr, context, i) val newAssumeStatement = AssumeStmt(renamedExpression, id) ASTNode.introducePos(true, true, newAssumeStatement, stmts.head.position) - val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssumeStatement.asInstanceOf[Statement])) - val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) + val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssumeStatement.asInstanceOf[Statement]),true) + val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt()),true) val modularStmt = IfElseStmt(checkActVarCondition, trueBlockStmt, falseBlockStmt) newbody += modularStmt } @@ -521,8 +521,8 @@ class ModularProductProgramPass extends RewritePass { val renamedExpression = getRenamedExpr(expr, context, i) val newAssumeStatement = AssumeStmt(renamedExpression, id) ASTNode.introducePos(true, true, newAssumeStatement, stmts.head.position) - val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssumeStatement.asInstanceOf[Statement])) - val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) + val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssumeStatement.asInstanceOf[Statement]),true) + val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt()),true) val modularStmt = IfElseStmt(checkActVarCondition, trueBlockStmt, falseBlockStmt) newbody += modularStmt } @@ -552,8 +552,8 @@ class ModularProductProgramPass extends RewritePass { val renamedExpression = getRenamedExpr(expr, context, k) val newAssertStatement = AssertStmt(renamedExpression, id) ASTNode.introducePos(true, true, newAssertStatement, stmts.head.position) - val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssertStatement.asInstanceOf[Statement])) - val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) + val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssertStatement.asInstanceOf[Statement]), true) + val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt()), true) val modularStmt = IfElseStmt(andCondition, trueBlockStmt, falseBlockStmt) newbody += modularStmt } @@ -566,8 +566,8 @@ class ModularProductProgramPass extends RewritePass { val renamedExpression = getRenamedExpr(expr, context, i) val newAssertStatement = AssertStmt(renamedExpression, id) ASTNode.introducePos(true, true, newAssertStatement, stmts.head.position) - val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssertStatement.asInstanceOf[Statement])) - val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) + val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssertStatement.asInstanceOf[Statement]), true) + val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt()),true) val modularStmt = IfElseStmt(checkActVarCondition, trueBlockStmt, falseBlockStmt) newbody += modularStmt } @@ -582,8 +582,8 @@ class ModularProductProgramPass extends RewritePass { val renamedExpression = getRenamedExpr(expr, context, i) val newAssertStatement = AssertStmt(renamedExpression, id) ASTNode.introducePos(true, true, newAssertStatement, stmts.head.position) - val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssertStatement.asInstanceOf[Statement])) - val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) + val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssertStatement.asInstanceOf[Statement]),true) + val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt()),true) val modularStmt = IfElseStmt(checkActVarCondition, trueBlockStmt, falseBlockStmt) newbody += modularStmt } @@ -635,8 +635,8 @@ class ModularProductProgramPass extends RewritePass { val actVarArray = helperObj.mapOfActivationVariables(currentScope) val actVarCond = actVarArray(i) val emptyVarsList: List[BlockVarsDecl] = List() - val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssignStmt.asInstanceOf[Statement] )) - val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) + val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssignStmt.asInstanceOf[Statement] ),true) + val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt()),true) val modularStmt = IfElseStmt(actVarCond, trueBlockStmt, falseBlockStmt) ASTNode.introducePos(true, true, modularStmt, stmts.head.position) newbody += modularStmt @@ -652,8 +652,8 @@ class ModularProductProgramPass extends RewritePass { val actVarArray = helperObj.mapOfActivationVariables(currentScope) val actVarCond = actVarArray(i) val emptyVarsList: List[BlockVarsDecl] = List() - val trueBlockStmt = BlockStmt(emptyVarsList,List(havocstmt.asInstanceOf[Statement] )) - val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) + val trueBlockStmt = BlockStmt(emptyVarsList,List(havocstmt.asInstanceOf[Statement] ),true) + val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt()),true) val modularStmt = IfElseStmt(actVarCond, trueBlockStmt, falseBlockStmt) ASTNode.introducePos(true, true, modularStmt, stmts.head.position) newbody += modularStmt @@ -666,8 +666,8 @@ class ModularProductProgramPass extends RewritePass { val actVarArray = helperObj.mapOfActivationVariables(currentScope) val actVarCond = actVarArray(i) val emptyVarsList: List[BlockVarsDecl] = List() - val trueBlockStmt = BlockStmt(emptyVarsList,List(havocstmt.asInstanceOf[Statement] )) - val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) + val trueBlockStmt = BlockStmt(emptyVarsList,List(havocstmt.asInstanceOf[Statement] ),true) + val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt()),true) val modularStmt = IfElseStmt(actVarCond, trueBlockStmt, falseBlockStmt) ASTNode.introducePos(true, true, modularStmt, stmts.head.position) newbody += modularStmt @@ -677,7 +677,7 @@ class ModularProductProgramPass extends RewritePass { } - case BlockStmt(blockvars, blockstmts) => + case BlockStmt(blockvars, blockstmts,isProc) => val ctx = context + blockvars var newblockvars: List[BlockVarsDecl] = List() helperObj.mapOfRenamedVarDecls get blocknum match { @@ -688,7 +688,7 @@ class ModularProductProgramPass extends RewritePass { val newblockstmts = ListBuffer[Statement]() blocknum+=1 translateBody(currentScope, blockstmts, newblockstmts, ctx) - val newBlock = BlockStmt(newblockvars, newblockstmts.toList) + val newBlock = BlockStmt(newblockvars, newblockstmts.toList, isProc) ASTNode.introducePos(true, true, newBlock, stmts.head.position) newbody += newBlock @@ -792,7 +792,7 @@ class ModularProductProgramPass extends RewritePass { helperObj.maxScope+=1 translateBody(helperObj.maxScope, List(body), whilebody, context) val emptyVarsList: List[BlockVarsDecl] = List() - val whilebodyblock = BlockStmt(emptyVarsList, whilebody.toList) + val whilebodyblock = BlockStmt(emptyVarsList, whilebody.toList, true) if(!body.asInstanceOf[BlockStmt].stmts.isEmpty) ASTNode.introducePos(true, true, whilebodyblock, body.asInstanceOf[BlockStmt].stmts.head.position) val newWhileStatement = WhileStmt(orCondition, whilebodyblock, newinvariants.toList) @@ -855,8 +855,8 @@ class ModularProductProgramPass extends RewritePass { } //creatingIfStmt1 val emptyVarsList: List[BlockVarsDecl] = List() - val trueBlockStmt1 = BlockStmt(emptyVarsList,trueStmtBlock1.toList) - val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) + val trueBlockStmt1 = BlockStmt(emptyVarsList,trueStmtBlock1.toList, true) + val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt()), true) val statement1 = IfElseStmt(checkActVarCondition, trueBlockStmt1, falseBlockStmt) newIfStatements1 += statement1 } @@ -899,8 +899,8 @@ class ModularProductProgramPass extends RewritePass { //creatingIfStmt2 val emptyVarsList: List[BlockVarsDecl] = List() - val trueBlockStmt2 = BlockStmt(emptyVarsList,trueStmtBlock2.toList) - val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) + val trueBlockStmt2 = BlockStmt(emptyVarsList,trueStmtBlock2.toList, true) + val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt()), true) val statement2 = IfElseStmt(checkActVarCondition, trueBlockStmt2, falseBlockStmt) newIfStatements2 += statement2 @@ -912,8 +912,8 @@ class ModularProductProgramPass extends RewritePass { modularStatements += procCallStmt modularStatements ++= newIfStatements2 val emptyVarsList: List[BlockVarsDecl] = List() - val trueBlockStmt = BlockStmt(emptyVarsList,modularStatements.toList) - val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) + val trueBlockStmt = BlockStmt(emptyVarsList,modularStatements.toList, true) + val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt()), true) val modularStmt = IfElseStmt(orCondition, trueBlockStmt, falseBlockStmt) newbody += modularStmt helperObj.maxVarScope += (numberOfParameters + numberOfReturnParameters) @@ -931,8 +931,8 @@ class ModularProductProgramPass extends RewritePass { variable => LhsId(getRenamedExpr(variable.ident.asInstanceOf[Expr], context, i).asInstanceOf[Identifier])) val newargs = args.map(getRenamedExpr(_, context, i)) val procCallStmt = ProcedureCallStmt(id, newlhss, newargs.toList, instId) - val trueBlockStmt = BlockStmt(emptyVarsList,List(procCallStmt)) - val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) + val trueBlockStmt = BlockStmt(emptyVarsList,List(procCallStmt), true) + val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt()), true) val newStmt = IfElseStmt(actVarCheckCondition, trueBlockStmt, falseBlockStmt) newbody += newStmt } @@ -973,7 +973,7 @@ class ModularProductProgramPass extends RewritePass { val newdecls = getLocalVarDeclarations(proc.body.asInstanceOf[BlockStmt].vars) val procIdentifier = Identifier(proc.id.name + "$" + k.toString()) val newbody = translateProcedure() - val procBody = BlockStmt(newVarDeclarations.toList ::: newdecls, newbody.toList) + val procBody = BlockStmt(newVarDeclarations.toList ::: newdecls, newbody.toList, true) ProcedureDecl(procIdentifier, procSignature, procBody, newRequiresList.distinct.toList, newEnsuresList.distinct.toList, newModifiesList, proc.annotations) } @@ -1118,8 +1118,8 @@ class ModularProductProgramPass extends RewritePass { val newelseblock = ListBuffer[Statement]() removeHyperSelectsFromBody(ifblock.asInstanceOf[BlockStmt].stmts, newifblock) removeHyperSelectsFromBody(elseblock.asInstanceOf[BlockStmt].stmts, newelseblock) - val trueblock = BlockStmt(ifblock.asInstanceOf[BlockStmt].vars, newifblock.toList) - val falseblock = BlockStmt(elseblock.asInstanceOf[BlockStmt].vars, newelseblock.toList) + val trueblock = BlockStmt(ifblock.asInstanceOf[BlockStmt].vars, newifblock.toList, true) + val falseblock = BlockStmt(elseblock.asInstanceOf[BlockStmt].vars, newelseblock.toList, true) val newIfStatement = IfElseStmt(cond, trueblock, falseblock) newstmts += newIfStatement @@ -1144,7 +1144,7 @@ class ModularProductProgramPass extends RewritePass { } val newwhilebody = ListBuffer[Statement]() removeHyperSelectsFromBody(body.asInstanceOf[BlockStmt].stmts, newwhilebody) - val newwhilebodyblock = BlockStmt(body.asInstanceOf[BlockStmt].vars, newwhilebody.toList) + val newwhilebodyblock = BlockStmt(body.asInstanceOf[BlockStmt].vars, newwhilebody.toList, true) val newwhilestmt = WhileStmt(cond, newwhilebodyblock, newinvariants.toList) newstmts += newwhilestmt.asInstanceOf[Statement] @@ -1160,7 +1160,7 @@ class ModularProductProgramPass extends RewritePass { removeFromEnsures(oldProc.ensures, true, newEnsuresList) val newbody = ListBuffer[Statement]() removeHyperSelectsFromBody(oldProc.body.asInstanceOf[BlockStmt].stmts, newbody) - val newbodyblock = BlockStmt(oldProc.body.asInstanceOf[BlockStmt].vars, newbody.toList) + val newbodyblock = BlockStmt(oldProc.body.asInstanceOf[BlockStmt].vars, newbody.toList, true) new ProcedureDecl(oldProc.id, oldProc.sig, newbodyblock , newRequiresList.distinct.toList, newEnsuresList.distinct.toList, oldProc.modifies, oldProc.annotations ) } diff --git a/src/main/scala/uclid/lang/ModuleFlattener.scala b/src/main/scala/uclid/lang/ModuleFlattener.scala index 45b534971..7e926f9be 100644 --- a/src/main/scala/uclid/lang/ModuleFlattener.scala +++ b/src/main/scala/uclid/lang/ModuleFlattener.scala @@ -356,7 +356,7 @@ class ModuleInstantiatorPass(module : Module, inst : InstanceDecl, targetModule // add initialization for the instance. override def rewriteInit(init : InitDecl, context : Scope) : Option[InitDecl] = { newModule.init match { - case Some(initD) => Some(InitDecl(BlockStmt(List.empty, List(initD.body) ++ List(init.body)))) + case Some(initD) => Some(InitDecl(BlockStmt(List.empty, List(initD.body) ++ List(init.body), true))) case None => Some(init) } } @@ -381,7 +381,7 @@ class ModuleInstantiatorPass(module : Module, inst : InstanceDecl, targetModule // rewrite module. override def rewriteModuleCall(modCall : ModuleCallStmt, context : Scope) : Option[Statement] = { if (modCall.id == inst.instanceId) { - Some(BlockStmt(List.empty, newNextStatements)) + Some(BlockStmt(List.empty, newNextStatements, false)) } else { Some(modCall) } @@ -572,7 +572,7 @@ class ModuleInstantiatorPass(module : Module, inst : InstanceDecl, targetModule AssumeStmt(exprP, None) } } - BlockStmt(List.empty, modifyHavocs ++ postconditionAssumes) + BlockStmt(List.empty, modifyHavocs ++ postconditionAssumes, true) } val stmtsP = if (callStmt.callLhss.size > 0) { val returnAssign = AssignStmt(callStmt.callLhss, retIds) @@ -580,7 +580,7 @@ class ModuleInstantiatorPass(module : Module, inst : InstanceDecl, targetModule } else { modifyInitAssigns ++ oldAssigns ++ preconditionAsserts ++ List(bodyP) ++ postconditionAsserts ++ modifyFinalAssigns } - BlockStmt(varsToDeclare, stmtsP) + BlockStmt(varsToDeclare, stmtsP, true) } /* diff --git a/src/main/scala/uclid/lang/ModuleTypeChecker.scala b/src/main/scala/uclid/lang/ModuleTypeChecker.scala index f8be4f077..c398efea2 100644 --- a/src/main/scala/uclid/lang/ModuleTypeChecker.scala +++ b/src/main/scala/uclid/lang/ModuleTypeChecker.scala @@ -111,7 +111,7 @@ class ModuleTypeCheckerPass extends ReadOnlyPass[Set[ModuleError]] ret - case BlockStmt(_, _) => + case BlockStmt(_, _, _) => in case IfElseStmt(cond, _, _) => val cType = exprTypeChecker.typeOf(cond, context) diff --git a/src/main/scala/uclid/lang/PrimedAssignmentChecker.scala b/src/main/scala/uclid/lang/PrimedAssignmentChecker.scala index 06d07cf87..efb28ae65 100644 --- a/src/main/scala/uclid/lang/PrimedAssignmentChecker.scala +++ b/src/main/scala/uclid/lang/PrimedAssignmentChecker.scala @@ -104,7 +104,7 @@ class PrimedAssignmentCheckerPass extends ReadOnlyPass[Set[ModuleError]] ForStmt(_, _, _, _) | WhileStmt(_, _, _) | CaseStmt(_) | SkipStmt() | AssertStmt(_, _) | AssumeStmt(_, _) | - HavocStmt(_) | BlockStmt(_, _) => + HavocStmt(_) | BlockStmt(_, _, _) => in case ModuleCallStmt(_) => checkParallelConstruct("next") diff --git a/src/main/scala/uclid/lang/PrimedVariableEliminator.scala b/src/main/scala/uclid/lang/PrimedVariableEliminator.scala index 3b1240642..7dab35e8c 100644 --- a/src/main/scala/uclid/lang/PrimedVariableEliminator.scala +++ b/src/main/scala/uclid/lang/PrimedVariableEliminator.scala @@ -130,12 +130,12 @@ class PrimedVariableEliminatorPass extends RewritePass { } override def rewriteInit(init : InitDecl, context : Scope) : Option[InitDecl] = { val primeDecls = getPrimeVarDecls(context) - val initP = InitDecl(BlockStmt(primeDecls, getInitialAssigns() ++ List(init.body))) + val initP = InitDecl(BlockStmt(primeDecls, getInitialAssigns() ++ List(init.body), true)) Some(initP) } override def rewriteNext(next : NextDecl, context : Scope) : Option[NextDecl] = { val primeDecls = getPrimeVarDecls(context) - val nextP = NextDecl(BlockStmt(primeDecls, getInitialAssigns() ++ List(next.body) ++ getFinalAssigns())) + val nextP = NextDecl(BlockStmt(primeDecls, getInitialAssigns() ++ List(next.body) ++ getFinalAssigns(), false)) Some(nextP) } override def rewriteHavoc(havocStmt : HavocStmt, context : Scope) : Option[Statement] = { diff --git a/src/main/scala/uclid/lang/ProcedureInliner.scala b/src/main/scala/uclid/lang/ProcedureInliner.scala index 7a85a06fe..0771c5c52 100644 --- a/src/main/scala/uclid/lang/ProcedureInliner.scala +++ b/src/main/scala/uclid/lang/ProcedureInliner.scala @@ -211,7 +211,7 @@ trait NewProcedureInlinerPass extends RewritePass { AssumeStmt(exprP, None) } } - BlockStmt(List.empty, modifyHavocs ++ postconditionAssumes) + BlockStmt(List.empty, modifyHavocs ++ postconditionAssumes, true) } val stmtsP = if (callStmt.callLhss.size > 0) { val returnAssign = AssignStmt(callStmt.callLhss, retIds) @@ -219,7 +219,7 @@ trait NewProcedureInlinerPass extends RewritePass { } else { argAssigns ++ modifyInitAssigns ++ oldAssigns ++ preconditionAsserts ++ List(bodyP) ++ postconditionAsserts ++ modifyFinalAssigns } - BlockStmt(varsToDeclare, stmtsP) + BlockStmt(varsToDeclare, stmtsP, true) } } diff --git a/src/main/scala/uclid/lang/PropertyRewriter.scala b/src/main/scala/uclid/lang/PropertyRewriter.scala index f7506a5ab..f38fe722b 100644 --- a/src/main/scala/uclid/lang/PropertyRewriter.scala +++ b/src/main/scala/uclid/lang/PropertyRewriter.scala @@ -442,8 +442,8 @@ class LTLPropertyRewriterPass extends RewritePass { } } def guardedAssignment(guardVar : Identifier, copyVar : Identifier, origVars : List[(Identifier, Type)], newVars : List[(Identifier, Type)]) : Statement = { - val thenBlock = BlockStmt(List.empty, AssignStmt(List(LhsId(copyVar)), List(BoolLit(true))) :: assignToVars(newVars, origVars)) - val ifStmt = IfElseStmt(andExpr(guardVar, notExpr(copyVar)), thenBlock, BlockStmt(List.empty, List.empty)) + val thenBlock = BlockStmt(List.empty, AssignStmt(List(LhsId(copyVar)), List(BoolLit(true))) :: assignToVars(newVars, origVars), true) + val ifStmt = IfElseStmt(andExpr(guardVar, notExpr(copyVar)), thenBlock, BlockStmt(List.empty, List.empty, true)) ifStmt } @@ -605,8 +605,8 @@ class LTLPropertyRewriterPass extends RewritePass { hasFailedAssignments ++ pendingAssignments ++ hasAcceptedAssignments ++ hasAcceptedTraceAssignments // new init/next. - val newInitDecl = InitDecl(BlockStmt(List.empty, List(module.init.get.body) ++ postInitStmts ++ postNextStmts)) - val newNextDecl = NextDecl(BlockStmt(List.empty, preNextStmts ++ List(module.next.get.body) ++ postNextStmts)) + val newInitDecl = InitDecl(BlockStmt(List.empty, List(module.init.get.body) ++ postInitStmts ++ postNextStmts, true)) + val newNextDecl = NextDecl(BlockStmt(List.empty, preNextStmts ++ List(module.next.get.body) ++ postNextStmts, false)) // new safety properties. val newSafetyProperties = (ltlSpecs zip safetyExprs).map { p => { diff --git a/src/main/scala/uclid/lang/RedundantAssignmentEliminator.scala b/src/main/scala/uclid/lang/RedundantAssignmentEliminator.scala index a5fed2e4c..1149e40d3 100644 --- a/src/main/scala/uclid/lang/RedundantAssignmentEliminator.scala +++ b/src/main/scala/uclid/lang/RedundantAssignmentEliminator.scala @@ -83,7 +83,7 @@ class RedundantAssignmentEliminatorPass extends RewritePass { } } - val blkP = BlockStmt(blkStmt.vars, stmtsP) + val blkP = BlockStmt(blkStmt.vars, stmtsP, blkStmt.isProcedural) if (stmtsP.size < blkStmt.stmts.size) { log.debug("Original :\n{}", blkStmt.toString()) log.debug("Revised :\n{}", blkP.toString()) diff --git a/src/main/scala/uclid/lang/RewriteFreshLiterals.scala b/src/main/scala/uclid/lang/RewriteFreshLiterals.scala index 4d2a67afc..537b43e4f 100644 --- a/src/main/scala/uclid/lang/RewriteFreshLiterals.scala +++ b/src/main/scala/uclid/lang/RewriteFreshLiterals.scala @@ -36,7 +36,7 @@ class IntroduceFreshHavocsPass extends RewritePass { st.cond match { case f : FreshLit => val havoc = HavocStmt(HavocableFreshLit(f)) - Some(BlockStmt(List.empty, List(havoc, st))) + Some(BlockStmt(List.empty, List(havoc, st), true)) case _ => Some(st) } diff --git a/src/main/scala/uclid/lang/SmokeInserter.scala b/src/main/scala/uclid/lang/SmokeInserter.scala index 0f021415a..a0f38bf79 100644 --- a/src/main/scala/uclid/lang/SmokeInserter.scala +++ b/src/main/scala/uclid/lang/SmokeInserter.scala @@ -53,7 +53,7 @@ class SmokeInsertPass() extends RewritePass { assertFalse.setPos(st.stmts(0).pos) val newstmts = st.stmts :+ assertFalse smokeCount += 1 - Some(BlockStmt(st.vars, newstmts)) + Some(BlockStmt(st.vars, newstmts, st.isProcedural)) } else if (st.stmts.length > 1) { val topLine = st.stmts(0).pos.line val bottomLine = st.stmts(st.stmts.length-1).pos.line @@ -61,7 +61,7 @@ class SmokeInsertPass() extends RewritePass { assertFalse.setPos(st.stmts(st.stmts.length-1).pos) val newstmts = st.stmts :+ assertFalse smokeCount += 1 - Some(BlockStmt(st.vars, newstmts)) + Some(BlockStmt(st.vars, newstmts, st.isProcedural)) } else { Some(st) } diff --git a/src/main/scala/uclid/lang/StatementScheduler.scala b/src/main/scala/uclid/lang/StatementScheduler.scala index 5d040d34e..04e18bba6 100644 --- a/src/main/scala/uclid/lang/StatementScheduler.scala +++ b/src/main/scala/uclid/lang/StatementScheduler.scala @@ -63,7 +63,7 @@ object StatementScheduler { case LhsId(_) | LhsNextId(_) => Some(lhs.ident) case _ => None }).flatten.toSet - case BlockStmt(vars, stmts) => + case BlockStmt(vars, stmts, _) => val declaredVars = vars.flatMap(vs => vs.ids.map(v => v)).toSet writeSets(stmts, context + vars) -- declaredVars case IfElseStmt(_, ifblock, elseblock) => @@ -124,7 +124,7 @@ object StatementScheduler { case HavocableInstanceId(_) => Set.empty } case AssignStmt(lhss, _) => lhss.map(lhs => lhs.ident).toSet - case BlockStmt(vars, stmts) => + case BlockStmt(vars, stmts, _) => val declaredVars : Set[Identifier] = vars.flatMap(vs => vs.ids.map(v => v)).toSet writeSetIds(stmts, context + vars) -- declaredVars case IfElseStmt(_, ifblock, elseblock) => @@ -205,7 +205,7 @@ object StatementScheduler { } readSets(rhss, prime)++readSets(arrayIndices.flatten, prime) } - case BlockStmt(vars, stmts) => + case BlockStmt(vars, stmts, _ ) => val declaredVars : Set[Identifier] = vars.flatMap(vs => vs.ids.map(v => v)).toSet readSets(stmts, context + vars, prime) -- declaredVars case IfElseStmt(cond, ifblock, elseblock) => @@ -355,16 +355,16 @@ class StatementSchedulerPass extends RewritePass { logger.debug("stmt dep graph: {}", stmtDepGraph.toString()) val sortedOrder = Utils.schedule(nodeIds, stmtDepGraph) logger.debug("sortedOrder: {}", sortedOrder.toString()) - BlockStmt(blkStmt.vars, sortedOrder.map(id => stmtIdToStmtMap.get(id).get)) + BlockStmt(blkStmt.vars, sortedOrder.map(id => stmtIdToStmtMap.get(id).get), blkStmt.isProcedural) } override def rewriteNext(next : NextDecl, context : Scope) : Option[NextDecl] = { - val bodyP = reorderStatements(BlockStmt(List.empty, List(next.body)), context).stmts + val bodyP = reorderStatements(BlockStmt(List.empty, List(next.body), false), context).stmts logger.debug(Utils.join(bodyP.flatMap(st => st.toLines), "\n")) - Some(NextDecl(BlockStmt(List.empty, bodyP))) + Some(NextDecl(BlockStmt(List.empty, bodyP, false))) } override def rewriteBlock(blk : BlockStmt, context : Scope) : Option[Statement] = { if (context.environment == SequentialEnvironment) { - val stmtsP = reorderStatements(BlockStmt(blk.vars, blk.stmts), context + blk.vars) + val stmtsP = reorderStatements(BlockStmt(blk.vars, blk.stmts, blk.isProcedural), context + blk.vars) Some(stmtsP) } else { Some(blk) diff --git a/src/main/scala/uclid/lang/TaintPass.scala b/src/main/scala/uclid/lang/TaintPass.scala index 8f565a120..127877ed5 100644 --- a/src/main/scala/uclid/lang/TaintPass.scala +++ b/src/main/scala/uclid/lang/TaintPass.scala @@ -112,10 +112,10 @@ class TaintNextPass extends RewritePass { // Takes a statement as input and adds taint expressions to the statements recursively def addTaintToStatement(statement: Statement, precondition: List[Expr]): List[Statement] = { statement match { - case BlockStmt(vars, stmts) => { + case BlockStmt(vars, stmts, isProc) => { val taint_vars = get_taint_vars(vars) val new_stmts = stmts.map(st => addTaintToStatement(st, precondition)).flatten - List(BlockStmt(taint_vars ++ vars, new_stmts)) + List(BlockStmt(taint_vars ++ vars, new_stmts, isProc)) } case HavocStmt(havocable) => { havocable match { diff --git a/src/main/scala/uclid/lang/UclidLanguage.scala b/src/main/scala/uclid/lang/UclidLanguage.scala index bda312fdf..6342620bc 100644 --- a/src/main/scala/uclid/lang/UclidLanguage.scala +++ b/src/main/scala/uclid/lang/UclidLanguage.scala @@ -1336,11 +1336,11 @@ case class AssignStmt(lhss: List[Lhs], rhss: List[Expr]) extends Statement { override val hasCall = false override val hasInternalCall = false } -case class BlockStmt(vars: List[BlockVarsDecl], stmts: List[Statement]) extends Statement { +case class BlockStmt(vars: List[BlockVarsDecl], stmts: List[Statement], isProcedural: Boolean) extends Statement { override def hasStmtBlock = true override val hasLoop = stmts.exists(st => st.hasLoop) override def toLines = { - List("{ //" ) ++ + List("{ // sequential code =" + isProcedural.toString()) ++ vars.map(PrettyPrinter.indent(1) + _.toString()) ++ stmts.flatMap(_.toLines).map(PrettyPrinter.indent(1) + _) ++ List("}") diff --git a/src/main/scala/uclid/lang/UclidParser.scala b/src/main/scala/uclid/lang/UclidParser.scala index e57b8f963..493ae05ce 100644 --- a/src/main/scala/uclid/lang/UclidParser.scala +++ b/src/main/scala/uclid/lang/UclidParser.scala @@ -583,33 +583,39 @@ object UclidParser extends UclidTokenParsers with PackratParsers { { case macroId => lang.MacroCallStmt(macroId) } | KwNext ~ "(" ~> Id <~ ")" ~ ";" ^^ { case id => lang.ModuleCallStmt(id) } | - KwIf ~ "(" ~ "*" ~ ")" ~> ((BlkStmt|Error_BlkStmt) <~ KwElse) ~ (BlkStmt|Error_BlkStmt) ^^ + KwIf ~ "(" ~ "*" ~ ")" ~> ((ProceduralBlkStmt|Error_BlkStmt) <~ KwElse) ~ (ProceduralBlkStmt|Error_BlkStmt) ^^ { case tblk ~ fblk => lang.IfElseStmt(lang.FreshLit(lang.BooleanType()), tblk, fblk) } | - KwIf ~ "(" ~ "*" ~ ")" ~> (BlkStmt|Error_BlkStmt) ^^ - { case blk => IfElseStmt(lang.FreshLit(lang.BooleanType()), blk, BlockStmt(List.empty, List.empty)) } | - KwIf ~ "(" ~> (Expr <~ ")") ~ (BlkStmt|Error_BlkStmt) ~ (KwElse ~> (BlkStmt|Error_BlkStmt)) ^^ + KwIf ~ "(" ~ "*" ~ ")" ~> (ProceduralBlkStmt|Error_BlkStmt) ^^ + { case blk => IfElseStmt(lang.FreshLit(lang.BooleanType()), blk, BlockStmt(List.empty, List.empty, true)) } | + KwIf ~ "(" ~> (Expr <~ ")") ~ (ProceduralBlkStmt|Error_BlkStmt) ~ (KwElse ~> (ProceduralBlkStmt|Error_BlkStmt)) ^^ { case e ~ f ~ g => IfElseStmt(e,f,g)} | - KwIf ~> (Expr ~ (BlkStmt|Error_BlkStmt)) ^^ - { case e ~ f => IfElseStmt(e, f, BlockStmt(List.empty, List.empty)) } | + KwIf ~> (Expr ~ (ProceduralBlkStmt|Error_BlkStmt)) ^^ + { case e ~ f => IfElseStmt(e, f, BlockStmt(List.empty, List.empty, true)) } | KwCase ~> rep(CaseBlockStmt) <~ KwEsac ^^ { case i => CaseStmt(i) } | - KwFor ~> (Id ~ (KwIn ~> (RangeLit|Error_RangeLit)) ~ (BlkStmt|Error_BlkStmt)) ^^ + KwFor ~> (Id ~ (KwIn ~> (RangeLit|Error_RangeLit)) ~ (ProceduralBlkStmt|Error_BlkStmt)) ^^ { case id ~ r ~ body => ForStmt(id, r._1.typeOf, r, body) } | - KwFor ~ "(" ~> (IdType <~ ")") ~ (KwIn ~> RangeExpr) ~ (BlkStmt|Error_BlkStmt) ^^ + KwFor ~ "(" ~> (IdType <~ ")") ~ (KwIn ~> RangeExpr) ~ (ProceduralBlkStmt|Error_BlkStmt) ^^ { case idtyp ~ range ~ body => ForStmt(idtyp._1, idtyp._2, range, body) } | - KwWhile ~> ("(" ~> Expr <~ ")") ~ rep((Invariant|Error_Invariant)) ~ (BlkStmt|Error_BlkStmt) ^^ + KwWhile ~> ("(" ~> Expr <~ ")") ~ rep((Invariant|Error_Invariant)) ~ (ProceduralBlkStmt|Error_BlkStmt) ^^ { case expr ~ invs ~ body => WhileStmt(expr, body, invs) } | - (BlkStmt|Error_BlkStmt) | + (ProceduralBlkStmt|Error_BlkStmt) | ";" ^^ { case _ => SkipStmt() } } lazy val CaseBlockStmt: PackratParser[(Expr, Statement)] = - (Expr ~ ":" ~ (BlkStmt|Error_BlkStmt)) ^^ { case e ~ ":" ~ ss => (e,ss) } | - (KwDefault ~ ":" ~> (BlkStmt|Error_BlkStmt)) ^^ { case ss => (BoolLit(true), ss) } + (Expr ~ ":" ~ (ProceduralBlkStmt|Error_BlkStmt)) ^^ { case e ~ ":" ~ ss => (e,ss) } | + (KwDefault ~ ":" ~> (ProceduralBlkStmt|Error_BlkStmt)) ^^ { case ss => (BoolLit(true), ss) } lazy val BlkStmt: PackratParser[lang.BlockStmt] = positioned{ "{" ~> rep (BlockVarsDecl) ~ rep ((Statement|Error_Statement)) <~ "}" ^^ { - case vars ~ stmts => lang.BlockStmt(vars, stmts) + case vars ~ stmts => lang.BlockStmt(vars, stmts, false) + } + } + + lazy val ProceduralBlkStmt: PackratParser[lang.BlockStmt] = positioned{ + "{" ~> rep (BlockVarsDecl) ~ rep ((Statement|Error_Statement)) <~ "}" ^^ { + case vars ~ stmts => lang.BlockStmt(vars, stmts, true) } } @@ -672,7 +678,7 @@ object UclidParser extends UclidTokenParsers with PackratParsers { lazy val ProcedureDecl : PackratParser[lang.ProcedureDecl] = positioned { KwProcedure ~> ProcedureAnnotationList.? ~ Id ~ IdTypeList ~ (KwReturns ~> IdTypeList) ~ - rep(ProcedureVerifExpr) ~ (BlkStmt|Error_BlkStmt) ^^ + rep(ProcedureVerifExpr) ~ (ProceduralBlkStmt|Error_BlkStmt) ^^ { case annotOpt ~ id ~ args ~ outs ~ verifExprs ~ body => val annotations = annotOpt match { case Some(ids) => ProcedureAnnotations(ids.toSet) @@ -685,7 +691,7 @@ object UclidParser extends UclidTokenParsers with PackratParsers { lang.ProcedureDecl(id, lang.ProcedureSig(args,outs), body, requiresList, ensuresList, modifiesList.toSet, annotations) } | // procedure with no return value - KwProcedure ~> ProcedureAnnotationList.? ~ Id ~ IdTypeList ~ rep(ProcedureVerifExpr) ~ (BlkStmt|Error_BlkStmt) ^^ + KwProcedure ~> ProcedureAnnotationList.? ~ Id ~ IdTypeList ~ rep(ProcedureVerifExpr) ~ (ProceduralBlkStmt|Error_BlkStmt) ^^ { case annotOpt ~ id ~ args ~ verifExprs ~ body => val annotations = annotOpt match { case Some(ids) => ProcedureAnnotations(ids.toSet) @@ -897,7 +903,7 @@ object UclidParser extends UclidTokenParsers with PackratParsers { } lazy val InitDecl : PackratParser[lang.InitDecl] = positioned { - KwInit ~> (BlkStmt|Error_BlkStmt) ^^ + KwInit ~> (ProceduralBlkStmt|Error_BlkStmt) ^^ { case b => lang.InitDecl(b) } } diff --git a/src/main/scala/uclid/lang/WhileLoopRewriter.scala b/src/main/scala/uclid/lang/WhileLoopRewriter.scala index e492e686b..30d980460 100644 --- a/src/main/scala/uclid/lang/WhileLoopRewriter.scala +++ b/src/main/scala/uclid/lang/WhileLoopRewriter.scala @@ -64,8 +64,9 @@ class WhileLoopRewriterPass extends RewritePass { } val finishAssump = AssumeStmt(Operator.not(cond), None) val ifBody = havocStmts ++ assumeStmts ++ List(body) ++ assertStmts - val ifElseStmt = IfElseStmt(cond, BlockStmt(List.empty, ifBody), BlockStmt(List.empty, List.empty)) - Some(BlockStmt(List.empty, initialAsserts ++ List(ifElseStmt, finishAssump))) + // BlockStatement containing while loop must be procedural code + val ifElseStmt = IfElseStmt(cond, BlockStmt(List.empty, ifBody, true), BlockStmt(List.empty, List.empty, true)) + Some(BlockStmt(List.empty, initialAsserts ++ List(ifElseStmt, finishAssump), true)) } } diff --git a/src/test/scala/VerifierSpec.scala b/src/test/scala/VerifierSpec.scala index f8c0104bc..bf698bac1 100644 --- a/src/test/scala/VerifierSpec.scala +++ b/src/test/scala/VerifierSpec.scala @@ -484,6 +484,9 @@ class ModuleVerifSpec extends AnyFlatSpec { "test-module-import-0.ucl" should "verify all assertions." in { VerifierSpec.expectedFails("./test/test-module-import-0.ucl", 0) } + "test-module-ordering.ucl" should "verify all assertions." in { + VerifierSpec.expectedFails("./test/test-module-ordering.ucl", 0) + } "test-type-import.ucl" should "verify all assertions." in { VerifierSpec.expectedFails("./test/test-type-import.ucl", 0) } diff --git a/test/test-module-ordering.ucl b/test/test-module-ordering.ucl new file mode 100644 index 000000000..6683ba88d --- /dev/null +++ b/test/test-module-ordering.ucl @@ -0,0 +1,45 @@ +module test { + input a : integer; + output b : integer; + + init { + b = 0; + } + + next { + b' = a+1; + } +} + +module main { + var x: integer; + var y: integer; + + // test1 reads in x and updates y'=x+1 + instance test1 : test(a : (x), b: (y)); + // test2 reads in y and updates x'=y+1 + instance test2 : test(a : (y), b: (x)); + + init { + x = 0; + y = 0; + + } + + next { + // both assertions should pass regardless of the ordering of these statements + next(test1); + next(test2); + } + + invariant test1_lt2: test1.b < 2; + invariant test2lt2: test2.b < 2; + + control { + print_module; + v = bmc(1); + check; + print_results; + v.print_cex; + } +} diff --git a/test/test-nested-instance-1.ucl b/test/test-nested-instance-1.ucl index 433f65e9b..ab137e3aa 100644 --- a/test/test-nested-instance-1.ucl +++ b/test/test-nested-instance-1.ucl @@ -41,11 +41,16 @@ module main next(bar1); } + // bar1.foox.a is x, bar1.fooy.a is x. + // y is bar1.z, which is bar1.foox.b + bar1.fooy.b + // This property says that x + 1 + x + 1 == y property b1: initd ==> (bar1.foox.a + 1 + bar1.fooy.a + 1 == y); control { - v = unroll(5); + v = unroll(1); check; print_results; + v.print_cex; + print_module; } }