Update tests, fix a bug from previous commit.

regression-tests/horn-hcc-array/Answers

@@ -119,7 +119,7 @@ Final:
  main18_36_3(S(store(store(store(store(const(4), 0, 0), 1, 1), 2, 2), 3, 3)), 0) 
 ---------------------------------------------------------------------------------
 Failed assertion:
-false :- main18_36_3(s:14, i:18), select(data(s:14), i:18) = i:18. (line:19 col:5) (property: user-assertion)
+false :- main18_36_3(s:14, i:18), select(S::data(s:14), i:18) = i:18. (line:19 col:5) (property: user-assertion)
 
 UNSAFE
 
@@ -197,7 +197,7 @@ Final:
  main8_3(newHeap(alloc(newHeap(alloc(emptyHeap, O_S(S(10)))), O_S(S(20)))), AddrRange(nthAddr(1), 2)) 
 ------------------------------------------------------------------------------------------------------
 Failed assertion:
-false :- main8_3(@h, sArr:5), f(getS(read(@h, nthAddrRange(sArr:5, 0)))) != 0. (line:8 col:3) (property: user-assertion)
+false :- main8_3(@h, sArr:5), S::f(getS(read(@h, nthAddrRange(sArr:5, 0)))) != 0. (line:8 col:3) (property: user-assertion)
 
 UNSAFE
 

regression-tests/horn-hcc-heap/Answers

@@ -62,7 +62,7 @@ Final:
  main_3(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_parent(parent(nthAddr(2), nthAddr(3))))), O_child(child(nthAddr(1))))), O_child(child(nthAddr(0))))), nthAddr(1)) 
 ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
 Failed assertion:
-false :- main_3(@h, list:14), p(getchild(read(@h, child1(getparent(read(@h, list:14)))))) != p(getchild(read(@h, child2(getparent(read(@h, list:14)))))). (line:20 col:3) (property: user-assertion)
+false :- main_3(@h, list:14), child::p(getchild(read(@h, parent::child1(getparent(read(@h, list:14)))))) != child::p(getchild(read(@h, parent::child2(getparent(read(@h, list:14)))))). (line:20 col:3) (property: user-assertion)
 
 UNSAFE
 

regression-tests/horn-hcc-pointer/Answers

@@ -25,7 +25,7 @@ Final:
  main_4(.AS0(1, .AS1(5, .AS2(6))), .AS0(4, .AS1(2, .AS2(3))), 0) 
 -----------------------------------------------------------------
 Failed assertion:
-false :- main_4(s1:9, s2:9, x1:21), a(b(s1:9)) != a(b(s1:9)) | a(b(s1:9)) != 2 | a(b(s2:9)) != 5. (line:23 col:5) (property: user-assertion)
+false :- main_4(s1:9, s2:9, x1:21), .AS1::a(.AS0::b(s1:9)) != .AS1::a(.AS0::b(s1:9)) | .AS1::a(.AS0::b(s1:9)) != 2 | .AS1::a(.AS0::b(s2:9)) != 5. (line:23 col:5) (property: user-assertion)
 
 UNSAFE
 

regression-tests/horn-hcc-struct/Answers

@@ -13,9 +13,9 @@ assign-exp-eval-order.hcc
 SAFE
 
 assign-illegal.hcc
-tricera.concurrency.ccreader.CCExceptions$TranslationException: Cannot assign struct S1: ((x/1p,int)) to struct S2: ((x/1p,int))!
-(error "Cannot assign struct S1: ((x/1p,int)) to struct S2: ((x/1p,int))!")
-Other Error: Cannot assign struct S1: ((x/1p,int)) to struct S2: ((x/1p,int))!
+tricera.concurrency.ccreader.CCExceptions$TranslationException: Cannot assign struct S1: ((S1::x/1p,int)) to struct S2: ((S2::x/1p,int))!
+(error "Cannot assign struct S1: ((S1::x/1p,int)) to struct S2: ((S2::x/1p,int))!")
+Other Error: Cannot assign struct S1: ((S1::x/1p,int)) to struct S2: ((S2::x/1p,int))!
 
 init.hcc
 Warning: entry function "main" not found

src/tricera/concurrency/CCReader.scala

@@ -644,9 +644,9 @@ class CCReader private (prog              : Program,
         s"Struct ${struct.name} was declared, but never defined, " +
           "or it has no fields.")
       val ADTFieldList : Seq[(String, HeapObj.CtorArgSort)] =
-        for(fieldInfo@FieldInfo(fieldName, fieldType, ptrDepth) <-
+        for(FieldInfo(rawFieldName, fieldType, ptrDepth) <-
               struct.fieldInfos) yield
-          (struct.getFullFieldName(fieldName),
+          (CCStruct.rawToFullFieldName(struct.name, rawFieldName),
             if (ptrDepth > 0) Heap.AddressCtor
             else { fieldType match {
               case Left(ind) => HeapObj.ADTSort(ind + 1)
@@ -724,9 +724,11 @@ class CCReader private (prog              : Program,
     objectSorts.zip(0 until structCount+structCtorsOffset).toMap
 
   for (((ctor, sels), i) <- structCtors zip structSels zipWithIndex) {
-    val fieldInfos = structInfos(i).fieldInfos
+    val curStruct = structInfos(i)
+    val fieldInfos = curStruct.fieldInfos
     val fieldsWithType = for (j <- fieldInfos.indices) yield {
-      val fullFieldName = structInfos(i).getFullFieldName(fieldInfos(j).name)
+      val fullFieldName =
+        CCStruct.rawToFullFieldName(curStruct.name, fieldInfos(j).name)
       assert(sels(j).name == fullFieldName)
       (sels(j),{
         val actualType = fieldInfos(j).typ match {
@@ -2778,18 +2780,18 @@ class CCReader private (prog              : Program,
         lhs.toTerm match {
         case fieldFun : IFunApp => // an ADT
           assignedToStruct = true
-          val (fieldNames, rootTerm) = getFieldInfo(fieldFun)
+          val (fieldSelectors, rootTerm) = getFieldInfo(fieldFun)
 
           rootTerm match {
             case Left(t) =>
               val structType = structDefs(t.sort.name)
-              val fieldAddress = structType.getFieldAddress(fieldNames)
+              val fieldAddress = structType.getFieldAddress(fieldSelectors)
               CCTerm(structType.setFieldTerm(t, rhs.toTerm, fieldAddress),
                 structType, rhs.srcInfo)
             case Right(f) =>
               val structType =
                 structDefs(f.fun.asInstanceOf[MonoSortedIFunction].resSort.name)
-              val fieldAddress = structType.getFieldAddress(fieldNames)
+              val fieldAddress = structType.getFieldAddress(fieldSelectors)
               CCTerm(structType.setFieldTerm(f, rhs.toTerm, fieldAddress),
                 structType, rhs.srcInfo)
             /*case _ => {getVarType(rootTerm.name) match {
@@ -2801,29 +2803,29 @@ class CCReader private (prog              : Program,
       }
     }
 
-    // Returns the root term and a list of names pointing to the given field.
+    // Returns the root term and a list of selectors pointing to the given field.
     // todo: this works incorrectly when root is not a pointer but the field is
     // e.g. getInt(read(h, f(someStruct)))
     private def getFieldInfo(nested : IFunApp) :
-    (List[String], Either[SortedConstantTerm, IFunApp]) = {
-      val fieldNames = List()
-      getFieldInfo(nested, fieldNames)
+    (List[IFunction], Either[SortedConstantTerm, IFunApp]) = {
+      val fieldSelectors = List()
+      getFieldInfo(nested, fieldSelectors)
     }
-    private def getFieldInfo(nested : IFunApp, fieldNames : List[String])
-    : (List[String], Either[SortedConstantTerm, IFunApp]) = {
+    private def getFieldInfo(nested : IFunApp, fieldSelectors : List[IFunction])
+    : (List[IFunction], Either[SortedConstantTerm, IFunApp]) = {
       nested.args.size match {
-        case n if n > 1 => (fieldNames, Left(getStructTerm(nested)))
+        case n if n > 1 => (fieldSelectors, Left(getStructTerm(nested)))
         case n if n == 1 =>
           nested.args.head match{
             case nestedMore : IFunApp if !(objectGetters contains nestedMore.fun) =>
-              getFieldInfo(nestedMore, nested.fun.name :: fieldNames)
+              getFieldInfo(nestedMore, nested.fun :: fieldSelectors)
             case objectGetter : IFunApp =>
-              (nested.fun.name :: fieldNames, Right(objectGetter))
+              (nested.fun :: fieldSelectors, Right(objectGetter))
             case lastLevel : IConstant =>
-              (nested.fun.name :: fieldNames,
+              (nested.fun :: fieldSelectors,
                 Left(lastLevel.c.asInstanceOf[SortedConstantTerm]))
           }
-        case _ => throw new TranslationException("Cannot get field names " +
+        case _ => throw new TranslationException("Cannot get field selectors " +
           "from given struct term " + nested)
       }
     }
@@ -3537,18 +3539,10 @@ class CCReader private (prog              : Program,
         val rawFieldName = exp.cident_
         subexpr.typ match {
           case structType : CCStruct => // todo a better way
-            val structInfo = structInfos.find(_.name == structType.shortName)
-            match {
-              case Some(info) => info
-              case None => throw new TranslationException(
-                s"Internal error: could not find struct ${structType.shortName} " +
-                s"in structInfos.")
-            }
-            val fullFieldName = structInfo.getFullFieldName(rawFieldName)
-            if(!structType.contains(fullFieldName))
+            if(!structType.contains(rawFieldName))
               throw new TranslationException(rawFieldName + " is not a member of "
                 + structType + "!")
-            val ind = structType.getFieldIndex(fullFieldName)
+            val ind = structType.getFieldIndex(rawFieldName)
             val fieldType = structType.getFieldType(ind) /*match {
               case declPtr : CCDeclarationOnlyPointer if !evaluatingLhs =>
                 getHeapPointer (declPtr)
@@ -3587,11 +3581,10 @@ class CCReader private (prog              : Program,
           case None => throw new TranslationException(
             s"Internal error: could not find struct ${structType.shortName} in structInfos.")
         }
-        val fullFieldName = structInfo.getFullFieldName(rawFieldName)
-        if(!structType.contains(fullFieldName))
+        if(!structType.contains(rawFieldName))
           throw new TranslationException(rawFieldName + " is not a member of "
             + structType + "!")
-        val ind = structType.getFieldIndex(fullFieldName)
+        val ind = structType.getFieldIndex(rawFieldName)
         val fieldType = structType.getFieldType(ind)
         val sel = structType.getADTSelector(ind)
         pushVal(CCTerm(sel(term.toTerm), fieldType, srcInfo))

src/tricera/concurrency/ccreader/CCType.scala

@@ -30,18 +30,15 @@
 package tricera.concurrency.ccreader
 
 import ap.basetypes.IdealInt
-import ap.parser.{IFormula, IIntLit, ITerm}
+import ap.parser.{IFormula, IFunction, IIntLit, ITerm}
 import ap.theories.Heap
 import tricera.concurrency.CCReader._
 import ap.parser.IExpression.{Sort, _}
 import ap.theories.bitvectors.ModuloArithmetic._
 import ap.types.{MonoSortedIFunction, SortedConstantTerm}
 import CCExceptions._
 
-import scala.collection.mutable.{
-  Stack,
-  HashMap => MHashMap
-}
+import scala.collection.mutable.{Stack, HashMap => MHashMap}
 
 abstract sealed class CCType {
   def shortName : String
@@ -274,10 +271,7 @@ case class FieldInfo(name       : String,
                      typ        : Either[Integer, CCType],
                      ptrDepth   : Integer)
 
-case class StructInfo(name : String, fieldInfos : Seq[FieldInfo]) {
-  def getFullFieldName(rawFieldName : String) : String =
-    s"$name::$rawFieldName"
-}
+case class StructInfo(name : String, fieldInfos : Seq[FieldInfo])
 
 /**
  * A struct field with a struct type
@@ -289,15 +283,23 @@ case class CCStructField(structName : String,
   def shortName = "field:" + structName
 }
 
+object CCStruct{
+  def rawToFullFieldName(structName : String, fieldName : String) =
+    s"$structName::$fieldName"
+}
 case class CCStruct(ctor : MonoSortedIFunction,
                     sels : IndexedSeq[(MonoSortedIFunction, CCType)])
   extends CCType {
+  import CCStruct._
   override def toString: String =
     "struct " + ctor.name + ": (" + sels.mkString + ")"
   def shortName = ctor.name
-  def getFieldIndex(name : String) = sels.indexWhere(_._1.name == name)
-  def getFieldAddress(nestedName : List[String]) : List[Int] =
-    nestedName match {
+  def getFieldIndex(rawFieldName : String) = sels.indexWhere(
+    _._1.name == rawToFullFieldName(shortName, rawFieldName))
+  def getFieldIndex(fieldSelector : IFunction) =
+    sels.indexWhere(_._1 == fieldSelector)
+  def getFieldAddress(nestedSelectors : List[IFunction]) : List[Int] =
+    nestedSelectors match {
       case hd :: Nil => getFieldIndex(hd) :: Nil
       case hd :: tl => {
         val ind = getFieldIndex(hd)
@@ -324,7 +326,7 @@ case class CCStruct(ctor : MonoSortedIFunction,
             "empty field index!")
     }
 
-  def contains(fieldName : String) = getFieldIndex(fieldName) != -1
+  def contains(rawFieldName : String) = getFieldIndex(rawFieldName) != -1
   def getFieldTerm(t : ITerm, fieldAddress: List[Int]): ITerm = {
     val hd :: tl = fieldAddress
     val sel      = getADTSelector(hd)