Memsafety and memcleanup

.github/actions/benchexec-report/action.yml

@@ -40,11 +40,11 @@ runs:
               all=0
               for txt in *.txt
               do
-                new_correct=$(tail -n9 $txt | grep '  correct:' | awk ' { print $2 } ')
+                new_correct=$(tail -n9 $txt | grep '  correct:' | awk ' { print $2 } ' || echo 0)
                 correct=$((correct + new_correct))
-                new_incorrect=$(tail -n9 $txt | grep '  incorrect:' | awk ' { print $2 } ')
+                new_incorrect=$(tail -n9 $txt | grep '  incorrect:' | awk ' { print $2 } ' || echo 0)
                 incorrect=$((incorrect + new_incorrect))
-                new_all=$(tail -n9 $txt | grep 'Statistics:' | awk ' { print $2 } ')
+                new_all=$(tail -n9 $txt | grep 'Statistics:' | awk ' { print $2 } ' || echo 0)
                 all=$((all + new_all))
                 echo "Found $new_correct correct and $new_incorrect incorrect results out of $new_all tasks in $txt"
               done

.github/actions/benchexec-test/action.yml

@@ -64,8 +64,8 @@ runs:
         for task in ${tasks[@]}
         do
           echo "Starting benchmark on rundefinition '${{ inputs.rundef }}', task set '$task'"
-          echo "timeout $timeout benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true"
-          timeout $timeout benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true
+          echo "timeout --kill-after 15 $timeout benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true"
+          timeout --kill-after 15 $timeout benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true
         done
     - name: Upload results
       uses: actions/upload-artifact@b4b15b8c7c6ac21ea08fcf65892d2ee8f75cf882 # v3.1.2

build.gradle.kts

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

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

@@ -50,6 +50,7 @@
 import hu.bme.mit.theta.frontend.transformation.model.statements.*;
 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.complex.compound.CArray;
 import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleType;
 import hu.bme.mit.theta.frontend.transformation.model.types.simple.Struct;
 import java.util.*;
@@ -72,13 +73,15 @@ public class FunctionVisitor extends CBaseVisitor<CStatement> {
     private final TypedefVisitor typedefVisitor;
     private final Logger uniqueWarningLogger;
 
-    private ParserRuleContext currentStatementContext = null;
+    private final LinkedList<Tuple2<ParserRuleContext, Optional<CCompound>>>
+            currentStatementContext = new LinkedList<>();
 
     public void clear() {
         variables.clear();
         atomicVariables.clear();
         flatVariables.clear();
         functions.clear();
+        currentStatementContext.clear();
     }
 
     private final Deque<Tuple2<String, Map<String, VarDecl<?>>>> variables;
@@ -184,8 +187,11 @@ public CStatement visitCompilationUnit(CParser.CompilationUnitContext ctx) {
     }
 
     public void recordMetadata(ParserRuleContext ctx, CStatement statement) {
-        if (currentStatementContext != null) {
-            ctx = currentStatementContext; // this will overwrite the current ASt element's ctx
+        if (!currentStatementContext.isEmpty()) {
+            ctx =
+                    currentStatementContext
+                            .peek()
+                            .get1(); // this will overwrite the current ASt element's ctx
             // with the statement's ctx
         }
         Token start = ctx.getStart();
@@ -300,10 +306,9 @@ public CStatement visitBlockItemList(CParser.BlockItemListContext ctx) {
         if (ctx.parent.parent.parent.parent instanceof CParser.BlockItemListContext)
             variables.push(Tuple2.of("anonymous" + anonCnt++, new LinkedHashMap<>()));
         for (CParser.BlockItemContext blockItemContext : ctx.blockItem()) {
-            final var save = currentStatementContext;
-            currentStatementContext = blockItemContext;
+            currentStatementContext.push(Tuple2.of(blockItemContext, Optional.of(compound)));
             compound.getcStatementList().add(blockItemContext.accept(this));
-            currentStatementContext = save;
+            currentStatementContext.pop();
         }
         if (ctx.parent.parent.parent.parent instanceof CParser.BlockItemListContext)
             variables.pop();
@@ -482,10 +487,9 @@ public CStatement visitReturnStatement(CParser.ReturnStatementContext ctx) {
 
     @Override
     public CStatement visitStatement(CParser.StatementContext ctx) {
-        final var save = currentStatementContext;
-        currentStatementContext = ctx;
+        currentStatementContext.push(Tuple2.of(ctx, Optional.empty()));
         final var ret = ctx.children.get(0).accept(this);
-        currentStatementContext = save;
+        currentStatementContext.pop();
         return ret;
     }
 
@@ -501,8 +505,37 @@ public CStatement visitBodyDeclaration(CParser.BodyDeclarationContext ctx) {
         compound.setPreStatements(preCompound);
         compound.setPostStatements(postCompound);
         for (CDeclaration declaration : declarations) {
+            createVars(declaration);
+            if (declaration.getActualType()
+                    instanceof CArray cArray) { // we transform it into a malloc
+                final var malloc =
+                        new CCall("malloc", List.of(cArray.getArrayDimension()), parseContext);
+                preCompound.getcStatementList().add(malloc);
+                final var free =
+                        new CCall(
+                                "free",
+                                List.of(new CExpr(malloc.getRet().getRef(), parseContext)),
+                                parseContext);
+                preCompound.getcStatementList().add(malloc);
+                CAssignment cAssignment =
+                        new CAssignment(
+                                declaration.getVarDecls().get(0).getRef(),
+                                new CExpr(malloc.getRet().getRef(), parseContext),
+                                "=",
+                                parseContext);
+                recordMetadata(ctx, cAssignment);
+                compound.getcStatementList().add(cAssignment);
+                if (!currentStatementContext.isEmpty()) {
+                    final var scope = currentStatementContext.peek().get2();
+                    if (scope.isPresent() && scope.get().getPostStatements() instanceof CCompound) {
+                        if (scope.get().getPostStatements() == null) {
+                            scope.get().setPostStatements(new CCompound(parseContext));
+                        }
+                        ((CCompound) scope.get().getPostStatements()).getcStatementList().add(free);
+                    }
+                }
+            }
             if (declaration.getInitExpr() != null) {
-                createVars(declaration);
                 if (declaration.getType() instanceof Struct) {
                     checkState(
                             declaration.getInitExpr() instanceof CInitializerList,
@@ -575,7 +608,6 @@ public CStatement visitBodyDeclaration(CParser.BodyDeclarationContext ctx) {
                     }
                 }
             } else {
-                createVars(declaration);
                 // if there is no initializer, then we'll add an assumption regarding min and max
                 // values
                 if (declaration.getType() instanceof Struct) {

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

@@ -13,20 +13,18 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
-
 package hu.bme.mit.theta.frontend.transformation.model.declaration;
 
+import static com.google.common.base.Preconditions.checkNotNull;
+
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.frontend.transformation.model.statements.CStatement;
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType;
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CArray;
 import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleType;
-
 import java.util.ArrayList;
 import java.util.List;
 
-import static com.google.common.base.Preconditions.checkNotNull;
-
 public class CDeclaration {
 
     private CSimpleType type;
@@ -87,13 +85,20 @@ public CComplexType getActualType() {
         for (CStatement arrayDimension : arrayDimensions) {
             CSimpleType simpleType = type.copyOf();
             simpleType.incrementPointer();
-            actualType = new CArray(simpleType, actualType, actualType.getParseContext()); // some day change this back to arrays, when simple & complex types are better synchronized...
+            actualType =
+                    new CArray(
+                            simpleType,
+                            actualType,
+                            actualType.getParseContext(),
+                            arrayDimension); // some day change this back to arrays, when simple &
+            // complex types are better synchronized...
         }
-//        for (int i = 0; i < derefCounter; i++) {
-//            CSimpleType simpleType = type.copyOf();
-//            simpleType.incrementPointer();
-//            actualType = new CPointer(simpleType, actualType, actualType.getParseContext());
-//        }
+        //        for (int i = 0; i < derefCounter; i++) {
+        //            CSimpleType simpleType = type.copyOf();
+        //            simpleType.incrementPointer();
+        //            actualType = new CPointer(simpleType, actualType,
+        // actualType.getParseContext());
+        //        }
 
         return actualType;
     }

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

@@ -13,10 +13,10 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
-
 package hu.bme.mit.theta.frontend.transformation.model.types.complex.compound;
 
 import hu.bme.mit.theta.frontend.ParseContext;
+import hu.bme.mit.theta.frontend.transformation.model.statements.CStatement;
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType;
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.CInteger;
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.clong.CUnsignedLong;
@@ -25,10 +25,22 @@
 public class CArray extends CInteger {
 
     private final CComplexType embeddedType;
+    private final CStatement arrayDimension; // if null, infinite
+
+    public CArray(
+            CSimpleType origin,
+            CComplexType embeddedType,
+            ParseContext parseContext,
+            CStatement arrayDimension) {
+        super(origin, parseContext);
+        this.embeddedType = embeddedType;
+        this.arrayDimension = arrayDimension;
+    }
 
     public CArray(CSimpleType origin, CComplexType embeddedType, ParseContext parseContext) {
         super(origin, parseContext);
         this.embeddedType = embeddedType;
+        this.arrayDimension = null;
     }
 
     public CComplexType getEmbeddedType() {
@@ -39,7 +51,6 @@ public <T, R> R accept(CComplexTypeVisitor<T, R> visitor, T param) {
         return visitor.visit(this, param);
     }
 
-
     @Override
     public CInteger getSignedVersion() {
         return this;
@@ -50,10 +61,12 @@ public CInteger getUnsignedVersion() {
         return this;
     }
 
-
     @Override
     public String getTypeName() {
         return new CUnsignedLong(null, parseContext).getTypeName();
     }
 
+    public CStatement getArrayDimension() {
+        return arrayDimension;
+    }
 }

subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt

@@ -21,25 +21,35 @@ import com.google.common.base.Preconditions
 import com.google.common.base.Preconditions.checkState
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.core.decl.Decls
+import hu.bme.mit.theta.core.decl.Decls.Var
 import hu.bme.mit.theta.core.decl.VarDecl
 import hu.bme.mit.theta.core.stmt.AssignStmt
 import hu.bme.mit.theta.core.stmt.MemoryAssignStmt
 import hu.bme.mit.theta.core.stmt.Stmts
 import hu.bme.mit.theta.core.stmt.Stmts.Assume
 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.abstracttype.AddExpr
+import hu.bme.mit.theta.core.type.abstracttype.DivExpr
+import hu.bme.mit.theta.core.type.abstracttype.MulExpr
+import hu.bme.mit.theta.core.type.abstracttype.SubExpr
 import hu.bme.mit.theta.core.type.anytype.Dereference
 import hu.bme.mit.theta.core.type.anytype.Exprs.Dereference
 import hu.bme.mit.theta.core.type.anytype.RefExpr
+import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr
+import hu.bme.mit.theta.core.type.arraytype.ArrayType
 import hu.bme.mit.theta.core.type.booltype.BoolExprs
 import hu.bme.mit.theta.core.type.booltype.BoolExprs.*
 import hu.bme.mit.theta.core.type.booltype.BoolType
 import hu.bme.mit.theta.core.type.bvtype.BvLitExpr
+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.utils.BvUtils
 import hu.bme.mit.theta.core.utils.ExprUtils
 import hu.bme.mit.theta.core.utils.TypeUtils.cast
 import hu.bme.mit.theta.frontend.ParseContext
+import hu.bme.mit.theta.frontend.UnsupportedFrontendElementException
 import hu.bme.mit.theta.frontend.transformation.grammar.expression.UnsupportedInitializer
 import hu.bme.mit.theta.frontend.transformation.model.statements.*
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType
@@ -48,10 +58,12 @@ import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CAr
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CPointer
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CStruct
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.CInteger
+import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.Fitsall
 import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFactory
 import hu.bme.mit.theta.xcfa.AssignStmtLabel
 import hu.bme.mit.theta.xcfa.model.*
 import hu.bme.mit.theta.xcfa.passes.CPasses
+import hu.bme.mit.theta.xcfa.passes.MemsafetyPass
 import java.math.BigInteger
 import java.util.stream.Collectors
 
@@ -95,6 +107,30 @@ class FrontendXcfaBuilder(
   fun buildXcfa(cProgram: CProgram): XcfaBuilder {
     val builder = XcfaBuilder(cProgram.id ?: "")
     val initStmtList: MutableList<XcfaLabel> = ArrayList()
+    if (MemsafetyPass.NEED_CHECK) {
+      val fitsall = Fitsall.getFitsall(parseContext)
+      val ptrType = CPointer(null, null, parseContext)
+      val ptrSize =
+        XcfaGlobalVar(
+          Var("__theta_ptr_size", ArrayType.of(ptrType.smtType, fitsall.smtType)),
+          ArrayLitExpr.of(
+            listOf(),
+            fitsall.nullValue as Expr<Type>,
+            ArrayType.of(ptrType.smtType as Type, fitsall.smtType as Type),
+          ),
+        )
+      builder.addVar(ptrSize)
+      initStmtList.add(
+        AssignStmtLabel(
+          ptrSize.wrappedVar,
+          ArrayLitExpr.of(
+            listOf(),
+            fitsall.nullValue as Expr<Type>,
+            ArrayType.of(ptrType.smtType as Type, fitsall.smtType as Type),
+          ),
+        )
+      )
+    }
     for (globalDeclaration in cProgram.globalDeclarations) {
       val type = CComplexType.getType(globalDeclaration.get2().ref, parseContext)
       if (type is CVoid) {
@@ -122,6 +158,14 @@ class FrontendXcfaBuilder(
             )
           )
         )
+        if (MemsafetyPass.NEED_CHECK) {
+          val bounds = globalDeclaration.get1().arrayDimensions[0].expression
+          checkState(
+            bounds is IntLitExpr || bounds is BvLitExpr,
+            "Only IntLit and BvLit expression expected here.",
+          )
+          initStmtList.add(builder.allocate(parseContext, globalDeclaration.get2().ref, bounds))
+        }
       } else {
         if (
           globalDeclaration.get1().initExpr != null &&
@@ -249,9 +293,7 @@ class FrontendXcfaBuilder(
         builder.setAtomic(flatVariable)
       }
       val type = CComplexType.getType(flatVariable.ref, parseContext)
-      if (
-        (type is CArray || type is CStruct) && builder.getParams().none { it.first == flatVariable }
-      ) {
+      if ((type is CStruct) && builder.getParams().none { it.first == flatVariable }) {
         initStmtList.add(
           StmtLabel(
             Stmts.Assign(
@@ -321,6 +363,13 @@ class FrontendXcfaBuilder(
         }
 
         is RefExpr<*> -> {
+          if (
+            (CComplexType.getType(lValue, parseContext) is CPointer ||
+              CComplexType.getType(lValue, parseContext) is CArray ||
+              CComplexType.getType(lValue, parseContext) is CStruct) && rExpression.hasArithmetic()
+          ) {
+            throw UnsupportedFrontendElementException("Pointer arithmetic not supported.")
+          }
           AssignStmtLabel(
             lValue,
             cast(CComplexType.getType(lValue, parseContext).castTo(rExpression), lValue.type),
@@ -1060,3 +1109,12 @@ class FrontendXcfaBuilder(
     }
   }
 }
+
+private fun Expr<*>.hasArithmetic(): Boolean =
+  when (this) {
+    is AddExpr -> true
+    is SubExpr -> true
+    is DivExpr -> true
+    is MulExpr -> true
+    else -> ops.any { it.hasArithmetic() }
+  }