Add support for heap pointers to uninterpreted predicates

uuverifiers · Apr 10, 2024 · 135956d · 135956d
1 parent da0ef67
commit 135956d
Show file tree

Hide file tree

Showing 3 changed files with 34 additions and 32 deletions.
diff --git a/regression-tests/uninterpreted-predicates/Answers b/regression-tests/uninterpreted-predicates/Answers
@@ -33,3 +33,11 @@ UNSAFE
 
 unint-pred-simple-true.c
 SAFE
+
+unint-pred-stack-ptr-unsupported.c
+tricera.concurrency.ccreader.CCExceptions$TranslationException: 5:3 Unsupported operation: stack pointer argument to uninterpreted predicate.
+(error "5:3 Unsupported operation: stack pointer argument to uninterpreted predicate.")
+Other Error: 5:3 Unsupported operation: stack pointer argument to uninterpreted predicate.
+
+unint-pred-simple-ptr-true.c
+SAFE
diff --git a/regression-tests/uninterpreted-predicates/runtests b/regression-tests/uninterpreted-predicates/runtests
@@ -3,7 +3,8 @@
 LAZABS=../../tri
 
 TESTS="pred-hint.c pred-hint-loop.c \
-       unint-pred-simple-false.c unint-pred-simple-true.c"
+       unint-pred-simple-false.c unint-pred-simple-true.c \
+       unint-pred-stack-ptr-unsupported.c unint-pred-simple-ptr-true.c"
 
 for name in $TESTS; do
     echo

diff --git a/src/tricera/concurrency/CCReader.scala b/src/tricera/concurrency/CCReader.scala
@@ -1418,49 +1418,38 @@ class CCReader private (prog              : Program,
     for (ind <- decList.indices) yield {
       decList(ind) match {
         case t : OnlyType => {
-          if (t.listdeclaration_specifier_.exists(spec => !spec
-            .isInstanceOf[Type]))
-            throw new TranslationException("Only type specifiers" +
-                                           "are allowed inside predicate" +
-                                           "declarations.")
+          if (t.listdeclaration_specifier_.exists(
+            spec => !spec.isInstanceOf[Type]))
+            throw new TranslationException(
+              "Only type specifiers are allowed inside predicate declarations.")
           val argType = getType(
             t.listdeclaration_specifier_.map(_.asInstanceOf[Type]
                                               .type_specifier_).toIterator)
           val argName = declName + "_" + ind
           (argType, argName)
         }
         case argDec : TypeAndParam => {
-          val name       = getName(argDec.declarator_)
-          val typ        = getType(argDec.listdeclaration_specifier_)
+          val name = getName(argDec.declarator_)
+          val typ  = getType(argDec.listdeclaration_specifier_)
           val actualType = argDec.declarator_ match {
-            case p : BeginPointer =>
-              //createHeapPointer(p, typ)
-              throw new TranslationException("Pointers inside " +
-                                             "predicate declarations are " +
-                                              "not supported.")
-            case np : NoPointer   =>
-              np.direct_declarator_ match {
-                case _ : Incomplete =>
-                  //CCHeapArrayPointer(heap, typ, HeapArray)
-                  throw new TranslationException("Arrays inside " +
-                                                 "predicate declarations " +
-                                                 "are not supported.")
-                case _ => typ
-              }
+            case p : BeginPointer => createHeapPointer(p, typ)
+            case np : NoPointer   => np.direct_declarator_ match {
+              case _ : Incomplete =>
+                //CCHeapArrayPointer(heap, typ, HeapArray)
+                throw new TranslationException(
+                  "Arrays inside predicate declarations are not supported.")
+              case _ => typ
+            }
             case _ => typ
           }
           (actualType, name)
         }
         case argDec : TypeHintAndParam => {
-          val name       = getName(argDec.declarator_)
-          val typ        = getType(argDec.listdeclaration_specifier_)
+          val name = getName(argDec.declarator_)
+          val typ  = getType(argDec.listdeclaration_specifier_)
           val actualType = argDec.declarator_ match {
-            case p : BeginPointer =>
-              //createHeapPointer(p, typ)
-              throw new TranslationException("Pointers inside" +
-                                             "predicate declarations are " +
-                                              "not supported.")
-            case _                => typ
+            case p : BeginPointer => createHeapPointer(p, typ)
+            case _ => typ
           }
           processHints(argDec.listannotation_) // todo: does this work??
           (actualType, name)
@@ -3399,9 +3388,13 @@ private def collectVarDecls(dec                    : Dec,
               case a : Efunkpar
                 if uninterpPredDecls contains(printer print a.exp_) =>
                 val args = a.listexp_.map(exp => atomicEval(exp, evalCtx))
-                                     .map(_.toTerm)
+                if(args.exists(a => a.typ.isInstanceOf[CCStackPointer])) {
+                  throw new TranslationException(
+                    getLineStringShort(srcInfo) + " Unsupported operation: " +
+                    "stack pointer argument to uninterpreted predicate.")
+                }
                 val pred = uninterpPredDecls(printer print a.exp_)
-                atom(pred, args)
+                atom(pred, args.map(_.toTerm))
               case interpPred : Efunkpar
                 if interpPredDefs contains(printer print interpPred.exp_) =>
                 val args    = interpPred.listexp_.map(