diff --git a/src/tricera/Main.scala b/src/tricera/Main.scala index 85bd6e3..e366507 100644 --- a/src/tricera/Main.scala +++ b/src/tricera/Main.scala @@ -167,16 +167,18 @@ object Main { // At most one sub-property is expected to not hold, if any. val updatedSubProps = verdictOption match { case Some(false) => p.subproperty match { - case Some("valid-free") => + case Some("valid-free") => initialSubProps.updated(properties.MemValidFree, false) - case Some("valid-deref") => + case Some("valid-deref") => initialSubProps.updated(properties.MemValidDeref, false) case Some("valid-memtrack") => initialSubProps.updated(properties.MemValidTrack, false) - case Some(prop) => throw new Exception( + case Some(prop) => throw new Exception( s"Unknown sub-property $prop for the memsafety category.") - case None => throw new Exception( - "The failing sub-property must be specified for memsafety.") + case None => throw new Exception( + "For memsafety where the expected verdict is 'false', the " + + "failing sub-property must be specified. Alternatively, the " + + "expected verdict can be removed.") } case _ => initialSubProps } diff --git a/src/tricera/concurrency/CCReader.scala b/src/tricera/concurrency/CCReader.scala index 4d21719..7e204ac 100644 --- a/src/tricera/concurrency/CCReader.scala +++ b/src/tricera/concurrency/CCReader.scala @@ -639,14 +639,14 @@ class CCReader private (prog : Program, val ObjSort = HeapObj.ADTSort(0) val structCtorSignatures : List[(String, HeapObj.CtorSignature)] = - (for (i <- structInfos.indices) yield { - if(structInfos(i).fieldInfos isEmpty) warn( - "Struct " + structInfos(i).name + " was declared, but never defined, " + + (for ((struct, i) <- structInfos zipWithIndex) yield { + if(struct.fieldInfos isEmpty) warn( + s"Struct ${struct.name} was declared, but never defined, " + "or it has no fields.") val ADTFieldList : Seq[(String, HeapObj.CtorArgSort)] = - for(FieldInfo(fieldName, fieldType, ptrDepth) <- - structInfos(i).fieldInfos) yield - (fieldName, + for(fieldInfo@FieldInfo(fieldName, fieldType, ptrDepth) <- + struct.fieldInfos) yield + (struct.getFullFieldName(fieldName), if (ptrDepth > 0) Heap.AddressCtor else { fieldType match { case Left(ind) => HeapObj.ADTSort(ind + 1) @@ -657,7 +657,7 @@ class CCReader private (prog : Program, } } }) - (structInfos(i).name, HeapObj.CtorSignature(ADTFieldList, HeapObj.ADTSort(i+1))) + (struct.name, HeapObj.CtorSignature(ADTFieldList, HeapObj.ADTSort(i+1))) }).toList // todo: only add types that exist in the program - should also add machine arithmetic types @@ -726,7 +726,8 @@ class CCReader private (prog : Program, for (((ctor, sels), i) <- structCtors zip structSels zipWithIndex) { val fieldInfos = structInfos(i).fieldInfos val fieldsWithType = for (j <- fieldInfos.indices) yield { - assert(sels(j).name == fieldInfos(j).name) + val fullFieldName = structInfos(i).getFullFieldName(fieldInfos(j).name) + assert(sels(j).name == fullFieldName) (sels(j),{ val actualType = fieldInfos(j).typ match { case Left(ind) => CCStructField(structInfos(ind).name, structDefs) @@ -1678,7 +1679,7 @@ class CCReader private (prog : Program, private def getPtrType (ptr : Pointer, _typ : CCType) : CCType = { ptr match { - case _ : Point => CCHeapPointer(heap, _typ) + case _ : Point | _ : PointQual => CCHeapPointer(heap, _typ) // todo; support pointer qualifiers? case ptr : PointPoint => getPtrType(ptr.pointer_, CCHeapPointer(heap, _typ)) case _ => throw new TranslationException( @@ -3335,6 +3336,8 @@ class CCReader private (prog : Program, "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( "Unsupported alloc expression: " + (printer print exp)) @@ -3556,13 +3559,13 @@ class CCReader private (prog : Program, evaluatingLhs = false val subexpr = eval(exp.exp_) evaluatingLhs = evaluatingLhs_pre - val fieldName = exp.cident_ + val rawFieldName = exp.cident_ val term = subexpr.typ match { case ptrType : CCStackPointer => getPointedTerm(ptrType) case _ : CCHeapPointer => //todo: error here if field is null heapRead(subexpr) case _ => throw new TranslationException( - "Trying to access field '->" + fieldName + "' of non pointer.") + "Trying to access field '->" + rawFieldName + "' of non pointer.") } val structType = term.typ match { case typ : CCStruct => typ @@ -3571,10 +3574,16 @@ class CCReader private (prog : Program, "only implemented for structs, not " + typ + ": " + (printer print exp)) } - if(!structType.contains(fieldName)) - throw new TranslationException(fieldName + " is not a member of " + 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} in structInfos.") + } + val fullFieldName = structInfo.getFullFieldName(rawFieldName) + if(!structType.contains(fullFieldName)) + throw new TranslationException(rawFieldName + " is not a member of " + structType + "!") - val ind = structType.getFieldIndex(fieldName) + val ind = structType.getFieldIndex(fullFieldName) val fieldType = structType.getFieldType(ind) val sel = structType.getADTSelector(ind) pushVal(CCTerm(sel(term.toTerm), fieldType, srcInfo)) @@ -3639,7 +3648,8 @@ class CCReader private (prog : Program, pushVal(readValue) case _ => throw new TranslationException(getLineString(exp) + - arrayTerm + " is not an array type!") + arrayTerm + " is not a supported array type - currently only " + + "1-d arrays are supported.") } case _ => diff --git a/src/tricera/concurrency/ccreader/CCBinaryExpressions.scala b/src/tricera/concurrency/ccreader/CCBinaryExpressions.scala index 0d22709..f14d019 100644 --- a/src/tricera/concurrency/ccreader/CCBinaryExpressions.scala +++ b/src/tricera/concurrency/ccreader/CCBinaryExpressions.scala @@ -33,6 +33,7 @@ import ap.theories.ModuloArithmetic import tricera.concurrency.CCReader._ import tricera.concurrency.ccreader.CCExceptions.TranslationException import IExpression._ +import tricera.Util.getLineString object CCBinaryExpressions { object BinaryOperators { @@ -53,10 +54,16 @@ object CCBinaryExpressions { protected def getIntRes: IExpression def expr: CCExpr = { - (lhs.typ, rhs.typ) match { + try {(lhs.typ, rhs.typ) match { case (CCFloat, _) => toCCExpr(getFloatRes) case (_, CCFloat) => toCCExpr(getFloatRes) case _ => toCCExpr(getIntRes) + }} catch { + case e : IllegalArgumentException => + throw new TranslationException( + getLineString(lhs.srcInfo) + + s"Could not apply binary operator: $this\n") + case e => throw e } } diff --git a/src/tricera/concurrency/ccreader/CCType.scala b/src/tricera/concurrency/ccreader/CCType.scala index 52bf75d..7beaf5d 100644 --- a/src/tricera/concurrency/ccreader/CCType.scala +++ b/src/tricera/concurrency/ccreader/CCType.scala @@ -44,11 +44,11 @@ import scala.collection.mutable.{ } abstract sealed class CCType { - def shortName: String + def shortName : String // todo: make this abstract. nice to have them all in the same place but // would lead to runtime errors if there are missing cases. - def toSort: Sort = tricera.params.TriCeraParameters.get.arithMode match { + def toSort : Sort = tricera.params.TriCeraParameters.get.arithMode match { case ArithmeticMode.Mathematical => this match { case CCBool => Sort.Bool @@ -130,7 +130,7 @@ abstract sealed class CCType { } } - def rangePred(t: ITerm): IFormula = + def rangePred(t : ITerm) : IFormula = toSort match { case Sort.Nat => t >= 0 @@ -140,7 +140,7 @@ abstract sealed class CCType { // ADTs } - def range: (Option[IdealInt], Option[IdealInt]) = { + def range : (Option[IdealInt], Option[IdealInt]) = { toSort match { case Sort.Nat => (Some(IdealInt(0)), None) case Sort.Integer => (None, None) @@ -153,28 +153,28 @@ abstract sealed class CCType { } } - def newConstant(name: String): ConstantTerm = toSort newConstant name + def newConstant(name : String) : ConstantTerm = toSort newConstant name - def cast(t: ITerm): ITerm = toSort match { - case s: ModSort => cast2Sort(s, t) + def cast(t: ITerm) : ITerm = toSort match { + case s : ModSort => cast2Sort(s, t) case _ => t } - def cast2Unsigned(t: ITerm): ITerm = toSort match { + def cast2Unsigned(t : ITerm) : ITerm = toSort match { case SignedBVSort(n) => cast2UnsignedBV(n, t) case _ => t } - def cast(e: CCExpr): CCExpr = e match { + def cast(e : CCExpr) : CCExpr = e match { case CCTerm(t, _, srcInfo) => CCTerm(cast(t), this, srcInfo) case CCFormula(f, _, srcInfo) => CCFormula(f, this, srcInfo) } - def getNonDet: ITerm = + def getNonDet : ITerm = new SortedConstantTerm("_", toSort) // todo: make this abstract - def getZeroInit: ITerm = this match { + def getZeroInit : ITerm = this match { case structType: CCStruct => val const: IndexedSeq[ITerm] = for ((_, fieldType) <- structType.sels) @@ -194,67 +194,67 @@ abstract sealed class CCType { } abstract class CCArithType extends CCType { - val UNSIGNED_RANGE: IdealInt - val isUnsigned: Boolean + val UNSIGNED_RANGE : IdealInt + val isUnsigned : Boolean } case object CCVoid extends CCType { - override def toString: String = "void" + override def toString : String = "void" def shortName = "void" } // Logical type - only to be used in ghost code & annotations case object CCBool extends CCType { - override def toString: String = "boolean" + override def toString : String = "boolean" def shortName = "boolean" } case object CCInt extends CCArithType { - override def toString: String = "int" + override def toString : String = "int" def shortName = "int" - val UNSIGNED_RANGE: IdealInt = IdealInt("FFFFFFFF", 16) // 32bit - val isUnsigned: Boolean = false + val UNSIGNED_RANGE : IdealInt = IdealInt("FFFFFFFF", 16) // 32bit + val isUnsigned : Boolean = false } // Logical type - only to be used in ghost code & annotations case object CCMathInt extends CCType { - override def toString: String = "integer" + override def toString : String = "integer" def shortName = "integer" } case object CCUInt extends CCArithType { override def toString: String = "unsigned int" def shortName = "uint" - val UNSIGNED_RANGE: IdealInt = IdealInt("FFFFFFFF", 16) // 32bit - val isUnsigned: Boolean = true + val UNSIGNED_RANGE : IdealInt = IdealInt("FFFFFFFF", 16) // 32bit + val isUnsigned : Boolean = true } case object CCLong extends CCArithType { override def toString: String = "long" def shortName = "long" - val UNSIGNED_RANGE: IdealInt = IdealInt("FFFFFFFFFFFFFFFF", 16) // 64bit - val isUnsigned: Boolean = false + val UNSIGNED_RANGE : IdealInt = IdealInt("FFFFFFFFFFFFFFFF", 16) // 64bit + val isUnsigned : Boolean = false } case object CCULong extends CCArithType { override def toString: String = "unsigned long" def shortName = "ulong" - val UNSIGNED_RANGE: IdealInt = IdealInt("FFFFFFFFFFFFFFFF", 16) // 64bit - val isUnsigned: Boolean = true + val UNSIGNED_RANGE : IdealInt = IdealInt("FFFFFFFFFFFFFFFF", 16) // 64bit + val isUnsigned : Boolean = true } case object CCLongLong extends CCArithType { override def toString: String = "long long" def shortName = "llong" - val UNSIGNED_RANGE: IdealInt = IdealInt("FFFFFFFFFFFFFFFF", 16) // 64bit - val isUnsigned: Boolean = false + val UNSIGNED_RANGE : IdealInt = IdealInt("FFFFFFFFFFFFFFFF", 16) // 64bit + val isUnsigned : Boolean = false } case object CCULongLong extends CCArithType { - override def toString: String = "unsigned long long" + override def toString : String = "unsigned long long" def shortName = "ullong" - val UNSIGNED_RANGE: IdealInt = IdealInt("FFFFFFFFFFFFFFFF", 16) // 64bit - val isUnsigned: Boolean = true + val UNSIGNED_RANGE : IdealInt = IdealInt("FFFFFFFFFFFFFFFF", 16) // 64bit + val isUnsigned : Boolean = true } case object CCFloat extends CCType { @@ -262,35 +262,41 @@ case object CCFloat extends CCType { def shortName = "float" } -case class CCHeap(heap: Heap) extends CCType { - override def toString: String = heap.toString +case class CCHeap(heap : Heap) extends CCType { + override def toString : String = heap.toString def shortName = "heap" } /** * typ is either an index into structInfos (if ADT type), or a CCType * ptrDepth 0 => not a pointer, 1 => *, 2 => **, ... */ -case class FieldInfo(name: String, - typ: Either[Integer, CCType], - ptrDepth: Integer) +case class FieldInfo(name : String, + typ : Either[Integer, CCType], + ptrDepth : Integer) -case class StructInfo(name: String, fieldInfos: Seq[FieldInfo]) +case class StructInfo(name : String, fieldInfos : Seq[FieldInfo]) { + def getFullFieldName(rawFieldName : String) : String = + s"$name::$rawFieldName" +} -case class CCStructField(structName: String, - structs: MHashMap[String, CCStruct]) - extends CCType { +/** + * A struct field with a struct type + */ +case class CCStructField(structName : String, + structs : MHashMap[String, CCStruct]) + extends CCType { override def toString: String = "field with type: " + structName def shortName = "field:" + structName } -case class CCStruct(ctor: MonoSortedIFunction, - sels: IndexedSeq[(MonoSortedIFunction, CCType)]) - extends CCType { +case class CCStruct(ctor : MonoSortedIFunction, + sels : IndexedSeq[(MonoSortedIFunction, CCType)]) + extends CCType { 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] = + def getFieldIndex(name : String) = sels.indexWhere(_._1.name == name) + def getFieldAddress(nestedName : List[String]) : List[Int] = nestedName match { case hd :: Nil => getFieldIndex(hd) :: Nil case hd :: tl => { @@ -300,11 +306,11 @@ case class CCStruct(ctor: MonoSortedIFunction, } case Nil => Nil // not possible to reach } - def getFieldType(ind: Int): CCType = sels(ind)._2 match { + def getFieldType(ind : Int) : CCType = sels(ind)._2 match { case CCStructField(name, structs) => structs(name) case typ => typ } - def getFieldType(fieldAddress: List[Int]): CCType = + def getFieldType(fieldAddress : List[Int]) : CCType = fieldAddress match { case hd :: Nil => getFieldType(hd) case hd :: tl => @@ -318,8 +324,8 @@ case class CCStruct(ctor: MonoSortedIFunction, "empty field index!") } - def contains(fieldName: String) = getFieldIndex(fieldName) != -1 - def getFieldTerm(t: ITerm, fieldAddress: List[Int]): ITerm = { + def contains(fieldName : String) = getFieldIndex(fieldName) != -1 + def getFieldTerm(t : ITerm, fieldAddress: List[Int]): ITerm = { val hd :: tl = fieldAddress val sel = getADTSelector(hd) getFieldType(hd) match {