Added code from CHC2C implementation

subprojects/frontends/c-frontend/src/main/antlr/C.g4

@@ -31,7 +31,8 @@ grammar C;
 
 
 primaryExpression
-    :   Identifier                                                          # primaryExpressionId
+    :   '__PRETTY_FUNC__'                                                   # gccPrettyFunc
+    |   Identifier                                                          # primaryExpressionId
     |   Constant                                                            # primaryExpressionConstant
     |   StringLiteral+                                                      # primaryExpressionStrings
     |   '(' expression ')'                                                  # primaryExpressionBraceExpression

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java

@@ -388,41 +388,43 @@ public Expr<?> visitMultiplicativeExpression(CParser.MultiplicativeExpressionCon
 
     /**
      * Conversion from C (/) semantics to solver (div) semantics.
+     *
      * @param a dividend
      * @param b divisor
      * @return expression representing C division semantics with solver operations
      */
     private Expr<?> createIntDiv(Expr<?> a, Expr<?> b) {
         DivExpr<?> aDivB = Div(a, b);
         return Ite(Geq(a, Int(0)),          // if (a >= 0)
-            aDivB,                                //   a div b
-                                                  // else
-            Ite(Neq(Mod(a, b), Int(0)),     //   if (a mod b != 0)
-                Ite(Geq(b, Int(0)),         //     if (b >= 0)
-                    Add(aDivB, Int(1)),     //       a div b + 1
-                                                  //     else
-                    Sub(aDivB, Int(1))      //       a div b - 1
-                ),                                //   else
-                aDivB                             //     a div b
-            )
+                aDivB,                                //   a div b
+                // else
+                Ite(Neq(Mod(a, b), Int(0)),     //   if (a mod b != 0)
+                        Ite(Geq(b, Int(0)),         //     if (b >= 0)
+                                Add(aDivB, Int(1)),     //       a div b + 1
+                                //     else
+                                Sub(aDivB, Int(1))      //       a div b - 1
+                        ),                                //   else
+                        aDivB                             //     a div b
+                )
         );
     }
 
     /**
      * Conversion from C (%) semantics to solver (mod) semantics.
+     *
      * @param a dividend
      * @param b divisor
      * @return expression representing C modulo semantics with solver operations
      */
     private Expr<?> createIntMod(Expr<?> a, Expr<?> b) {
         ModExpr<?> aModB = Mod(a, b);
         return Ite(Geq(a, Int(0)),  // if (a >= 0)
-            aModB,                        //   a mod b
-                                          // else
-            Ite(Geq(b, Int(0)),     //   if (b >= 0)
-                Sub(aModB, b),            //     a mod b - b
-                Add(aModB, b)             //     a mod b + b
-            )
+                aModB,                        //   a mod b
+                // else
+                Ite(Geq(b, Int(0)),     //   if (b >= 0)
+                        Sub(aModB, b),            //     a mod b - b
+                        Add(aModB, b)             //     a mod b + b
+                )
         );
     }
 
@@ -625,6 +627,15 @@ public Expr<?> visitPostfixExpressionBrackets(CParser.PostfixExpressionBracketsC
         return ctx.expression().accept(this);
     }
 
+    @Override
+    public Expr<?> visitGccPrettyFunc(CParser.GccPrettyFuncContext ctx) {
+        System.err.println("WARNING: gcc intrinsic encountered in place of an expression, using a literal 0 instead.");
+        CComplexType signedInt = CComplexType.getSignedInt(parseContext);
+        LitExpr<?> zero = signedInt.getNullValue();
+        parseContext.getMetadata().create(zero, "cType", signedInt);
+        return zero;
+    }
+
     @Override
     public Expr<?> visitPrimaryExpressionId(CParser.PrimaryExpressionIdContext ctx) {
         return getVar(ctx.Identifier().getText()).getRef();

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/UnsupportedInitializer.java

@@ -0,0 +1,42 @@
+/*
+ *  Copyright 2023 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.
+ */
+
+package hu.bme.mit.theta.frontend.transformation.grammar.expression;
+
+import hu.bme.mit.theta.core.model.Valuation;
+import hu.bme.mit.theta.core.type.LitExpr;
+import hu.bme.mit.theta.core.type.NullaryExpr;
+import hu.bme.mit.theta.core.type.inttype.IntType;
+
+import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int;
+
+public class UnsupportedInitializer extends NullaryExpr<IntType> {
+
+    @Override
+    public IntType getType() {
+        return Int();
+    }
+
+    @Override
+    public LitExpr<IntType> eval(Valuation val) {
+        throw new UnsupportedOperationException("UnsupportedInitializer expressions are not supported.");
+    }
+
+    @Override
+    public String toString() {
+        return "UnsupportedInitializer";
+    }
+}

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/DeclarationVisitor.java

@@ -19,9 +19,11 @@
 import hu.bme.mit.theta.c.frontend.dsl.gen.CBaseVisitor;
 import hu.bme.mit.theta.c.frontend.dsl.gen.CParser;
 import hu.bme.mit.theta.frontend.ParseContext;
+import hu.bme.mit.theta.frontend.transformation.grammar.expression.UnsupportedInitializer;
 import hu.bme.mit.theta.frontend.transformation.grammar.function.FunctionVisitor;
 import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.TypedefVisitor;
 import hu.bme.mit.theta.frontend.transformation.model.declaration.CDeclaration;
+import hu.bme.mit.theta.frontend.transformation.model.statements.CExpr;
 import hu.bme.mit.theta.frontend.transformation.model.statements.CInitializerList;
 import hu.bme.mit.theta.frontend.transformation.model.statements.CStatement;
 import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleType;
@@ -81,13 +83,17 @@ public List<CDeclaration> getDeclarations(CParser.DeclarationSpecifiersContext d
                                 "Initializer list designators not yet implemented!");
                         CInitializerList cInitializerList = new CInitializerList(
                                 cSimpleType.getActualType(), parseContext);
-                        for (CParser.InitializerContext initializer : context.initializer()
-                                .initializerList().initializers) {
-                            CStatement expr = initializer.assignmentExpression()
-                                    .accept(functionVisitor);
-                            cInitializerList.addStatement(null /* TODO: add designator */, expr);
+                        try {
+                            for (CParser.InitializerContext initializer : context.initializer()
+                                    .initializerList().initializers) {
+                                CStatement expr = initializer.assignmentExpression().accept(functionVisitor);
+                                cInitializerList.addStatement(null /* TODO: add designator */, expr);
+                            }
+                            initializerExpression = cInitializerList;
+                        } catch (NullPointerException e) {
+                            initializerExpression = new CExpr(new UnsupportedInitializer(), parseContext);
+                            parseContext.getMetadata().create(initializerExpression.getExpression(), "cType", cSimpleType);
                         }
-                        initializerExpression = cInitializerList;
                     } else {
                         initializerExpression = context.initializer().assignmentExpression()
                                 .accept(functionVisitor);

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java

@@ -20,6 +20,9 @@
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.LitExpr;
 import hu.bme.mit.theta.core.type.Type;
+import hu.bme.mit.theta.core.type.arraytype.ArrayType;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.type.inttype.IntType;
 import hu.bme.mit.theta.frontend.ParseContext;
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CArray;
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CCompound;
@@ -117,7 +120,7 @@ public CComplexType getSmallestCommonType(CComplexType type) {
     }
 
     public String getTypeName() {
-        throw new RuntimeException("Type name could not be queried from this type!");
+        throw new RuntimeException("Type name could not be queried from this type: " + this);
     }
 
     public int width() {
@@ -138,7 +141,20 @@ public static CComplexType getType(Expr<?> expr, ParseContext parseContext) {
             return (CComplexType) cTypeOptional.get();
         } else if (cTypeOptional.isPresent() && cTypeOptional.get() instanceof CSimpleType) {
             return ((CSimpleType) cTypeOptional.get()).getActualType();
-        } else throw new RuntimeException("Type not known for expression: " + expr);
+        } else {
+            return getType(expr.getType(), parseContext);
+//            throw new RuntimeException("Type not known for expression: " + expr);
+        }
+    }
+
+    private static CComplexType getType(Type type, ParseContext parseContext) {
+        if (type instanceof IntType) {
+            return new CSignedInt(null, parseContext);
+        } else if (type instanceof ArrayType<?, ?> aType) {
+            return new CArray(null, getType(aType.getElemType(), parseContext), parseContext);
+        } else if (type instanceof BoolType) {
+            return new CBool(null, parseContext);
+        } else throw new RuntimeException("Not yet implemented for type: " + type);
     }
 
 

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CVoid.java

@@ -28,4 +28,9 @@ public CVoid(CSimpleType origin, ParseContext parseContext) {
     public <T, R> R accept(CComplexTypeVisitor<T, R> visitor, T param) {
         return visitor.visit(this, param);
     }
+
+    @Override
+    public String getTypeName() {
+        return "void";
+    }
 }

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CDouble.java

@@ -31,4 +31,9 @@ public CDouble(CSimpleType origin, ParseContext parseContext) {
     public <T, R> R accept(CComplexTypeVisitor<T, R> visitor, T param) {
         return visitor.visit(this, param);
     }
+
+    @Override
+    public String getTypeName() {
+        return "double";
+    }
 }

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CFloat.java

@@ -31,4 +31,9 @@ public CFloat(CSimpleType origin, ParseContext parseContext) {
     public <T, R> R accept(CComplexTypeVisitor<T, R> visitor, T param) {
         return visitor.visit(this, param);
     }
+
+    @Override
+    public String getTypeName() {
+        return "float";
+    }
 }

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CLongDouble.java

@@ -31,4 +31,9 @@ public CLongDouble(CSimpleType origin, ParseContext parseContext) {
     public <T, R> R accept(CComplexTypeVisitor<T, R> visitor, T param) {
         return visitor.visit(this, param);
     }
+
+    @Override
+    public String getTypeName() {
+        return "long double";
+    }
 }

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

@@ -26,21 +26,41 @@
 import hu.bme.mit.theta.core.type.Type;
 import hu.bme.mit.theta.core.type.booltype.BoolLitExpr;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
-import hu.bme.mit.theta.xcfa.model.*;
-import hu.bme.mit.theta.xcfa.passes.ChcPasses;
+import hu.bme.mit.theta.xcfa.model.EmptyMetaData;
+import hu.bme.mit.theta.xcfa.model.InvokeLabel;
+import hu.bme.mit.theta.xcfa.model.ParamDirection;
+import hu.bme.mit.theta.xcfa.model.SequenceLabel;
+import hu.bme.mit.theta.xcfa.model.StmtLabel;
+import hu.bme.mit.theta.xcfa.model.XcfaBuilder;
+import hu.bme.mit.theta.xcfa.model.XcfaEdge;
+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.*;
+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.*;
+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;
 
 public class ChcBackwardXcfaBuilder extends CHCBaseVisitor<Object> implements ChcXcfaBuilder {
     private final Map<String, XcfaProcedureBuilder> procedures = new HashMap<>();
+    private final ProcedurePassManager procedurePassManager;
     private XcfaBuilder xcfaBuilder;
     private int callCount = 0;
 
+    public ChcBackwardXcfaBuilder(final ProcedurePassManager procedurePassManager) {
+        this.procedurePassManager = procedurePassManager;
+    }
+
     @Override
     public XcfaBuilder buildXcfa(CHCParser parser) {
         xcfaBuilder = new XcfaBuilder("chc");
@@ -123,7 +143,7 @@ private XcfaLocation createLocation(XcfaProcedureBuilder builder) {
     }
 
     private XcfaProcedureBuilder createProcedure(String procName) {
-        XcfaProcedureBuilder builder = new XcfaProcedureBuilder(procName, new ChcPasses());
+        XcfaProcedureBuilder builder = new XcfaProcedureBuilder(procName, procedurePassManager);
         builder.setName(procName);
         builder.addParam(Decls.Var(procName + "_ret", Bool()), ParamDirection.OUT);
 

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

@@ -22,27 +22,41 @@
 import hu.bme.mit.theta.core.stmt.AssignStmt;
 import hu.bme.mit.theta.core.stmt.HavocStmt;
 import hu.bme.mit.theta.core.type.Type;
-import hu.bme.mit.theta.xcfa.model.*;
-import hu.bme.mit.theta.xcfa.passes.ChcPasses;
+import hu.bme.mit.theta.xcfa.model.EmptyMetaData;
+import hu.bme.mit.theta.xcfa.model.SequenceLabel;
+import hu.bme.mit.theta.xcfa.model.StmtLabel;
+import hu.bme.mit.theta.xcfa.model.XcfaBuilder;
+import hu.bme.mit.theta.xcfa.model.XcfaEdge;
+import hu.bme.mit.theta.xcfa.model.XcfaLabel;
+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 java.util.ArrayList;
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
 
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool;
-import static hu.bme.mit.theta.frontend.chc.ChcUtils.*;
+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;
 
 public class ChcForwardXcfaBuilder extends CHCBaseVisitor<Object> implements ChcXcfaBuilder {
+    private final ProcedurePassManager procedurePassManager;
     private XcfaProcedureBuilder builder;
     private XcfaLocation initLocation;
     private XcfaLocation errorLocation;
     private final Map<String, UPred> locations = new HashMap<>();
 
+    public ChcForwardXcfaBuilder(final ProcedurePassManager procedurePassManager) {
+        this.procedurePassManager = procedurePassManager;
+    }
+
     @Override
     public XcfaBuilder buildXcfa(CHCParser parser) {
         XcfaBuilder xcfaBuilder = new XcfaBuilder("chc");
-        builder = new XcfaProcedureBuilder("main", new ChcPasses());
+        builder = new XcfaProcedureBuilder("main", procedurePassManager);
         builder.createInitLoc();
         builder.createErrorLoc();
         builder.createFinalLoc();

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

@@ -18,6 +18,8 @@
 import hu.bme.mit.theta.chc.frontend.dsl.gen.CHCLexer;
 import hu.bme.mit.theta.chc.frontend.dsl.gen.CHCParser;
 import hu.bme.mit.theta.xcfa.model.XcfaBuilder;
+import hu.bme.mit.theta.xcfa.passes.ProcedurePassManager;
+import org.antlr.v4.runtime.BailErrorStrategy;
 import org.antlr.v4.runtime.CharStream;
 import org.antlr.v4.runtime.CommonTokenStream;
 
@@ -35,12 +37,13 @@ public ChcFrontend(ChcTransformation transformation) {
         chcTransformation = transformation;
     }
 
-    public XcfaBuilder buildXcfa(CharStream charStream) {
+    public XcfaBuilder buildXcfa(CharStream charStream, ProcedurePassManager procedurePassManager) {
         ChcUtils.init(charStream);
         CHCParser parser = new CHCParser(new CommonTokenStream(new CHCLexer(charStream)));
+        parser.setErrorHandler(new BailErrorStrategy());
         ChcXcfaBuilder chcXcfaBuilder = switch (chcTransformation) {
-            case FORWARD -> new ChcForwardXcfaBuilder();
-            case BACKWARD -> new ChcBackwardXcfaBuilder();
+            case FORWARD -> new ChcForwardXcfaBuilder(procedurePassManager);
+            case BACKWARD -> new ChcBackwardXcfaBuilder(procedurePassManager);
             default ->
                     throw new RuntimeException("Should not be here; adapt PORTFOLIO to FW/BW beforehand.");
         };

subprojects/frontends/llvm/build.gradle.kts

@@ -52,7 +52,7 @@ fun llvmConfigFlags(vararg args: String): Array<String> {
     } catch (e: IOException) {
         e.printStackTrace()
         arrayOf()
-    }.also { println("LLVM flags (${args.toList()}): ${it.toList()}") }
+    }//.also { println("LLVM flags (${args.toList()}): ${it.toList()}") }
 }
 
 fun jniConfigFlags(): Array<String> {
@@ -67,7 +67,7 @@ fun jniConfigFlags(): Array<String> {
     return arrayOf(
         "-I${mainInclude.absolutePath}",
         "-I${linuxInclude.absolutePath}",
-    ).also { println("JNI flags: ${it.toList()}") }
+    )//.also { println("JNI flags: ${it.toList()}") }
 }
 
 library {