Merge pull request #365 from ftsrg/chcfix

CHC to XCFA fixes

Author: mondokm

build.gradle.kts

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

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

@@ -130,6 +130,9 @@ private List<XcfaLabel> getIncomingAssignments(
             CHCParser.Chc_tailContext tail, Map<String, VarDecl<?>> localVars) {
         List<XcfaLabel> labels = new ArrayList<>();
         UPred from = locations.get(getTailFrom(tail).getName());
+        if (tail.u_pred_atom().isEmpty()) {
+            localVars.values().forEach(var -> labels.add(new StmtLabel(HavocStmt.of(var))));
+        }
         tail.u_pred_atom()
                 .forEach(
                         u_pred -> {

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

@@ -45,11 +45,7 @@
 import hu.bme.mit.theta.xcfa.model.StmtLabel;
 import hu.bme.mit.theta.xcfa.model.XcfaLabel;
 import hu.bme.mit.theta.xcfa.model.XcfaProcedureBuilder;
-import java.util.ArrayList;
-import java.util.Collections;
-import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
+import java.util.*;
 import org.antlr.v4.runtime.CharStream;
 import org.antlr.v4.runtime.ParserRuleContext;
 import org.antlr.v4.runtime.misc.Interval;
@@ -101,17 +97,29 @@ public static String getOriginalText(ParserRuleContext ctx) {
         return charStream.getText(new Interval(ctx.start.getStartIndex(), ctx.stop.getStopIndex()));
     }
 
+    private static final Map<Tuple2<String, Type>, VarDecl<?>> cache = new LinkedHashMap<>();
+
+    private static VarDecl<?> createVar(XcfaProcedureBuilder builder, String name, Type type) {
+        var ret =
+                cache.computeIfAbsent(
+                        Tuple2.of(name, type),
+                        objects -> {
+                            var v = Decls.Var(name, type);
+                            builder.addVar(v);
+                            return v;
+                        });
+        transformConst(Decls.Const(name, type), false);
+        return ret;
+    }
+
     public static Map<String, VarDecl<?>> createVars(
             XcfaProcedureBuilder builder, List<CHCParser.Var_declContext> var_decls) {
         resetSymbolTable();
         Map<String, VarDecl<?>> vars = new HashMap<>();
         for (CHCParser.Var_declContext var_decl : var_decls) {
             String name = var_decl.symbol().getText();
-            String varName = name + "_" + builder.getEdges().size();
             Type type = transformSort(var_decl.sort());
-            VarDecl<?> var = Decls.Var(varName, type);
-            builder.addVar(var);
-            transformConst(Decls.Const(name, type), false);
+            VarDecl<?> var = createVar(builder, name, type);
             vars.put(name, var);
         }
         return vars;

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt

@@ -39,6 +39,8 @@ import hu.bme.mit.theta.core.type.fptype.FpType
 import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
 import hu.bme.mit.theta.core.type.inttype.IntLitExpr
 import hu.bme.mit.theta.core.type.inttype.IntType
+import hu.bme.mit.theta.core.type.rattype.RatExprs.Rat
+import hu.bme.mit.theta.core.type.rattype.RatType
 import hu.bme.mit.theta.core.utils.BvUtils
 import hu.bme.mit.theta.core.utils.FpUtils
 import hu.bme.mit.theta.core.utils.StmtUtils
@@ -119,6 +121,7 @@ fun XCFA.toMonolithicExpr(parseContext: ParseContext, initValues: Boolean = fals
                 it.ref,
                 BvUtils.bigIntegerToNeutralBvLitExpr(BigInteger.ZERO, (it.type as BvType).size),
               )
+            is RatType -> Eq(it.ref, Rat(0, 1))
             is FpType ->
               FpAssign(
                 it.ref as Expr<FpType>,

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToMddChecker.kt

@@ -35,6 +35,7 @@ import hu.bme.mit.theta.xcfa.cli.params.*
 import hu.bme.mit.theta.xcfa.cli.utils.getSolver
 import hu.bme.mit.theta.xcfa.getFlatLabels
 import hu.bme.mit.theta.xcfa.model.XCFA
+import kotlin.jvm.optionals.getOrNull
 
 fun getMddChecker(
   xcfa: XCFA,
@@ -70,11 +71,18 @@ fun getMddChecker(
   val solverPool = SolverPool(refinementSolverFactory)
   val iterationStrategy = mddConfig.iterationStrategy
 
-  return MddChecker.create<ExprAction>(
-    monolithicExpr,
-    variableOrder,
-    solverPool,
-    logger,
-    iterationStrategy,
-  )
+  val checker =
+    MddChecker.create<ExprAction>(
+      monolithicExpr,
+      variableOrder,
+      solverPool,
+      logger,
+      iterationStrategy,
+    )
+  return SafetyChecker<MddProof, MddCex, UnitPrec> { input ->
+    val result = checker.check(input)
+    val stats = result.stats.getOrNull()
+    stats?.keySet()?.forEach { key -> logger.writeln(Logger.Level.INFO, "$key: ${stats[key]}") }
+    result
+  }
 }

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/chccomp25.kt

@@ -87,6 +87,7 @@ fun chcCompPortfolio25(
           ConfigNode(
             "Bounded-BMC-$inProcess",
             baseBoundedConfig.adaptConfig(
+              inProcess = inProcess,
               bmcEnabled = true,
               indEnabled = false,
               itpEnabled = false,
@@ -99,6 +100,7 @@ fun chcCompPortfolio25(
           ConfigNode(
             "Bounded-KIND-$inProcess",
             baseBoundedConfig.adaptConfig(
+              inProcess = inProcess,
               bmcEnabled = true,
               indEnabled = true,
               itpEnabled = false,
@@ -113,6 +115,7 @@ fun chcCompPortfolio25(
           ConfigNode(
             "Bounded-IMC-$inProcess",
             baseBoundedConfig.adaptConfig(
+              inProcess = inProcess,
               bmcEnabled = false,
               indEnabled = false,
               itpEnabled = true,

subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt

@@ -155,12 +155,7 @@ class XcfaCliVerifyTest {
           "/chc/chc-LIA-Lin_000.smt2",
           ChcFrontend.ChcTransformation.FORWARD,
           "--domain PRED_CART",
-        ),
-        Arguments.of(
-          "/chc/chc-LIA-Arrays_000.smt2",
-          ChcFrontend.ChcTransformation.BACKWARD,
-          "--domain PRED_CART --search BFS",
-        ),
+        )
       )
     }
   }

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/EliminateSelfLoops.kt

@@ -16,31 +16,29 @@
 package hu.bme.mit.theta.xcfa.passes
 
 import hu.bme.mit.theta.xcfa.model.*
-import java.util.stream.Collectors
 
 class EliminateSelfLoops : ProcedurePass {
 
   override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder {
-    val selfLoops: Set<XcfaEdge> =
-      builder
-        .getEdges()
-        .stream()
-        .filter { xcfaEdge -> xcfaEdge.source === xcfaEdge.target }
-        .collect(Collectors.toSet())
-    for (selfLoop in selfLoops) {
-      builder.removeEdge(selfLoop)
-      val source = selfLoop.source
-      val target =
-        XcfaLocation(source.name + XcfaLocation.uniqueCounter(), metadata = source.metadata)
-      builder.addLoc(target)
-      for (outgoingEdge in LinkedHashSet(source.outgoingEdges)) {
-        builder.removeEdge(outgoingEdge)
+    while (true) {
+      val selfLoop =
+        builder.getEdges().firstOrNull { xcfaEdge -> xcfaEdge.source === xcfaEdge.target }
+      if (selfLoop != null) {
+        builder.removeEdge(selfLoop)
+        val source = selfLoop.source
+        val target =
+          XcfaLocation(
+            source.name + "_selfloop_" + XcfaLocation.uniqueCounter(),
+            metadata = source.metadata,
+          )
+        builder.addLoc(target)
+        builder.addEdge(XcfaEdge(source, target, selfLoop.label, selfLoop.metadata))
         builder.addEdge(
-          XcfaEdge(target, outgoingEdge.target, outgoingEdge.label, outgoingEdge.metadata)
+          XcfaEdge(target, source, SequenceLabel(listOf(NopLabel)), selfLoop.metadata)
         )
+      } else {
+        break
       }
-      builder.addEdge(XcfaEdge(source, target, selfLoop.label, selfLoop.metadata))
-      builder.addEdge(XcfaEdge(target, source, SequenceLabel(listOf(NopLabel)), selfLoop.metadata))
     }
     builder.metaData["noSelfLoops"] = Unit
     return builder