diff --git a/regression-tests/horn-contracts/Answers b/regression-tests/horn-contracts/Answers index 29e5489..19bbbc1 100644 --- a/regression-tests/horn-contracts/Answers +++ b/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)) diff --git a/regression-tests/horn-hcc-heap/Answers b/regression-tests/horn-hcc-heap/Answers index f99019b..b843a0f 100644 --- a/regression-tests/horn-hcc-heap/Answers +++ b/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) diff --git a/regression-tests/horn-hcc-heap/runtests b/regression-tests/horn-hcc-heap/runtests index 798a069..7972341 100755 --- a/regression-tests/horn-hcc-heap/runtests +++ b/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 diff --git a/regression-tests/horn-hcc-heap/stackptr-to-heapptr-double.c b/regression-tests/horn-hcc-heap/stackptr-to-heapptr-double.c new file mode 100644 index 0000000..957db26 --- /dev/null +++ b/regression-tests/horn-hcc-heap/stackptr-to-heapptr-double.c @@ -0,0 +1,9 @@ +#include + +void main () { + int *x1, *x2; + int y = 42; + x1 = &y; + x2 = &y; + assert(x1 == x2); +} \ No newline at end of file diff --git a/src/tricera/Main.scala b/src/tricera/Main.scala index 7fce576..d259f4f 100644 --- a/src/tricera/Main.scala +++ b/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 } diff --git a/src/tricera/concurrency/CCReader.scala b/src/tricera/concurrency/CCReader.scala index e122194..ce4574e 100644 --- a/src/tricera/concurrency/CCReader.scala +++ b/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)) } diff --git a/src/tricera/concurrency/ccreader/CCExceptions.scala b/src/tricera/concurrency/ccreader/CCExceptions.scala index 4534550..26343f3 100644 --- a/src/tricera/concurrency/ccreader/CCExceptions.scala +++ b/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 }