Fixed negation and expansion order for subtraction

ftsrg · Nov 17, 2023 · f39ba00 · f39ba00
1 parent 1008f67
commit f39ba00
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 5 deletions.
diff --git a/...n/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/...n/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java
@@ -351,9 +351,11 @@ public Expr<?> visitAdditiveExpression(CParser.AdditiveExpressionContext ctx) {
             CComplexType smallestCommonType = CComplexType.getSmallestCommonType(types, parseContext);
             List<Expr<?>> collect = new ArrayList<>();
             for (int i = 0; i < exprs.size(); i++) {
-                Expr<?> expr = (i == 0 || ctx.signs.get(i - 1).getText().equals("+")) ? exprs.get(i) : AbstractExprs.Neg(exprs.get(i));
-                parseContext.getMetadata().create(expr, "cType", CComplexType.getType(exprs.get(i), parseContext));
-                Expr<?> castTo = smallestCommonType.castTo(expr);
+                parseContext.getMetadata().create(exprs.get(i), "cType", CComplexType.getType(exprs.get(i), parseContext));
+                Expr<?> castTo = smallestCommonType.castTo(exprs.get(i));
+                if (i != 0 && ctx.signs.get(i - 1).getText().equals("-")) {
+                    castTo = AbstractExprs.Neg(castTo);
+                }
                 collect.add(castTo);
             }
             Expr<?> add = AbstractExprs.Add(collect);

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt
@@ -39,7 +39,7 @@ import hu.bme.mit.theta.common.visualization.writer.WebDebuggerLogger
 import hu.bme.mit.theta.frontend.ParseContext
 import hu.bme.mit.theta.frontend.chc.ChcFrontend
 import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig
-import hu.bme.mit.theta.llvm2xcfa.ArithmeticType
+import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.ArithmeticType
 import hu.bme.mit.theta.llvm2xcfa.XcfaUtils.fromFile
 import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager
 import hu.bme.mit.theta.xcfa.analysis.ErrorDetection
@@ -88,6 +88,10 @@ class XcfaCli(private val args: Array<String>) {
         description = "Level of LBE (NO_LBE, LBE_LOCAL, LBE_SEQ, LBE_FULL)")
     var lbeLevel: LbePass.LbeLevel = LbePass.LbeLevel.LBE_SEQ
 
+    @Parameter(names = ["--arithmetic"],
+        description = "Arithmetic type (efficient, bitvector, integer)")
+    var arithmetic: ArithmeticType = ArithmeticType.efficient
+
     @Parameter(names = ["--unroll"], description = "Max number of loop iterations to unroll")
     var loopUnroll: Int = 50
 
@@ -215,6 +219,7 @@ class XcfaCli(private val args: Array<String>) {
 
         logger.write(Logger.Level.INFO, "Parsing the input $input as $inputType\n")
         val parseContext = ParseContext()
+        parseContext.arithmetic = arithmetic
         val xcfa = getXcfa(logger, explicitProperty, parseContext, uniqueWarningLogger)
         ConeOfInfluence = if (parseContext.multiThreading) XcfaCoiMultiThread(xcfa) else XcfaCoiSingleThread(xcfa)
         logger.write(Logger.Level.INFO, "Frontend finished: ${xcfa.name}  (in ${
@@ -421,7 +426,7 @@ class XcfaCli(private val args: Array<String>) {
                     xcfaFromC
                 }
 
-                InputType.LLVM -> fromFile(input!!, ArithmeticType.efficient)
+                InputType.LLVM -> fromFile(input!!, hu.bme.mit.theta.llvm2xcfa.ArithmeticType.efficient)
 
                 InputType.JSON -> {
                     val gson = getGson()