From 9d1dd2a78103716098f28ad17b080f8677a4e9f1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Tue, 12 Apr 2016 23:45:44 +0200
Subject: [PATCH] properly add a GlobalState to program
---
.../xlang/IntroduceGlobalStatePhase.scala | 20 ++++++++++---------
1 file changed, 11 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/leon/xlang/IntroduceGlobalStatePhase.scala b/src/main/scala/leon/xlang/IntroduceGlobalStatePhase.scala
index 7bc975309..bf91ff246 100644
--- a/src/main/scala/leon/xlang/IntroduceGlobalStatePhase.scala
+++ b/src/main/scala/leon/xlang/IntroduceGlobalStatePhase.scala
@@ -19,18 +19,16 @@ object IntroduceGlobalStatePhase extends TransformationPhase {
val description = "Introduce a global state passed around to all functions that depend on it"
- private val globalStateCCD = new CaseClassDef(FreshIdentifier("GlobalState"), Seq(), None, false)
- private val epsilonSeed = FreshIdentifier("epsilonSeed", IntegerType)
- globalStateCCD.setFields(Seq(ValDef(epsilonSeed).setIsVar(true)))
-
override def apply(ctx: LeonContext, pgm: Program): Program = {
+ val globalStateCCD = new CaseClassDef(FreshIdentifier("GlobalState"), Seq(), None, false)
+ val epsilonSeed = FreshIdentifier("epsilonSeed", IntegerType)
+ globalStateCCD.setFields(Seq(ValDef(epsilonSeed).setIsVar(true)))
+
val fds = allFunDefs(pgm)
var updatedFunctions: Map[FunDef, FunDef] = Map()
val statefulFunDefs = funDefsNeedingState(pgm)
- //println("Stateful fun def: " + statefulFunDefs.map(_.id))
-
/*
* The first pass will introduce all new function definitions,
@@ -45,10 +43,14 @@ object IntroduceGlobalStatePhase extends TransformationPhase {
for {
fd <- fds if statefulFunDefs.contains(fd)
} {
- updateBody(fd, updatedFunctions)(ctx)
+ updateBody(fd, updatedFunctions, globalStateCCD, epsilonSeed)(ctx)
}
- replaceDefsInProgram(pgm)(updatedFunctions)
+ val pgm0 = replaceDefsInProgram(pgm)(updatedFunctions)
+
+ val globalStateModule = ModuleDef(FreshIdentifier("GlobalStateModule"), Seq(globalStateCCD), false)
+ val globalStateUnit = UnitDef(FreshIdentifier("GlobalStateUnit"), List("leon", "internal"), Seq(), Seq(globalStateModule), false)
+ pgm0.copy(units = globalStateUnit :: pgm0.units)
}
private def extendFunDefWithState(fd: FunDef, stateCCD: CaseClassDef)(ctx: LeonContext): FunDef = {
@@ -59,7 +61,7 @@ object IntroduceGlobalStatePhase extends TransformationPhase {
newFunDef
}
- private def updateBody(fd: FunDef, updatedFunctions: Map[FunDef, FunDef])(ctx: LeonContext): FunDef = {
+ private def updateBody(fd: FunDef, updatedFunctions: Map[FunDef, FunDef], globalStateCCD: CaseClassDef, epsilonSeed: Identifier)(ctx: LeonContext): FunDef = {
val nfd = updatedFunctions(fd)
val stateParam: ValDef = nfd.params.last
--
GitLab