Skip to content

Commit

Permalink
Checkpointing IR.
Browse files Browse the repository at this point in the history
  • Loading branch information
@robby-phd
robby-phd committed Feb 12, 2025
1 parent aaae37a commit c51f3e7
Show file tree
Hide file tree
Showing 4 changed files with 96 additions and 79 deletions.
14 changes: 7 additions & 7 deletions ast/shared/src/main/scala/org/sireum/lang/ast/IR.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,25 +61,25 @@ object IR {
}

@datatype class Int(val tipe: Typed, val value: Z, val pos: Position) extends Exp {
@strictpure def prettyST: ST = st"$value [$tipe]"
@strictpure def prettyST: ST = st"$value"
@strictpure def numOfTemps: Z = 0
}

@datatype class F32(val value: org.sireum.F32, val pos: Position) extends Exp {
@strictpure def tipe: Typed = Typed.f32
@strictpure def prettyST: ST = st"$value [f32]"
@strictpure def prettyST: ST = st"$value"
@strictpure def numOfTemps: Z = 0
}

@datatype class F64(val value: org.sireum.F64, val pos: Position) extends Exp {
@strictpure def tipe: Typed = Typed.f64
@strictpure def prettyST: ST = st"$value [f64]"
@strictpure def prettyST: ST = st"$value"
@strictpure def numOfTemps: Z = 0
}

@datatype class R(val value: org.sireum.R, val pos: Position) extends Exp {
@strictpure def tipe: Typed = Typed.r
@strictpure def prettyST: ST = st"$value [r]"
@strictpure def prettyST: ST = st"$value"
@strictpure def numOfTemps: Z = 0
}

Expand Down Expand Up @@ -286,12 +286,12 @@ object IR {

object Assign {

@datatype class Local(val copy: B, val context: MethodContext, val lhs: String, val rhs: Exp, val pos: Position) extends Assign {
@datatype class Local(val copy: B, val context: MethodContext, val lhs: String, val tipe: Typed, val rhs: Exp, val pos: Position) extends Assign {
@strictpure def prettyST: ST = st"$lhs ${if (copy) ":=" else "="} ${rhs.prettyST}"
@strictpure def computeLocalsTemps(locals: Z, temps: Z): (Z, Z) = (locals, temps - rhs.numOfTemps)
}

@datatype class Global(val copy: B, val name: ISZ[String], val rhs: Exp, val pos: Position) extends Assign {
@datatype class Global(val copy: B, val name: ISZ[String], val tipe: Typed, val rhs: Exp, val pos: Position) extends Assign {
@strictpure def prettyST: ST = st"${(name, ".")} ${if (copy) ":=" else "="} ${rhs.prettyST}"
@strictpure def computeLocalsTemps(locals: Z, temps: Z): (Z, Z) = (locals, temps - rhs.numOfTemps)
}
Expand All @@ -301,7 +301,7 @@ object IR {
@strictpure def computeLocalsTemps(locals: Z, temps: Z): (Z, Z) = (locals, temps - rhs.numOfTemps + 1)
}

@datatype class Field(val copy: B, val receiver: Exp, val receiverType: Typed.Name, val id: String, val rhs: Exp, val pos: Position) extends Assign {
@datatype class Field(val copy: B, val receiver: Exp, val receiverType: Typed.Name, val id: String, val tipe: Typed, val rhs: Exp, val pos: Position) extends Assign {
@strictpure def prettyST: ST = st"${receiver.prettyST}.$id ${if (copy) ":=" else "="} ${rhs.prettyST}"
@strictpure def computeLocalsTemps(locals: Z, temps: Z): (Z, Z) = (locals, temps - receiver.numOfTemps - rhs.numOfTemps)
}
Expand Down
75 changes: 42 additions & 33 deletions ast/shared/src/main/scala/org/sireum/lang/ast/IRTransformer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1127,17 +1127,19 @@ import IRTransformer._
TPostResult(r0.ctx, None())
case o2: IR.Stmt.Assign.Local =>
val r0: TPostResult[Context, IR.MethodContext] = transformIRMethodContext(preR.ctx, o2.context)
val r1: TPostResult[Context, Typed] = transformTyped(r0.ctx, o2.tipe)
val r2: TPostResult[Context, IR.Exp] = transformIRExp(r1.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty || r1.resultOpt.nonEmpty || r2.resultOpt.nonEmpty)
TPostResult(r2.ctx, Some(o2(context = r0.resultOpt.getOrElse(o2.context), tipe = r1.resultOpt.getOrElse(o2.tipe), rhs = r2.resultOpt.getOrElse(o2.rhs))))
else
TPostResult(r2.ctx, None())
case o2: IR.Stmt.Assign.Global =>
val r0: TPostResult[Context, Typed] = transformTyped(preR.ctx, o2.tipe)
val r1: TPostResult[Context, IR.Exp] = transformIRExp(r0.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty || r1.resultOpt.nonEmpty)
TPostResult(r1.ctx, Some(o2(context = r0.resultOpt.getOrElse(o2.context), rhs = r1.resultOpt.getOrElse(o2.rhs))))
TPostResult(r1.ctx, Some(o2(tipe = r0.resultOpt.getOrElse(o2.tipe), rhs = r1.resultOpt.getOrElse(o2.rhs))))
else
TPostResult(r1.ctx, None())
case o2: IR.Stmt.Assign.Global =>
val r0: TPostResult[Context, IR.Exp] = transformIRExp(preR.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty)
TPostResult(r0.ctx, Some(o2(rhs = r0.resultOpt.getOrElse(o2.rhs))))
else
TPostResult(r0.ctx, None())
case o2: IR.Stmt.Assign.Temp =>
val r0: TPostResult[Context, IR.Exp] = transformIRExp(preR.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty)
Expand All @@ -1147,11 +1149,12 @@ import IRTransformer._
case o2: IR.Stmt.Assign.Field =>
val r0: TPostResult[Context, IR.Exp] = transformIRExp(preR.ctx, o2.receiver)
val r1: TPostResult[Context, Typed.Name] = transformTypedName(r0.ctx, o2.receiverType)
val r2: TPostResult[Context, IR.Exp] = transformIRExp(r1.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty || r1.resultOpt.nonEmpty || r2.resultOpt.nonEmpty)
TPostResult(r2.ctx, Some(o2(receiver = r0.resultOpt.getOrElse(o2.receiver), receiverType = r1.resultOpt.getOrElse(o2.receiverType), rhs = r2.resultOpt.getOrElse(o2.rhs))))
val r2: TPostResult[Context, Typed] = transformTyped(r1.ctx, o2.tipe)
val r3: TPostResult[Context, IR.Exp] = transformIRExp(r2.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty || r1.resultOpt.nonEmpty || r2.resultOpt.nonEmpty || r3.resultOpt.nonEmpty)
TPostResult(r3.ctx, Some(o2(receiver = r0.resultOpt.getOrElse(o2.receiver), receiverType = r1.resultOpt.getOrElse(o2.receiverType), tipe = r2.resultOpt.getOrElse(o2.tipe), rhs = r3.resultOpt.getOrElse(o2.rhs))))
else
TPostResult(r2.ctx, None())
TPostResult(r3.ctx, None())
case o2: IR.Stmt.Assign.Index =>
val r0: TPostResult[Context, IR.Exp] = transformIRExp(preR.ctx, o2.receiver)
val r1: TPostResult[Context, Typed.Name] = transformTypedName(r0.ctx, o2.receiverType)
Expand Down Expand Up @@ -1235,17 +1238,19 @@ import IRTransformer._
TPostResult(r0.ctx, None())
case o2: IR.Stmt.Assign.Local =>
val r0: TPostResult[Context, IR.MethodContext] = transformIRMethodContext(preR.ctx, o2.context)
val r1: TPostResult[Context, Typed] = transformTyped(r0.ctx, o2.tipe)
val r2: TPostResult[Context, IR.Exp] = transformIRExp(r1.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty || r1.resultOpt.nonEmpty || r2.resultOpt.nonEmpty)
TPostResult(r2.ctx, Some(o2(context = r0.resultOpt.getOrElse(o2.context), tipe = r1.resultOpt.getOrElse(o2.tipe), rhs = r2.resultOpt.getOrElse(o2.rhs))))
else
TPostResult(r2.ctx, None())
case o2: IR.Stmt.Assign.Global =>
val r0: TPostResult[Context, Typed] = transformTyped(preR.ctx, o2.tipe)
val r1: TPostResult[Context, IR.Exp] = transformIRExp(r0.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty || r1.resultOpt.nonEmpty)
TPostResult(r1.ctx, Some(o2(context = r0.resultOpt.getOrElse(o2.context), rhs = r1.resultOpt.getOrElse(o2.rhs))))
TPostResult(r1.ctx, Some(o2(tipe = r0.resultOpt.getOrElse(o2.tipe), rhs = r1.resultOpt.getOrElse(o2.rhs))))
else
TPostResult(r1.ctx, None())
case o2: IR.Stmt.Assign.Global =>
val r0: TPostResult[Context, IR.Exp] = transformIRExp(preR.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty)
TPostResult(r0.ctx, Some(o2(rhs = r0.resultOpt.getOrElse(o2.rhs))))
else
TPostResult(r0.ctx, None())
case o2: IR.Stmt.Assign.Temp =>
val r0: TPostResult[Context, IR.Exp] = transformIRExp(preR.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty)
Expand All @@ -1255,11 +1260,12 @@ import IRTransformer._
case o2: IR.Stmt.Assign.Field =>
val r0: TPostResult[Context, IR.Exp] = transformIRExp(preR.ctx, o2.receiver)
val r1: TPostResult[Context, Typed.Name] = transformTypedName(r0.ctx, o2.receiverType)
val r2: TPostResult[Context, IR.Exp] = transformIRExp(r1.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty || r1.resultOpt.nonEmpty || r2.resultOpt.nonEmpty)
TPostResult(r2.ctx, Some(o2(receiver = r0.resultOpt.getOrElse(o2.receiver), receiverType = r1.resultOpt.getOrElse(o2.receiverType), rhs = r2.resultOpt.getOrElse(o2.rhs))))
val r2: TPostResult[Context, Typed] = transformTyped(r1.ctx, o2.tipe)
val r3: TPostResult[Context, IR.Exp] = transformIRExp(r2.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty || r1.resultOpt.nonEmpty || r2.resultOpt.nonEmpty || r3.resultOpt.nonEmpty)
TPostResult(r3.ctx, Some(o2(receiver = r0.resultOpt.getOrElse(o2.receiver), receiverType = r1.resultOpt.getOrElse(o2.receiverType), tipe = r2.resultOpt.getOrElse(o2.tipe), rhs = r3.resultOpt.getOrElse(o2.rhs))))
else
TPostResult(r2.ctx, None())
TPostResult(r3.ctx, None())
case o2: IR.Stmt.Assign.Index =>
val r0: TPostResult[Context, IR.Exp] = transformIRExp(preR.ctx, o2.receiver)
val r1: TPostResult[Context, Typed.Name] = transformTypedName(r0.ctx, o2.receiverType)
Expand Down Expand Up @@ -1309,17 +1315,19 @@ import IRTransformer._
val rOpt: TPostResult[Context, IR.Stmt.Assign] = o2 match {
case o2: IR.Stmt.Assign.Local =>
val r0: TPostResult[Context, IR.MethodContext] = transformIRMethodContext(preR.ctx, o2.context)
val r1: TPostResult[Context, Typed] = transformTyped(r0.ctx, o2.tipe)
val r2: TPostResult[Context, IR.Exp] = transformIRExp(r1.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty || r1.resultOpt.nonEmpty || r2.resultOpt.nonEmpty)
TPostResult(r2.ctx, Some(o2(context = r0.resultOpt.getOrElse(o2.context), tipe = r1.resultOpt.getOrElse(o2.tipe), rhs = r2.resultOpt.getOrElse(o2.rhs))))
else
TPostResult(r2.ctx, None())
case o2: IR.Stmt.Assign.Global =>
val r0: TPostResult[Context, Typed] = transformTyped(preR.ctx, o2.tipe)
val r1: TPostResult[Context, IR.Exp] = transformIRExp(r0.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty || r1.resultOpt.nonEmpty)
TPostResult(r1.ctx, Some(o2(context = r0.resultOpt.getOrElse(o2.context), rhs = r1.resultOpt.getOrElse(o2.rhs))))
TPostResult(r1.ctx, Some(o2(tipe = r0.resultOpt.getOrElse(o2.tipe), rhs = r1.resultOpt.getOrElse(o2.rhs))))
else
TPostResult(r1.ctx, None())
case o2: IR.Stmt.Assign.Global =>
val r0: TPostResult[Context, IR.Exp] = transformIRExp(preR.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty)
TPostResult(r0.ctx, Some(o2(rhs = r0.resultOpt.getOrElse(o2.rhs))))
else
TPostResult(r0.ctx, None())
case o2: IR.Stmt.Assign.Temp =>
val r0: TPostResult[Context, IR.Exp] = transformIRExp(preR.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty)
Expand All @@ -1329,11 +1337,12 @@ import IRTransformer._
case o2: IR.Stmt.Assign.Field =>
val r0: TPostResult[Context, IR.Exp] = transformIRExp(preR.ctx, o2.receiver)
val r1: TPostResult[Context, Typed.Name] = transformTypedName(r0.ctx, o2.receiverType)
val r2: TPostResult[Context, IR.Exp] = transformIRExp(r1.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty || r1.resultOpt.nonEmpty || r2.resultOpt.nonEmpty)
TPostResult(r2.ctx, Some(o2(receiver = r0.resultOpt.getOrElse(o2.receiver), receiverType = r1.resultOpt.getOrElse(o2.receiverType), rhs = r2.resultOpt.getOrElse(o2.rhs))))
val r2: TPostResult[Context, Typed] = transformTyped(r1.ctx, o2.tipe)
val r3: TPostResult[Context, IR.Exp] = transformIRExp(r2.ctx, o2.rhs)
if (hasChanged || r0.resultOpt.nonEmpty || r1.resultOpt.nonEmpty || r2.resultOpt.nonEmpty || r3.resultOpt.nonEmpty)
TPostResult(r3.ctx, Some(o2(receiver = r0.resultOpt.getOrElse(o2.receiver), receiverType = r1.resultOpt.getOrElse(o2.receiverType), tipe = r2.resultOpt.getOrElse(o2.tipe), rhs = r3.resultOpt.getOrElse(o2.rhs))))
else
TPostResult(r2.ctx, None())
TPostResult(r3.ctx, None())
case o2: IR.Stmt.Assign.Index =>
val r0: TPostResult[Context, IR.Exp] = transformIRExp(preR.ctx, o2.receiver)
val r1: TPostResult[Context, Typed.Name] = transformTypedName(r0.ctx, o2.receiverType)
Expand Down
63 changes: 36 additions & 27 deletions ast/shared/src/main/scala/org/sireum/lang/ast/MIRTransformer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1339,15 +1339,17 @@ import MIRTransformer._
MNone()
case o2: IR.Stmt.Assign.Local =>
val r0: MOption[IR.MethodContext] = transformIRMethodContext(o2.context)
val r1: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty || r1.nonEmpty)
MSome(o2(context = r0.getOrElse(o2.context), rhs = r1.getOrElse(o2.rhs)))
val r1: MOption[Typed] = transformTyped(o2.tipe)
val r2: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty || r1.nonEmpty || r2.nonEmpty)
MSome(o2(context = r0.getOrElse(o2.context), tipe = r1.getOrElse(o2.tipe), rhs = r2.getOrElse(o2.rhs)))
else
MNone()
case o2: IR.Stmt.Assign.Global =>
val r0: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty)
MSome(o2(rhs = r0.getOrElse(o2.rhs)))
val r0: MOption[Typed] = transformTyped(o2.tipe)
val r1: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty || r1.nonEmpty)
MSome(o2(tipe = r0.getOrElse(o2.tipe), rhs = r1.getOrElse(o2.rhs)))
else
MNone()
case o2: IR.Stmt.Assign.Temp =>
Expand All @@ -1359,9 +1361,10 @@ import MIRTransformer._
case o2: IR.Stmt.Assign.Field =>
val r0: MOption[IR.Exp] = transformIRExp(o2.receiver)
val r1: MOption[Typed.Name] = transformTypedName(o2.receiverType)
val r2: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty || r1.nonEmpty || r2.nonEmpty)
MSome(o2(receiver = r0.getOrElse(o2.receiver), receiverType = r1.getOrElse(o2.receiverType), rhs = r2.getOrElse(o2.rhs)))
val r2: MOption[Typed] = transformTyped(o2.tipe)
val r3: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty || r1.nonEmpty || r2.nonEmpty || r3.nonEmpty)
MSome(o2(receiver = r0.getOrElse(o2.receiver), receiverType = r1.getOrElse(o2.receiverType), tipe = r2.getOrElse(o2.tipe), rhs = r3.getOrElse(o2.rhs)))
else
MNone()
case o2: IR.Stmt.Assign.Index =>
Expand Down Expand Up @@ -1447,15 +1450,17 @@ import MIRTransformer._
MNone()
case o2: IR.Stmt.Assign.Local =>
val r0: MOption[IR.MethodContext] = transformIRMethodContext(o2.context)
val r1: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty || r1.nonEmpty)
MSome(o2(context = r0.getOrElse(o2.context), rhs = r1.getOrElse(o2.rhs)))
val r1: MOption[Typed] = transformTyped(o2.tipe)
val r2: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty || r1.nonEmpty || r2.nonEmpty)
MSome(o2(context = r0.getOrElse(o2.context), tipe = r1.getOrElse(o2.tipe), rhs = r2.getOrElse(o2.rhs)))
else
MNone()
case o2: IR.Stmt.Assign.Global =>
val r0: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty)
MSome(o2(rhs = r0.getOrElse(o2.rhs)))
val r0: MOption[Typed] = transformTyped(o2.tipe)
val r1: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty || r1.nonEmpty)
MSome(o2(tipe = r0.getOrElse(o2.tipe), rhs = r1.getOrElse(o2.rhs)))
else
MNone()
case o2: IR.Stmt.Assign.Temp =>
Expand All @@ -1467,9 +1472,10 @@ import MIRTransformer._
case o2: IR.Stmt.Assign.Field =>
val r0: MOption[IR.Exp] = transformIRExp(o2.receiver)
val r1: MOption[Typed.Name] = transformTypedName(o2.receiverType)
val r2: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty || r1.nonEmpty || r2.nonEmpty)
MSome(o2(receiver = r0.getOrElse(o2.receiver), receiverType = r1.getOrElse(o2.receiverType), rhs = r2.getOrElse(o2.rhs)))
val r2: MOption[Typed] = transformTyped(o2.tipe)
val r3: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty || r1.nonEmpty || r2.nonEmpty || r3.nonEmpty)
MSome(o2(receiver = r0.getOrElse(o2.receiver), receiverType = r1.getOrElse(o2.receiverType), tipe = r2.getOrElse(o2.tipe), rhs = r3.getOrElse(o2.rhs)))
else
MNone()
case o2: IR.Stmt.Assign.Index =>
Expand Down Expand Up @@ -1521,15 +1527,17 @@ import MIRTransformer._
val rOpt: MOption[IR.Stmt.Assign] = o2 match {
case o2: IR.Stmt.Assign.Local =>
val r0: MOption[IR.MethodContext] = transformIRMethodContext(o2.context)
val r1: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty || r1.nonEmpty)
MSome(o2(context = r0.getOrElse(o2.context), rhs = r1.getOrElse(o2.rhs)))
val r1: MOption[Typed] = transformTyped(o2.tipe)
val r2: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty || r1.nonEmpty || r2.nonEmpty)
MSome(o2(context = r0.getOrElse(o2.context), tipe = r1.getOrElse(o2.tipe), rhs = r2.getOrElse(o2.rhs)))
else
MNone()
case o2: IR.Stmt.Assign.Global =>
val r0: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty)
MSome(o2(rhs = r0.getOrElse(o2.rhs)))
val r0: MOption[Typed] = transformTyped(o2.tipe)
val r1: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty || r1.nonEmpty)
MSome(o2(tipe = r0.getOrElse(o2.tipe), rhs = r1.getOrElse(o2.rhs)))
else
MNone()
case o2: IR.Stmt.Assign.Temp =>
Expand All @@ -1541,9 +1549,10 @@ import MIRTransformer._
case o2: IR.Stmt.Assign.Field =>
val r0: MOption[IR.Exp] = transformIRExp(o2.receiver)
val r1: MOption[Typed.Name] = transformTypedName(o2.receiverType)
val r2: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty || r1.nonEmpty || r2.nonEmpty)
MSome(o2(receiver = r0.getOrElse(o2.receiver), receiverType = r1.getOrElse(o2.receiverType), rhs = r2.getOrElse(o2.rhs)))
val r2: MOption[Typed] = transformTyped(o2.tipe)
val r3: MOption[IR.Exp] = transformIRExp(o2.rhs)
if (hasChanged || r0.nonEmpty || r1.nonEmpty || r2.nonEmpty || r3.nonEmpty)
MSome(o2(receiver = r0.getOrElse(o2.receiver), receiverType = r1.getOrElse(o2.receiverType), tipe = r2.getOrElse(o2.tipe), rhs = r3.getOrElse(o2.rhs)))
else
MNone()
case o2: IR.Stmt.Assign.Index =>
Expand Down
Loading

0 comments on commit c51f3e7

Please sign in to comment.