Disable heap-stack pointer combinations.

regression-tests/horn-contracts/Answers

@@ -118,6 +118,4 @@ false :- main12_3_1(x:12), x:12 != 0. (line:14 col:3) (property: user-assertion)
 UNSAFE
 
 stackptr.hcc
-tricera.concurrency.ccreader.CCExceptions$TranslationException: Function contracts are currently not supported together with stack pointers (10:5)
-(error "Function contracts are currently not supported together with stack pointers (10:5)")
-Other Error: Function contracts are currently not supported together with stack pointers (10:5)
+UNKNOWN (Unsupported C fragment. Function contracts are currently not supported together with stack pointers (10:5))

regression-tests/horn-hcc-heap/Answers

@@ -165,6 +165,9 @@ UNSAFE
 stackptr-to-heapptr.c
 SAFE
 
+stackptr-to-heapptr-double.c
+UNKNOWN (Unsupported C fragment. 6:8 Only limited support for stack pointers)
+
 free-1-unsafe.c
 
 ------------------------------------------------------------------------
@@ -245,4 +248,4 @@ struct-ptrfield-1.c
 SAFE
 
 stack-ptr-bug-1.c
-SAFE
+UNKNOWN (Unsupported C fragment. 11:10 Stack pointers in combination with heap pointers)

regression-tests/horn-hcc-heap/runtests

@@ -2,7 +2,7 @@
 
 LAZABS=../../tri
 
-TESTS="list-001.c list-001-fail.c list-002-fail.c mutually-referential-structs.c mutually-referential-structs-fail.c mutually-referential-structs-unsafe.c simple-struct.c simple-struct-2.c simple-struct-fail.c swap-1.c swap-1-fail.c swap-2.c swap-2-fail.c swap-3.c simple-arith.c typecastUnsafe-001.c typecastSafe-001.c illegal-access-001.c illegal-access-002.c postop.c postop-struct.c preop.c preop-struct.c opassign.c opassign-struct.c unsafe-access-001.c stackptr-to-heapptr.c free-1-unsafe.c free-2-nondet-unsafe.c free-3-safe.c free-4-unsafe.c struct-ptrfield-1.c"
+TESTS="list-001.c list-001-fail.c list-002-fail.c mutually-referential-structs.c mutually-referential-structs-fail.c mutually-referential-structs-unsafe.c simple-struct.c simple-struct-2.c simple-struct-fail.c swap-1.c swap-1-fail.c swap-2.c swap-2-fail.c swap-3.c simple-arith.c typecastUnsafe-001.c typecastSafe-001.c illegal-access-001.c illegal-access-002.c postop.c postop-struct.c preop.c preop-struct.c opassign.c opassign-struct.c unsafe-access-001.c stackptr-to-heapptr.c stackptr-to-heapptr-double.c free-1-unsafe.c free-2-nondet-unsafe.c free-3-safe.c free-4-unsafe.c struct-ptrfield-1.c"
 
 for name in $TESTS; do
     echo

regression-tests/horn-hcc-heap/stackptr-to-heapptr-double.c

@@ -0,0 +1,9 @@
+#include <stdlib.h>
+
+void main () {
+  int *x1, *x2;
+  int y = 42;
+  x1 = &y;
+  x2 = &y;
+  assert(x1 == x2);
+}

src/tricera/Main.scala

@@ -366,6 +366,10 @@ class Main (args: Array[String]) {
         case e : UnsupportedCastException =>
           return ExecutionSummary(Unknown(e.getMessage), Map(),
                                   modelledHeap, 0, preprocessTimer.s)
+        case e : UnsupportedCFragmentException =>
+          return ExecutionSummary(
+            Unknown("Unsupported C fragment. " + e.getMessage), Map(),
+            modelledHeap, 0, preprocessTimer.s)
         case e : Throwable => throw e
       }
 

src/tricera/concurrency/CCReader.scala

@@ -1608,8 +1608,8 @@ private def collectVarDecls(dec                    : Dec,
                     "initialization is not yet supported.")
               }
             }
-            case Some(_) => throw new TranslationException("Unsupported" +
-              "initializer expression.")
+            case Some(_) => throw new UnsupportedCFragmentException(
+              getLineStringShort(srcInfo) + " Unsupported initializer expression.")
             case None =>
               varDec.typ match {
                 case typ : CCHeapArrayPointer =>
@@ -2655,9 +2655,10 @@ private def collectVarDecls(dec                    : Dec,
       else
         values(ind)
 
-    private def getPointedTerm (ptrType : CCStackPointer) =
+    private def getPointedTerm (ptrType : CCStackPointer) : CCTerm =
       ptrType.fieldAddress match {
-        case Nil => getValue(ptrType.targetInd, false)
+        case Nil =>
+          getValue(ptrType.targetInd, false).asInstanceOf[CCTerm]
         case _ =>
           val structVal = getValue(ptrType.targetInd, false)
           val structType = structVal.typ.asInstanceOf[CCStruct]
@@ -3002,9 +3003,13 @@ private def collectVarDecls(dec                    : Dec,
                      evalCtx.enclosingFunctionName)
           } else {
             val lhsName = asLValue(exp.exp_1)
-            val actualRhsVal = rhsVal.toTerm match {
-              case lit : IIntLit =>
-                if (lit.value.intValue != 0) {
+            val actualRhsVal = rhsVal match {
+              case CCTerm(_, stackPtr@CCStackPointer(_,_,_), srcInfo) =>
+                throw new UnsupportedCFragmentException(
+                  getLineStringShort(srcInfo) +
+                  " Only limited support for stack pointers")
+              case CCTerm(IIntLit(value), _, _) =>
+                if (value.intValue != 0) {
                   throw new TranslationException("Pointer arithmetic is not " +
                     "allowed, and the only assignable integer value for " +
                     "pointers is 0 (NULL)")
@@ -3026,8 +3031,8 @@ private def collectVarDecls(dec                    : Dec,
                           arrayPtr2.arrayLocation == ArrayLocation.Heap) // -> alloca
                         updateVarType(lhsName, arrayPtr1,
                                       evalCtx.enclosingFunctionName) // todo: replace with a static analysis? we should detect arrays on stack beforehand maybe?
-                      else throw new TranslationException(getLineString(exp) +
-                        "Unsupported operation: pointer " + lhsName +
+                      else throw new UnsupportedCFragmentException(getLineString(exp) +
+                        "Pointer " + lhsName +
                         " points to elements of multiple arrays (or array types)." +
                         "Try initialising the array directly.")
                     }
@@ -3288,12 +3293,15 @@ private def collectVarDecls(dec                    : Dec,
                     // alternatively one could rewrite this using a temporary variable
                     // and create a stack pointer to it (but this needs to be done during preprocessing,
                     // otherwise when we evaluate this we would be pushing two terms instead of one)
-                    val newTerm = heapAlloc(popVal.asInstanceOf[CCTerm])
-                    assert(c.args.size == 1)
-                    val readObj = c.args.head
-                    val resSort = c.fun.asInstanceOf[MonoSortedIFunction].resSort
-                    addGuard(heap.heapADTs.hasCtor(readObj, sortCtorIdMap(resSort)))
-                    pushVal(newTerm)
+//                    val newTerm = heapAlloc(popVal.asInstanceOf[CCTerm])
+//                    assert(c.args.size == 1)
+//                    val readObj = c.args.head
+//                    val resSort = c.fun.asInstanceOf[MonoSortedIFunction].resSort
+//                    addGuard(heap.heapADTs.hasCtor(readObj, sortCtorIdMap(resSort)))
+//                    pushVal(newTerm)
+                  throw new UnsupportedCFragmentException(
+                    getLineStringShort(srcInfo) +
+                    " Stack pointers in combination with heap pointers")
                 }
               case f : IFunApp if objectGetters contains f.fun => // a heap read (might also be from a heap array)
                 val readFunApp = f.args.head.asInstanceOf[IFunApp] // sth like read(h, ...)
@@ -3323,7 +3331,7 @@ private def collectVarDecls(dec                    : Dec,
                   //val newTerm = heapAlloc(popVal.asInstanceOf[CCTerm])
                   //maybeOutputClause(Some(getSourceInfo(exp)))
                   //newTerm
-                  throw new TranslationException(
+                  throw new UnsupportedCFragmentException(
                     "Function contracts are currently not supported together " +
                     s"with stack pointers (${exp.line_num}:${exp.col_num})")
                 } else {
@@ -3450,14 +3458,14 @@ private def collectVarDecls(dec                    : Dec,
                 case e if exp.exp_2.isInstanceOf[Ebytestype] =>
                   (getType(exp.exp_2.asInstanceOf[Ebytestype]), eval(e))
                 case _ =>
-                  throw new TranslationException(
+                  throw new UnsupportedCFragmentException(
                     "Unsupported alloc expression: " + (printer print exp))
               }
             //case exp : Evar => // allocation in bytes
             case e : Econst => // allocation in bytes
               (CCInt, eval(e)) // todo: add support for char?
 
-            case _ => throw new TranslationException(
+            case _ => throw new UnsupportedCFragmentException(
               "Unsupported alloc expression: " + (printer print exp))
           }
 
@@ -3556,12 +3564,12 @@ private def collectVarDecls(dec                    : Dec,
                 case e if exp.exp_2.isInstanceOf[Ebytestype] =>
                   (getType(exp.exp_2.asInstanceOf[Ebytestype]), eval(e))
                 case _ =>
-                  throw new TranslationException(
+                  throw new UnsupportedCFragmentException(
                     "Unsupported alloc expression: " + (printer print exp))
               }
             //case exp : Evar => // allocation in bytes
 
-            case _ => throw new TranslationException(
+            case _ => throw new UnsupportedCFragmentException(
               "Unsupported alloc expression: " + (printer print exp))
           }
 

src/tricera/concurrency/ccreader/CCExceptions.scala

@@ -33,6 +33,7 @@ object CCExceptions {
   class ParseException(msg : String) extends Exception(msg)
   class TranslationException(msg : String) extends Exception(msg)
   class UnsupportedCastException(msg : String) extends Exception(msg)
+  class UnsupportedCFragmentException(msg : String) extends Exception(msg)
   object NeedsTimeException extends Exception
   object NeedsHeapModelException extends Exception
 }