Various fixes to tests and grammar

ftsrg · Apr 26, 2024 · 217fd3c · 217fd3c
1 parent 1f24632
commit 217fd3c
Show file tree

Hide file tree

Showing 19 changed files with 227 additions and 177 deletions.
diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/ptr/PtrAnalysisTest.kt b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/ptr/PtrAnalysisTest.kt
@@ -38,7 +38,8 @@ class PtrAnalysisTest {
     companion object {
         private val x = Var("x", Int())
 
-        private val explTop = PtrState(ExplState.top())
+        private val explTop0 = PtrState(ExplState.top(), nextCnt = 0)
+        private val explTop1 = PtrState(ExplState.top(), nextCnt = 1)
 
         private val emptyAction = PtrActionStub(listOf(), emptyMap())
         private val readLiteralOnly = PtrActionStub(listOf(Assume(Eq(Dereference(Int(0), Int(1), Int()), Int(0)))),
@@ -51,12 +52,13 @@ class PtrAnalysisTest {
         @JvmStatic
         fun testInputs(): Collection<Arguments> {
             return listOf(
-                Arguments.of(explTop, emptyAction, emptyPrec,
-                    listOf(explTop)),
-                Arguments.of(explTop, readLiteralOnly, emptyPrec,
-                    listOf(explTop)),
-                Arguments.of(explTop, writeLiteralOnly, emptyPrec,
-                    listOf(PtrState(ExplState.top(), writeLiteralOnly.nextWriteTriples(prec.trackedDerefParams)))),
+                Arguments.of(explTop0, emptyAction, emptyPrec,
+                    listOf(explTop0)),
+                Arguments.of(explTop0, readLiteralOnly, emptyPrec,
+                    listOf(explTop1)),
+                Arguments.of(explTop0, writeLiteralOnly, emptyPrec,
+                    listOf(
+                        PtrState(ExplState.top(), writeLiteralOnly.nextWriteTriples(emptyPrec.trackedDerefParams), 1))),
             )
         }
     }

diff --git a/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/dsl/ExprTest.kt b/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/dsl/ExprTest.kt
@@ -223,7 +223,6 @@ class ExprTest {
                     emptyMap<Symbol, Decl<*>>()),
 
                 arrayOf(Dereference(Int(0), Int(1), Int()), "(deref 0 1 Int)", emptyMap<Symbol, Decl<*>>()),
-                arrayOf(Reference(Int(0), Int()), "(ref 0 Int)", emptyMap<Symbol, Decl<*>>()),
             )
         }
     }

diff --git a/subprojects/frontends/c-frontend/src/main/antlr/C.g4 b/subprojects/frontends/c-frontend/src/main/antlr/C.g4
@@ -137,19 +137,23 @@ multiplicativeExpression
     ;
 
 additiveExpression
-    :   multiplicativeExpression (signs+=('+'|'-') multiplicativeExpression)*
+    :   LeftParen multiplicativeExpression RightParen (signs+=('+'|'-') (multiplicativeExpression | LeftParen multiplicativeExpression RightParen))* // TODO: all others as well?
+    |   multiplicativeExpression (signs+=('+'|'-') multiplicativeExpression)*
     ;
 
 shiftExpression
-    :   additiveExpression (signs+=('<<'|'>>') additiveExpression)*
+    :   LeftParen additiveExpression RightParen (signs+=('<<'|'>>') (additiveExpression | LeftParen additiveExpression RightParen))* // TODO: all others as well?
+    |   additiveExpression (signs+=('<<'|'>>') additiveExpression)*
     ;
 
 relationalExpression
-    :   shiftExpression (signs+=('<'|'>'|'<='|'>=') shiftExpression)*
+    :   LeftParen shiftExpression RightParen (signs+=('<'|'>'|'<='|'>=') (shiftExpression | LeftParen shiftExpression RightParen))* // TODO: all others as well?
+    |   shiftExpression (signs+=('<'|'>'|'<='|'>=') shiftExpression)*
     ;
 
 equalityExpression
-    :   relationalExpression (signs+=('=='| '!=') relationalExpression)*
+    :   LeftParen relationalExpression RightParen (signs+=('=='| '!=') (relationalExpression | LeftParen relationalExpression RightParen))* // TODO: all others as well?
+    |   relationalExpression (signs+=('=='| '!=') relationalExpression)*
     ;
 
 andExpression

diff --git a/.../main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java b/.../main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java
@@ -61,6 +61,7 @@
 import hu.bme.mit.theta.frontend.transformation.model.statements.CSwitch;
 import hu.bme.mit.theta.frontend.transformation.model.statements.CWhile;
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType;
+import hu.bme.mit.theta.frontend.transformation.model.types.complex.CVoid;
 import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleType;
 import hu.bme.mit.theta.frontend.transformation.model.types.simple.Struct;
 import org.antlr.v4.runtime.ParserRuleContext;
@@ -492,7 +493,7 @@ public CStatement visitBodyDeclaration(CParser.BodyDeclarationContext ctx) {
                     }
                 } else {
                     VarDecl<?> varDecl = declaration.getVarDecls().get(0);
-                    if (!(varDecl.getType() instanceof ArrayType) && !(varDecl.getType() instanceof BoolType)) {
+                    if (!(varDecl.getType() instanceof ArrayType) && !(varDecl.getType() instanceof BoolType) && !(CComplexType.getType(varDecl.getRef(), parseContext) instanceof CVoid)) {
                         AssumeStmt assumeStmt = CComplexType.getType(varDecl.getRef(), parseContext).limit(varDecl.getRef());
                         CAssume cAssume = new CAssume(assumeStmt, parseContext);
                         compound.getcStatementList().add(cAssume);

diff --git a/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTermTransformer.java b/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTermTransformer.java
@@ -26,7 +26,6 @@
 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.abstracttype.AbstractExprs;
 import hu.bme.mit.theta.core.type.arraytype.ArrayInitExpr;
 import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr;
 import hu.bme.mit.theta.core.type.arraytype.ArrayType;
@@ -82,11 +81,13 @@
 import static com.google.common.collect.ImmutableList.toImmutableList;
 import static hu.bme.mit.theta.core.decl.Decls.Const;
 import static hu.bme.mit.theta.core.decl.Decls.Param;
+import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Exists;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Forall;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;
+import static hu.bme.mit.theta.core.type.fptype.FpExprs.FpAssign;
 import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int;
 import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat;
 
@@ -114,7 +115,7 @@ public JavaSMTTermTransformer(final JavaSMTSymbolTable symbolTable, SolverContex
         addFunc("ite", exprTernaryOperator(hu.bme.mit.theta.core.type.anytype.IteExpr::create));
         addFunc("if", exprTernaryOperator(hu.bme.mit.theta.core.type.anytype.IteExpr::create));
         addFunc("prime", exprUnaryOperator(hu.bme.mit.theta.core.type.anytype.PrimeExpr::of));
-        addFunc("=", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Eq));
+        addFunc("=", exprBinaryOperator((expr, expr2) -> expr.getType() instanceof FpType ? FpAssign((Expr<FpType>) expr, (Expr<FpType>) expr2) : Eq(expr, expr2)));
         addFunc(">=", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Geq));
         addFunc(">", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Gt));
         addFunc("<=", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Leq));
@@ -249,7 +250,7 @@ public JavaSMTTermTransformer(final JavaSMTSymbolTable symbolTable, SolverContex
         });
         environment.put(Tuple2.of("EqZero", 1), (term, args, model, vars) -> {
             final Expr<?> op = transform(args.get(0), model, vars);
-            return AbstractExprs.Eq(op, TypeUtils.getDefaultValue(op.getType()));
+            return Eq(op, TypeUtils.getDefaultValue(op.getType()));
         });
         environment.put(Tuple2.of("fp", 3), (term, args, model, vars) -> {
             final Expr<BvType> op1 = (Expr<BvType>) transform(args.get(0), model, vars);

diff --git a/.../solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTransformerTest.java b/.../solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTransformerTest.java
@@ -20,10 +20,13 @@
 import hu.bme.mit.theta.common.OsHelper.OperatingSystem;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.Type;
+import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs;
 import hu.bme.mit.theta.core.type.arraytype.ArrayInitExpr;
 import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
 import hu.bme.mit.theta.core.type.booltype.QuantifiedExpr;
 import hu.bme.mit.theta.core.type.bvtype.BvType;
+import hu.bme.mit.theta.core.type.fptype.FpExprs;
 import hu.bme.mit.theta.core.type.fptype.FpType;
 import hu.bme.mit.theta.core.type.functype.FuncType;
 import hu.bme.mit.theta.core.type.rattype.RatType;
@@ -42,10 +45,10 @@
 
 import java.util.Collection;
 import java.util.Set;
+import java.util.function.BiFunction;
 import java.util.function.Predicate;
 import java.util.stream.Collectors;
 
-import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not;
 import static org.junit.Assert.assertNotNull;
 import static org.junit.Assume.assumeFalse;
@@ -115,12 +118,14 @@ public void testRoundtripTransformer() throws Exception {
                     throw e; // for functions, we don't want the solver to step in
                 }
                 try (final var solver = JavaSMTSolverFactory.create(this.solver, new String[]{}).createSolver()) {
+                    BiFunction<Expr, Expr, Expr<BoolType>> eq = expr.getType() instanceof FpType ? FpExprs::FpAssign : AbstractExprs::Eq;
+
                     solver.push();
-                    solver.add(Eq(expr, expExpr));
+                    solver.add(eq.apply(expr, expExpr));
                     Assert.assertTrue("(= %s %s) is unsat\n".formatted(expr, expExpr), solver.check().isSat());
                     solver.pop();
                     solver.push();
-                    solver.add(Not(Eq(expr, expExpr)));
+                    solver.add(Not(eq.apply(expr, expExpr)));
                     Assert.assertTrue("(not (= %s %s)) is sat with model %s\n".formatted(expr, expExpr, solver.check().isSat() ? solver.getModel() : ""), solver.check().isUnsat());
                     solver.pop();
                 }

diff --git a/subprojects/xcfa/c2xcfa/src/test/resources/18multithread.c b/subprojects/xcfa/c2xcfa/src/test/resources/18multithread.c
@@ -686,6 +686,9 @@ extern int pthread_atfork (void (*__prepare) (void),
 
 void reach_error(){}
 
+void __VERIFIER_atomic_begin() {}
+void __VERIFIER_atomic_end() {}
+
 int x = 0;
 int ERR = 0;
 

diff --git a/subprojects/xcfa/c2xcfa/src/test/resources/21namecollision.c b/subprojects/xcfa/c2xcfa/src/test/resources/21namecollision.c
@@ -1,3 +1,4 @@
+void reach_error(){}
 int f(int x) {
     return x - 1;
 }

diff --git a/subprojects/xcfa/c2xcfa/src/test/resources/22nondet.c b/subprojects/xcfa/c2xcfa/src/test/resources/22nondet.c
@@ -1,3 +1,4 @@
+void reach_error(){}
 extern int __VERIFIER_nondet_int();
 int main() {
     int i = 0;

diff --git a/subprojects/xcfa/c2xcfa/src/test/resources/23exotic.c b/subprojects/xcfa/c2xcfa/src/test/resources/23exotic.c
@@ -1,3 +1,4 @@
+void reach_error(){}
 extern unsigned int __VERIFIER_nondet_uint();
 int main() {
     int i = 0;