Skip to content

Commit

Permalink
Fixes a bug when dumping clauses as SMT, and few others.
Browse files Browse the repository at this point in the history 
- Qualifiers in pointers do not raise an error now - bug are ignored.
- Improve some error messages.
  • Loading branch information
@zafer-esen
zafer-esen committed Jan 30, 2024
1 parent f6b55d7 commit c57855f
Show file tree
Hide file tree
Showing 4 changed files with 94 additions and 69 deletions.
12 changes: 7 additions & 5 deletions src/tricera/Main.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
Expand Down
40 changes: 25 additions & 15 deletions src/tricera/concurrency/CCReader.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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(
Expand Down Expand Up @@ -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))
Expand Down Expand Up @@ -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
Expand All @@ -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))
Expand Down Expand Up @@ -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 _ =>
Expand Down
9 changes: 8 additions & 1 deletion src/tricera/concurrency/ccreader/CCBinaryExpressions.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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
}
}

Expand Down
102 changes: 54 additions & 48 deletions src/tricera/concurrency/ccreader/CCType.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -194,103 +194,109 @@ 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 {
override def toString : String = "float"
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 => {
Expand All @@ -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 =>
Expand All @@ -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 {
Expand Down

0 comments on commit c57855f

Please sign in to comment.