Witnesses 2.0

.gitignore

@@ -35,3 +35,4 @@ xcfa.dot
 xcfa.json
 *.plantuml
 xcfa-*.smt2
+witness.yml

build.gradle.kts

@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.6.4"
+    version = "6.6.5"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

buildSrc/build.gradle.kts

@@ -38,6 +38,7 @@ fun gradlePlugin(id: String, version: String): String = "$id:$id.gradle.plugin:$
 dependencies {
     compileOnly(gradleKotlinDsl())
     implementation(kotlin("gradle-plugin", kotlinVersion))
+    implementation(kotlin("serialization", kotlinVersion))
     implementation(gradlePlugin("com.github.johnrengelman.shadow", shadowVersion))
     implementation(gradlePlugin("com.diffplug.spotless", spotlessVersion))
 }

buildSrc/gradle.properties

@@ -40,4 +40,5 @@ gsonVersion=2.9.1
 javasmtVersion=4.1.1
 sosylabVersion=0.3000-569-g89796f98
 cliktVersion=4.4.0
-spotlessVersion=6.25.0
+spotlessVersion=6.25.0
+kamlVersion=0.59.0

buildSrc/src/main/kotlin/Deps.kt

@@ -79,4 +79,6 @@ object Deps {
     }
 
     val clikt = "com.github.ajalt.clikt:clikt:${Versions.clikt}"
+
+    val kaml = "com.charleskorn.kaml:kaml:${Versions.kaml}"
 }

buildSrc/src/main/kotlin/kaml-serialization.gradle.kts

@@ -0,0 +1,41 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+import gradle.kotlin.dsl.accessors._07de9d51edfbede3e6fa517ade9dcf20.implementation
+
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+apply(plugin = "kotlin-common")
+plugins {
+    kotlin("plugin.serialization")
+}
+dependencies {
+    implementation(Deps.kaml)
+}

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CStatement.java

@@ -13,17 +13,17 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
-
 package hu.bme.mit.theta.frontend.transformation.model.statements;
 
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.frontend.ParseContext;
 import hu.bme.mit.theta.frontend.UnsupportedFrontendElementException;
+import org.antlr.v4.runtime.ParserRuleContext;
 
 /**
- * Every Program, Function and Statement is a subclass of this base class.
- * Any CStatement might have an id associated with it, in case there was a label in the source code. This also provides
- * an XcfaLocation, which can be used when jumping to this named location via a _goto_ instruction
+ * Every Program, Function and Statement is a subclass of this base class. Any CStatement might have
+ * an id associated with it, in case there was a label in the source code. This also provides an
+ * XcfaLocation, which can be used when jumping to this named location via a _goto_ instruction
  */
 public abstract class CStatement {
     protected final ParseContext parseContext;
@@ -39,6 +39,7 @@ public abstract class CStatement {
     private int offsetStart = -1;
     private int offsetEnd = -1;
     private String sourceText = "";
+    private ParserRuleContext ctx;
 
     protected CStatement(ParseContext parseContext) {
         this.parseContext = parseContext;
@@ -53,10 +54,10 @@ public void setId(String id) {
     }
 
     /**
-     * Returns the expression associated with a CStatement, which by default throws an exception, as not all subtypes
-     * will return one. For example, the C language statement `int a = (b = 0, 2)` will create a CCompound statement as
-     * the right-hand side of the assignment, whose associated expression will be 2, but the assignment to b has to come
-     * beforehand.
+     * Returns the expression associated with a CStatement, which by default throws an exception, as
+     * not all subtypes will return one. For example, the C language statement `int a = (b = 0, 2)`
+     * will create a CCompound statement as the right-hand side of the assignment, whose associated
+     * expression will be 2, but the assignment to b has to come beforehand.
      *
      * @return The expression associated with the statement.
      */
@@ -69,15 +70,17 @@ public CStatement getPostStatements() {
     }
 
     public void setPostStatements(CStatement postStatements) {
-        throw new UnsupportedFrontendElementException("Only CCompounds shall currently have pre- and post statements!");
+        throw new UnsupportedFrontendElementException(
+                "Only CCompounds shall currently have pre- and post statements!");
     }
 
     public CStatement getPreStatements() {
         return preStatements;
     }
 
     public void setPreStatements(CStatement preStatements) {
-        throw new UnsupportedFrontendElementException("Only CCompounds shall currently have pre- and post statements!");
+        throw new UnsupportedFrontendElementException(
+                "Only CCompounds shall currently have pre- and post statements!");
     }
 
     public abstract <P, R> R accept(CStatementVisitor<P, R> visitor, P param);
@@ -137,4 +140,12 @@ public String getSourceText() {
     public void setSourceText(String sourceText) {
         this.sourceText = sourceText;
     }
+
+    public ParserRuleContext getCtx() {
+        return ctx;
+    }
+
+    public void setCtx(ParserRuleContext ctx) {
+        this.ctx = ctx;
+    }
 }

subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcBackwardXcfaBuilder.java

@@ -15,6 +15,12 @@
  */
 package hu.bme.mit.theta.frontend.chc;
 
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool;
+import static hu.bme.mit.theta.frontend.chc.ChcUtils.createVars;
+import static hu.bme.mit.theta.frontend.chc.ChcUtils.getTailConditionLabels;
+import static hu.bme.mit.theta.frontend.chc.ChcUtils.transformConst;
+import static hu.bme.mit.theta.frontend.chc.ChcUtils.transformSort;
+
 import hu.bme.mit.theta.chc.frontend.dsl.gen.CHCBaseVisitor;
 import hu.bme.mit.theta.chc.frontend.dsl.gen.CHCParser;
 import hu.bme.mit.theta.core.decl.Decls;
@@ -36,20 +42,13 @@
 import hu.bme.mit.theta.xcfa.model.XcfaLocation;
 import hu.bme.mit.theta.xcfa.model.XcfaProcedureBuilder;
 import hu.bme.mit.theta.xcfa.passes.ProcedurePassManager;
-import kotlin.Pair;
-import org.antlr.v4.runtime.RuleContext;
-
 import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
 import java.util.Optional;
-
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool;
-import static hu.bme.mit.theta.frontend.chc.ChcUtils.createVars;
-import static hu.bme.mit.theta.frontend.chc.ChcUtils.getTailConditionLabels;
-import static hu.bme.mit.theta.frontend.chc.ChcUtils.transformConst;
-import static hu.bme.mit.theta.frontend.chc.ChcUtils.transformSort;
+import kotlin.Pair;
+import org.antlr.v4.runtime.RuleContext;
 
 public class ChcBackwardXcfaBuilder extends CHCBaseVisitor<Object> implements ChcXcfaBuilder {
     private final Map<String, XcfaProcedureBuilder> procedures = new HashMap<>();
@@ -67,8 +66,8 @@ public XcfaBuilder buildXcfa(CHCParser parser) {
 
         visit(parser.benchmark());
 
-//        xcfaBuilder.addProcess(procBuilder);
-//        xcfaBuilder.setMainProcess(procBuilder);
+        //        xcfaBuilder.addProcess(procBuilder);
+        //        xcfaBuilder.setMainProcess(procBuilder);
         return xcfaBuilder;
     }
 
@@ -103,9 +102,19 @@ public Object visitChc_assert(CHCParser.Chc_assertContext ctx) {
                     vars.put(ctx.chc_head().u_pred_atom().symbol(i++).getText(), param.getFirst());
             }
             XcfaLocation middle = createLocation(procedure);
-            XcfaEdge edge = new XcfaEdge(procedure.getInitLoc(), middle, new SequenceLabel(getTailConditionLabels(ctx.chc_tail(), vars)));
+            XcfaEdge edge =
+                    new XcfaEdge(
+                            procedure.getInitLoc(),
+                            middle,
+                            new SequenceLabel(getTailConditionLabels(ctx.chc_tail(), vars)),
+                            EmptyMetaData.INSTANCE);
             procedure.addEdge(edge);
-            createCalls(procedure, middle, procedure.getFinalLoc().get(), ctx.chc_tail().u_pred_atom(), vars);
+            createCalls(
+                    procedure,
+                    middle,
+                    procedure.getFinalLoc().get(),
+                    ctx.chc_tail().u_pred_atom(),
+                    vars);
         } else {
             String procName;
             if (ctx.chc_head() != null) {
@@ -115,7 +124,12 @@ public Object visitChc_assert(CHCParser.Chc_assertContext ctx) {
             }
             procedure = procedures.get(procName);
             Stmt returnTrue = AssignStmt.create(getOutParam(procedure), BoolLitExpr.of(true));
-            XcfaEdge edge = new XcfaEdge(procedure.getInitLoc(), procedure.getFinalLoc().get(), new StmtLabel(returnTrue));
+            XcfaEdge edge =
+                    new XcfaEdge(
+                            procedure.getInitLoc(),
+                            procedure.getFinalLoc().get(),
+                            new StmtLabel(returnTrue),
+                            EmptyMetaData.INSTANCE);
             procedure.addEdge(edge);
         }
         return super.visitChc_assert(ctx);
@@ -128,16 +142,26 @@ public Object visitChc_query(CHCParser.Chc_queryContext ctx) {
 
         Map<String, VarDecl<?>> vars = createVars(mainProcedure, ctx.var_decl());
         XcfaLocation middle = createLocation(mainProcedure);
-        XcfaEdge edge = new XcfaEdge(mainProcedure.getInitLoc(), middle, new SequenceLabel(getTailConditionLabels(ctx.chc_tail(), vars)));
+        XcfaEdge edge =
+                new XcfaEdge(
+                        mainProcedure.getInitLoc(),
+                        middle,
+                        new SequenceLabel(getTailConditionLabels(ctx.chc_tail(), vars)),
+                        EmptyMetaData.INSTANCE);
         mainProcedure.addEdge(edge);
-        createCalls(mainProcedure, middle, mainProcedure.getErrorLoc().get(), ctx.chc_tail().u_pred_atom(), vars);
+        createCalls(
+                mainProcedure,
+                middle,
+                mainProcedure.getErrorLoc().get(),
+                ctx.chc_tail().u_pred_atom(),
+                vars);
         return super.visitChc_query(ctx);
     }
 
     private int uniqeCounter = 0;
 
     private XcfaLocation createLocation(XcfaProcedureBuilder builder) {
-        XcfaLocation location = new XcfaLocation("l_" + uniqeCounter++);
+        XcfaLocation location = new XcfaLocation("l_" + uniqeCounter++, EmptyMetaData.INSTANCE);
         builder.addLoc(location);
         return location;
     }
@@ -156,35 +180,56 @@ private XcfaProcedureBuilder createProcedure(String procName) {
     }
 
     private VarDecl<?> getOutParam(XcfaProcedureBuilder procedure) {
-        Optional<Pair<VarDecl<?>, ParamDirection>> param = procedure.getParams()
-                .stream().filter(entry -> entry.getSecond() == ParamDirection.OUT).findAny();
+        Optional<Pair<VarDecl<?>, ParamDirection>> param =
+                procedure.getParams().stream()
+                        .filter(entry -> entry.getSecond() == ParamDirection.OUT)
+                        .findAny();
         return param.map(Pair::getFirst).orElse(null);
     }
 
-    private void createCalls(XcfaProcedureBuilder builder, XcfaLocation start, XcfaLocation end, List<CHCParser.U_pred_atomContext> uPreds, Map<String, VarDecl<?>> localVars) {
+    private void createCalls(
+            XcfaProcedureBuilder builder,
+            XcfaLocation start,
+            XcfaLocation end,
+            List<CHCParser.U_pred_atomContext> uPreds,
+            Map<String, VarDecl<?>> localVars) {
         XcfaLocation from = start;
         for (CHCParser.U_pred_atomContext uPred : uPreds) {
             XcfaLocation middle = createLocation(builder);
             XcfaLocation to = createLocation(builder);
 
             XcfaProcedureBuilder calledProcedure = procedures.get(uPred.u_predicate().getText());
-            VarDecl<BoolType> ret = Decls.Var(calledProcedure.getName() + "_ret_" + callCount++, Bool());
+            VarDecl<BoolType> ret =
+                    Decls.Var(calledProcedure.getName() + "_ret_" + callCount++, Bool());
             builder.addVar(ret);
             localVars.put(ret.getName(), ret);
-            List<String> paramNames = new ArrayList<>(uPred.symbol().stream().map(RuleContext::getText).toList());
+            List<String> paramNames =
+                    new ArrayList<>(uPred.symbol().stream().map(RuleContext::getText).toList());
             paramNames.add(0, ret.getName());
-            List<? extends Expr<?>> params = paramNames.stream().map(s -> localVars.get(s).getRef()).toList();
-
-            XcfaEdge callEdge = new XcfaEdge(from, middle, new InvokeLabel(calledProcedure.getName(), params, EmptyMetaData.INSTANCE));
+            List<? extends Expr<?>> params =
+                    paramNames.stream().map(s -> localVars.get(s).getRef()).toList();
+
+            XcfaEdge callEdge =
+                    new XcfaEdge(
+                            from,
+                            middle,
+                            new InvokeLabel(
+                                    calledProcedure.getName(), params, EmptyMetaData.INSTANCE),
+                            EmptyMetaData.INSTANCE);
             builder.addEdge(callEdge);
 
-            XcfaEdge assertEdge = new XcfaEdge(middle, to, new StmtLabel(AssumeStmt.of(ret.getRef())));
+            XcfaEdge assertEdge =
+                    new XcfaEdge(
+                            middle,
+                            to,
+                            new StmtLabel(AssumeStmt.of(ret.getRef())),
+                            EmptyMetaData.INSTANCE);
             builder.addEdge(assertEdge);
 
             from = to;
         }
         Stmt returnTrue = AssignStmt.create(getOutParam(builder), BoolLitExpr.of(true));
-        XcfaEdge edge = new XcfaEdge(from, end, new StmtLabel(returnTrue));
+        XcfaEdge edge = new XcfaEdge(from, end, new StmtLabel(returnTrue), EmptyMetaData.INSTANCE);
         builder.addEdge(edge);
     }
 }