Add support of the result variable in ensures contracts

vorpal-research · Aug 17, 2021 · 6421c27 · 6421c27
1 parent d20f300
commit 6421c27
Show file tree

Hide file tree

Showing 6 changed files with 86 additions and 29 deletions.
diff --git a/src/main/kotlin/org/jetbrains/research/libsl/asg/ASGSerializer.kt b/src/main/kotlin/org/jetbrains/research/libsl/asg/ASGSerializer.kt
@@ -148,6 +148,10 @@ val variableSerializer = JsonSerializer<Variable> { src, _, context ->
             is GlobalVariableDeclaration -> {
                 addProperty("kind", "global")
             }
+            is ResultVariable -> {
+                addProperty("kind", "result")
+                addProperty("name", "result")
+            }
         }
     }
 }

diff --git a/src/main/kotlin/org/jetbrains/research/libsl/asg/Nodes.kt b/src/main/kotlin/org/jetbrains/research/libsl/asg/Nodes.kt
@@ -163,6 +163,7 @@ data class Function(
     val automaton: Automaton by lazy { context.resolveAutomaton(automatonName) ?: error("unresolved automaton") }
     val qualifiedName: String by lazy { "${automaton.name}.$name" }
     lateinit var target: Automaton
+    var resultVariable: Variable? = null
 }
 
 sealed class Statement: Node()
@@ -264,6 +265,12 @@ data class FunctionArgument(
         get() = "${function.name}.$name"
 }
 
+data class ResultVariable(
+    override val type: Type
+) : Variable() {
+    override val name: String = "result"
+}
+
 data class Annotation(
     val name: String,
     val values: List<Atomic>

diff --git a/src/main/kotlin/org/jetbrains/research/libsl/visitors/ASGBuilder.kt b/src/main/kotlin/org/jetbrains/research/libsl/visitors/ASGBuilder.kt
@@ -482,8 +482,14 @@ class ASGBuilder(private val context: LslContext) : LibSLBaseVisitor<Node>() {
         val res = when (ctx) {
             is LibSLParser.FunctionDeclContext -> {
                 val func = resolveFunctionByCtx(ctx)!!
-                func.args.firstOrNull { it.name == variableName }
-                    ?: func.automaton.variables.firstOrNull { it.name == variableName }
+                if (variableName == "result") {
+                    func.resultVariable
+                } else {
+                    func.args.firstOrNull { it.name == variableName }
+                        ?: func.automaton.variables.firstOrNull {
+                            it.name == variableName
+                        }
+                }
             }
             is LibSLParser.AutomatonDeclContext -> {
                 val automatonName = ctx.name.text

diff --git a/src/main/kotlin/org/jetbrains/research/libsl/visitors/Resolver.kt b/src/main/kotlin/org/jetbrains/research/libsl/visitors/Resolver.kt
@@ -261,6 +261,10 @@ class Resolver(
         context.storeResolvedFunction(func)
 
         args.forEach { it.function = func }
+        if (returnType != null) {
+            val result = ResultVariable(returnType)
+            func.resultVariable = result
+        }
     }
 
     override fun visitEnumBlock(ctx: LibSLParser.EnumBlockContext) {

diff --git a/src/test/testdata/expected/contracts.json b/src/test/testdata/expected/contracts.json
@@ -30,6 +30,7 @@
         {
           "name": "f",
           "automaton": "A",
+          "returnType": "Int",
           "target": "A",
           "args": [
             {
@@ -101,10 +102,41 @@
               "kind": "ENSURES",
               "expression": {
                 "kind": "binary",
-                "op": "LT",
+                "op": "AND",
                 "left": {
-                  "kind": "oldValue",
-                  "value": {
+                  "kind": "binary",
+                  "op": "LT",
+                  "left": {
+                    "kind": "oldValue",
+                    "value": {
+                      "kind": "qualifiedAccess",
+                      "access": {
+                        "kind": "variableAccess",
+                        "name": "param",
+                        "variableInfo": {
+                          "name": "param",
+                          "fullName": "f.param",
+                          "type": {
+                            "name": "Int",
+                            "isPointer": false,
+                            "kind": "simple",
+                            "realType": {
+                              "name": "int",
+                              "isPointer": false,
+                              "kind": "real"
+                            }
+                          },
+                          "kind": "functionArgument",
+                          "function": "A.f",
+                          "functionArgTypes": [
+                            "Int"
+                          ]
+                        },
+                        "type": "Int"
+                      }
+                    }
+                  },
+                  "right": {
                     "kind": "qualifiedAccess",
                     "access": {
                       "kind": "variableAccess",
@@ -133,30 +165,34 @@
                   }
                 },
                 "right": {
-                  "kind": "qualifiedAccess",
-                  "access": {
-                    "kind": "variableAccess",
-                    "name": "param",
-                    "variableInfo": {
-                      "name": "param",
-                      "fullName": "f.param",
-                      "type": {
-                        "name": "Int",
-                        "isPointer": false,
-                        "kind": "simple",
-                        "realType": {
-                          "name": "int",
+                  "kind": "binary",
+                  "op": "EQ",
+                  "left": {
+                    "kind": "qualifiedAccess",
+                    "access": {
+                      "kind": "variableAccess",
+                      "name": "result",
+                      "variableInfo": {
+                        "name": "result",
+                        "fullName": "result",
+                        "type": {
+                          "name": "Int",
                           "isPointer": false,
-                          "kind": "real"
-                        }
+                          "kind": "simple",
+                          "realType": {
+                            "name": "int",
+                            "isPointer": false,
+                            "kind": "real"
+                          }
+                        },
+                        "kind": "result"
                       },
-                      "kind": "functionArgument",
-                      "function": "A.f",
-                      "functionArgTypes": [
-                        "Int"
-                      ]
-                    },
-                    "type": "Int"
+                      "type": "Int"
+                    }
+                  },
+                  "right": {
+                    "kind": "integer",
+                    "value": 1
                   }
                 }
               }

diff --git a/src/test/testdata/lsl/contracts.lsl b/src/test/testdata/lsl/contracts.lsl
@@ -8,9 +8,9 @@ types {
 automaton A : Int {
    var i: Int;
 
-   fun f(param: Int)
+   fun f(param: Int): Int
    requires test1: param >= i;
-   ensures param' < param;
+   ensures param' < param & result = 1;
    {
 
    }