Rewriting system.

sireum · Feb 19, 2024 · bb49c63 · bb49c63
1 parent 6cec653
commit bb49c63
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 9 deletions.
diff --git a/jvm/src/test/scala/org/sireum/logika/LogikaRcTest.scala b/jvm/src/test/scala/org/sireum/logika/LogikaRcTest.scala
@@ -57,7 +57,7 @@ class LogikaRcTest extends SireumRcSpec {
 }
 
   def textResources: scala.collection.SortedMap[scala.Vector[Predef.String], Predef.String] = {
-    val m = $internal.RC.text(Vector("example")) { (p, f) => p.last.endsWith(".sc") && !p.last.startsWith("wip-") }
+    val m = $internal.RC.text(Vector("example")) { (p, f) => p.last.endsWith("comp-instance.sc") && !p.last.startsWith("wip-") }
     implicit val ordering: Ordering[Vector[Predef.String]] = m.ordering
     for ((k, v) <- m; pair <- {
       var r = Vector[(Vector[Predef.String], Predef.String)]()

diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala
@@ -1992,7 +1992,7 @@ import Util._
           if (isInObject) {
             return ISZ()
           } else {
-            return ISZ(evalThis(AST.Exp.This(AST.TypedAttr(ident.posOpt, context.methodOpt.get.receiverTypeOpt))))
+            return ISZ(evalThis(AST.Exp.This(context.methodName, AST.TypedAttr(ident.posOpt, context.methodOpt.get.receiverTypeOpt))))
           }
       }
     }
@@ -2534,7 +2534,7 @@ import Util._
                     val (s4, sym) = idIntro(pos, s3, ctx, "this", t, None())
                     invokeReceiverOpt match {
                       case Some(invokeReceiver) => assigns = assigns :+ ((invokeReceiver, sym))
-                      case _ => assigns = assigns :+ ((AST.Exp.This(AST.TypedAttr(posOpt, Some(t))), sym))
+                      case _ => assigns = assigns :+ ((AST.Exp.This(ctx, AST.TypedAttr(posOpt, Some(t))), sym))
                     }
                     s3 = s4
                   }
@@ -5077,7 +5077,7 @@ import Util._
             }
             if (receiverModified) {
               val srw6 = evalAssignReceiver(whileStmt.contract.modifies, this, this, smt2, cache, rtCheck, srw,
-                Some(AST.Exp.This(AST.TypedAttr(whileStmt.posOpt, Some(receiverOpt.get.tipe)))), receiverOpt,
+                Some(AST.Exp.This(context.methodName, AST.TypedAttr(whileStmt.posOpt, Some(receiverOpt.get.tipe)))), receiverOpt,
                 HashMap.empty, reporter)
               val (srw7, sym) = idIntro(whileStmt.posOpt.get, srw6, context.methodName, "this",
                 context.receiverLocalTypeOpt.get._2, None())

diff --git a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala
@@ -449,6 +449,8 @@ object RewritingSystem {
         case e: AST.Exp.Tuple =>
           return if (e.args.size == 1) rec(e.args(0), funStack, localMap)
           else AST.CoreExp.Constructor(e.typedOpt.get, for (arg <- e.args) yield rec(arg, funStack, localMap))
+        case e: AST.Exp.This =>
+          return AST.CoreExp.LocalVarRef(F, e.owner, "this", e.typedOpt.get)
         case e: AST.Exp.Ident =>
           e.resOpt.get match {
             case res: AST.ResolvedInfo.LocalVar =>
@@ -474,7 +476,8 @@ object RewritingSystem {
                 }
               }
               return AST.CoreExp.ObjectVarRef(res.owner, res.id, e.typedOpt.get)
-            case res: AST.ResolvedInfo.Method => halt(s"TODO: $e")
+            case res: AST.ResolvedInfo.Method =>
+              return AST.CoreExp.ObjectVarRef(res.owner, res.id, e.typedOpt.get)
             case _ => halt(s"Infeasible: $e")
           }
         case e: AST.Exp.Unary =>
@@ -583,8 +586,9 @@ object RewritingSystem {
             case Some(receiver) =>
               return AST.CoreExp.Apply(T, rec(e.ident, funStack, localMap),
                 rec(receiver, funStack, localMap) +: args, e.typedOpt.get)
-            case _ => return AST.CoreExp.Apply(F, rec(e.ident, funStack, localMap),
-              args, e.typedOpt.get)
+            case _ =>
+              return AST.CoreExp.Apply(F, rec(e.ident, funStack, localMap),
+                args, e.typedOpt.get)
           }
         case e: AST.Exp.InvokeNamed =>
           def getArgs: ISZ[AST.CoreExp.Base] = {

diff --git a/shared/src/main/scala/org/sireum/logika/Util.scala b/shared/src/main/scala/org/sireum/logika/Util.scala
@@ -1637,7 +1637,7 @@ object Util {
         val tOpt = Option.some(value.tipe)
         val exp: AST.Exp = if (isLocal) {
           if (id == "this") {
-            AST.Exp.This(AST.TypedAttr(posOpt, tOpt))
+            AST.Exp.This(owner, AST.TypedAttr(posOpt, tOpt))
           } else {
             AST.Exp.Ident(AST.Id(id, AST.Attr(posOpt)), AST.ResolvedAttr(posOpt,
               Some(AST.ResolvedInfo.LocalVar(owner, AST.ResolvedInfo.LocalVar.Scope.Current, isSpec, F, id)), tOpt))
@@ -2398,7 +2398,7 @@ object Util {
             s0 = s0.addClaim(State.Claim.Let.CurrentId(T, receiver, logika.context.methodName, "this", None()))
             args = args :+ receiver
           case _ =>
-            val e = AST.Exp.This(AST.TypedAttr(posOpt, receiverTypeOpt))
+            val e = AST.Exp.This(logika.context.methodName, AST.TypedAttr(posOpt, receiverTypeOpt))
             val ISZ((s1, arg)) = logika.evalExp(Split.Disabled, smt2, cache, T, s0, e, reporter)
             s0 = s1
             args = args :+ arg