diff --git a/build.sc b/build.sc index 34fd4c7f28..00822d675d 100644 --- a/build.sc +++ b/build.sc @@ -41,7 +41,7 @@ object external extends Module { object viper extends ScalaModule { object silverGit extends GitModule { def url = T { "https://github.com/viperproject/silver.git" } - def commitish = T { "4a8065758868eae3414f86f3d96e843a283444fc" } + def commitish = T { "93bc9b7516a710c8f01438e430058c4a54e20512" } def filteredRepo = T { val workspace = repo() os.remove.all(workspace / "src" / "test") @@ -50,8 +50,8 @@ object viper extends ScalaModule { } object siliconGit extends GitModule { - def url = T { "https://github.com/viperproject/silicon.git" } - def commitish = T { "4033dd21614b3bbba9c7615655e41c6cf0b9d80b" } + def url = T { "https://github.com/superaxander/silicon.git" } + def commitish = T { "c63989f64eb759f33bde68c330ce07d6e34134fa" } def filteredRepo = T { val workspace = repo() os.remove.all(workspace / "src" / "test") diff --git a/examples/concepts/c/pointer_casts.c b/examples/concepts/c/pointer_casts.c new file mode 100644 index 0000000000..d09264f7aa --- /dev/null +++ b/examples/concepts/c/pointer_casts.c @@ -0,0 +1,90 @@ +#include + +struct A { + int integer; + bool boolean; +}; + +struct B { + struct A struct_a; +}; + +void canCastToInteger() { + struct B struct_b; + struct_b.struct_a.integer = 5; + int *pointer_to_integer = (int *)&struct_b; + //@ assert *pointer_to_integer == 5; + //@ assert pointer_to_integer == &struct_b.struct_a.integer; + //@ assert pointer_to_integer == (int *)&struct_b.struct_a; + // The following is not implemented yet + // assert pointer_to_integer == &struct_b + // assert pointer_to_integer == &struct_b.struct_a + *pointer_to_integer = 10; + //@ assert struct_b.struct_a.integer == 10; +} + + +void castRemainsValidInLoop() { + struct B struct_b; + struct_b.struct_a.integer = 10; + + int *pointer_to_integer = (int *)&struct_b; + + //@ loop_invariant 0 <= i && i <= 10; + //@ loop_invariant Perm(&struct_b, write); + //@ loop_invariant Perm(struct_b, write); + //@ loop_invariant pointer_to_integer == (int *)&struct_b; + //@ loop_invariant *pointer_to_integer == 10 - i; + for (int i = 0; i < 10; i++) { + *pointer_to_integer = *pointer_to_integer - 1; + } + + //@ assert struct_b.struct_a.integer == 0; + struct_b.struct_a.integer = 10; + + // We can also specify the permission through the pointer + //@ loop_invariant 0 <= i && i <= 10; + //@ loop_invariant Perm(pointer_to_integer, write); + //@ loop_invariant *pointer_to_integer == 10 - i; + for (int i = 0; i < 10; i++) { + *pointer_to_integer = *pointer_to_integer - 1; + } + + //@ assert struct_b.struct_a.integer == 0; +} + +void castRemainsValidInParBlock() { + struct B struct_b; + struct_b.struct_a.integer = 10; + + int *pointer_to_integer = (int *)&struct_b; + + //@ context i == 8 ==> Perm(pointer_to_integer, write); + //@ ensures i == 8 ==> *pointer_to_integer == 0; + for (int i = 0; i < 10; i++) { + if (i == 8) { + *pointer_to_integer = *pointer_to_integer - 10; + } + } + + // Unfortunately we don't support a par block where we specify permission to the struct and then access through the cast (the generated cast helper is put too far away) + + //@ assert struct_b.struct_a.integer == 0; +} + +//@ requires a != NULL; +//@ context Perm(a, write); +//@ ensures *a == \old(*a) + 1; +void increaseByOne(int *a) { + *a += 1; +} + +void callWithCast() { + struct B struct_b; + struct_b.struct_a.integer = 15; + + int *pointer_to_integer = (int *)&struct_b; + increaseByOne(pointer_to_integer); + + //@ assert struct_b.struct_a.integer == 16; +} diff --git a/examples/concepts/c/structs.c b/examples/concepts/c/structs.c index 44882c9ac6..4638fd1ac4 100644 --- a/examples/concepts/c/structs.c +++ b/examples/concepts/c/structs.c @@ -21,8 +21,8 @@ struct linked_list{ /*@ context p != NULL ** Perm(p, write); - context Perm(p->x, write); - context Perm(p->y, write); + context Perm(&p->x, write); + context Perm(&p->y, write); ensures p->x == 0; ensures p->y == 0; ensures \old(*p) == *p; @@ -44,14 +44,15 @@ void alter_struct_1(struct point *p){ } /*@ - context Perm(p.x, 1\1); - context Perm(p.y, 1\1); + context Perm(&p.x, 1\1); + context Perm(&p.y, 1\1); @*/ void alter_copy_struct(struct point p){ p.x = 0; p.y = 0; } +// TODO: Should be auto-generated /*@ context Perm(p, 1\1); @*/ @@ -75,7 +76,7 @@ int avr_x(struct triangle *r){ requires inp != NULL && \pointer_length(inp) >= n; requires (\forall* int i; 0 <= i && i < n; Perm(&inp[i], 1\10)); requires (\forall int i, int j; 0<=i && i {:inp[i]:} != {:inp[j]:}); - requires (\forall* int i; 0 <= i && i < n; Perm(inp[i].x, 1\10)); + requires (\forall* int i; 0 <= i && i < n; Perm(&inp[i].x, 1\10)); ensures |\result| == n; ensures (\forall int i; 0 <= i && i < n; \result[i] == inp[i].x); //ensures n>0 ==> \result == inp_to_seq(inp, n-1) + [inp[n-1].x]; @@ -132,7 +133,7 @@ int main(){ struct point *pp; pp = &p; - //@ assert (pp[0] != NULL ); + /* //@ assert (pp[0] != NULL ); */ assert (pp != NULL ); p.x = 1; @@ -168,4 +169,4 @@ int main(){ assert(avr_pol == 2); return 0; -} \ No newline at end of file +} diff --git a/res/universal/res/adt/pointer.pvl b/res/universal/res/adt/pointer.pvl index 743584d8b4..9cbbedb16b 100644 --- a/res/universal/res/adt/pointer.pvl +++ b/res/universal/res/adt/pointer.pvl @@ -16,6 +16,7 @@ adt `pointer` { pure `pointer` pointer_of(`block` b, int offset); pure `block` pointer_block(`pointer` p); pure int pointer_offset(`pointer` p); + pure `pointer` pointer_inv(ref r); // the block offset is valid wrt the length of the block axiom (∀ `pointer` p; @@ -26,6 +27,10 @@ adt `pointer` { axiom (∀`block` b, int offset; {:pointer_block(pointer_of(b, offset)):} == b && {:pointer_offset(pointer_of(b, offset)):} == offset); + + axiom (∀ ref r; ptr_deref({:pointer_inv(r):}) == r); + + axiom (∀ `pointer` p; pointer_inv({:ptr_deref(p):}) == p); } decreases; @@ -38,4 +43,4 @@ requires `pointer`.pointer_offset(p) + offset < `block`.block_length(`pointer`.p pure `pointer` ptr_add(`pointer` p, int offset) = `pointer`.pointer_of( `pointer`.pointer_block(p), - `pointer`.pointer_offset(p) + offset); \ No newline at end of file + `pointer`.pointer_offset(p) + offset); diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 59d8d36153..80842a9769 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -107,6 +107,7 @@ final case class VerificationContext[G](program: Program[G])( @scopes[ModelDeclaration] @scopes[EnumConstant] @scopes[Variable] +@scopes[LocalHeapVariable] final case class Program[G](declarations: Seq[GlobalDeclaration[G]])( val blame: Blame[UnsafeCoercion] )(implicit val o: Origin) @@ -132,6 +133,9 @@ final case class TArray[G](element: Type[G])( final case class TPointer[G](element: Type[G])( implicit val o: Origin = DiagnosticOrigin ) extends Type[G] with TPointerImpl[G] +final case class TNonNullPointer[G](element: Type[G])( + implicit val o: Origin = DiagnosticOrigin +) extends Type[G] with TNonNullPointerImpl[G] final case class TType[G](t: Type[G])(implicit val o: Origin = DiagnosticOrigin) extends Type[G] with TTypeImpl[G] final case class TVar[G](ref: Ref[G, Variable[G]])( @@ -218,9 +222,17 @@ sealed trait DeclaredType[G] extends Type[G] with DeclaredTypeImpl[G] final case class TModel[G](model: Ref[G, Model[G]])( implicit val o: Origin = DiagnosticOrigin ) extends DeclaredType[G] with TModelImpl[G] -final case class TClass[G](cls: Ref[G, Class[G]], typeArgs: Seq[Type[G]])( - implicit val o: Origin = DiagnosticOrigin -) extends DeclaredType[G] with TClassImpl[G] +sealed trait TClass[G] extends DeclaredType[G] with TClassImpl[G] +final case class TByReferenceClass[G]( + cls: Ref[G, Class[G]], + typeArgs: Seq[Type[G]], +)(implicit val o: Origin = DiagnosticOrigin) + extends TClass[G] with TByReferenceClassImpl[G] +final case class TByValueClass[G]( + cls: Ref[G, Class[G]], + typeArgs: Seq[Type[G]], +)(implicit val o: Origin = DiagnosticOrigin) + extends TClass[G] with TByValueClassImpl[G] final case class TAnyClass[G]()(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TAnyClassImpl[G] final case class TAxiomatic[G]( @@ -249,6 +261,7 @@ final case class ParSequential[G](regions: Seq[ParRegion[G]])( )(implicit val o: Origin) extends ParRegion[G] with ParSequentialImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] @scopes[SendDecl] @scopes[ParBlockDecl] final case class ParBlock[G]( @@ -276,6 +289,7 @@ final case class IterationContract[G]( extends LoopContract[G] with IterationContractImpl[G] @family @scopes[Variable] +@scopes[LocalHeapVariable] final case class CatchClause[G](decl: Variable[G], body: Statement[G])( implicit val o: Origin ) extends NodeFamily[G] with CatchClauseImpl[G] @@ -314,6 +328,11 @@ final case class LocalDecl[G](local: Variable[G])(implicit val o: Origin) extends NonExecutableStatement[G] with PurelySequentialStatement[G] with LocalDeclImpl[G] +final case class HeapLocalDecl[G](local: LocalHeapVariable[G])( + implicit val o: Origin +) extends NonExecutableStatement[G] + with PurelySequentialStatement[G] + with HeapLocalDeclImpl[G] final case class SpecIgnoreStart[G]()(implicit val o: Origin) extends NonExecutableStatement[G] with PurelySequentialStatement[G] @@ -520,6 +539,7 @@ final case class Block[G](statements: Seq[Statement[G]])(implicit val o: Origin) with ControlContainerStatement[G] with BlockImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] @scopes[CLocalDeclaration] @scopes[CPPLocalDeclaration] @scopes[JavaLocalDeclaration] @@ -555,6 +575,7 @@ final case class Loop[G]( with ControlContainerStatement[G] with LoopImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final case class RangedFor[G]( iter: IterVariable[G], contract: LoopContract[G], @@ -609,6 +630,7 @@ final case class ParStatement[G](impl: ParRegion[G])(implicit val o: Origin) with PurelySequentialStatement[G] with ParStatementImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final case class VecBlock[G]( iters: Seq[IterVariable[G]], requires: Expr[G], @@ -643,18 +665,26 @@ final class HeapVariable[G](val t: Type[G])(implicit val o: Origin) final class SimplificationRule[G](val axiom: Expr[G])(implicit val o: Origin) extends GlobalDeclaration[G] with SimplificationRuleImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final class AxiomaticDataType[G]( val decls: Seq[ADTDeclaration[G]], val typeArgs: Seq[Variable[G]], )(implicit val o: Origin) extends GlobalDeclaration[G] with AxiomaticDataTypeImpl[G] -final class Class[G]( +sealed trait Class[G] extends GlobalDeclaration[G] with ClassImpl[G] +final class ByReferenceClass[G]( val typeArgs: Seq[Variable[G]], val decls: Seq[ClassDeclaration[G]], val supports: Seq[Type[G]], val intrinsicLockInvariant: Expr[G], )(implicit val o: Origin) - extends GlobalDeclaration[G] with ClassImpl[G] + extends Class[G] with ByReferenceClassImpl[G] +final class ByValueClass[G]( + val typeArgs: Seq[Variable[G]], + val decls: Seq[ClassDeclaration[G]], + val supports: Seq[Type[G]], +)(implicit val o: Origin) + extends Class[G] with ByValueClassImpl[G] final class Model[G](val declarations: Seq[ModelDeclaration[G]])( implicit val o: Origin ) extends GlobalDeclaration[G] with Declarator[G] with ModelImpl[G] @@ -687,6 +717,7 @@ final class VeSUVMainMethod[G](val body: Option[Statement[G]])( )(implicit val o: Origin) extends GlobalDeclaration[G] with VeSUVMainMethodImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final class Predicate[G]( val args: Seq[Variable[G]], val body: Option[Expr[G]], @@ -759,6 +790,7 @@ final class InstanceMethod[G]( with AbstractMethod[G] with InstanceMethodImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final class InstancePredicate[G]( val args: Seq[Variable[G]], val body: Option[Expr[G]], @@ -814,6 +846,7 @@ sealed trait ModelDeclaration[G] final class ModelField[G](val t: Type[G])(implicit val o: Origin) extends ModelDeclaration[G] with Field[G] with ModelFieldImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final class ModelProcess[G]( val args: Seq[Variable[G]], val impl: Expr[G], @@ -824,6 +857,7 @@ final class ModelProcess[G]( )(val blame: Blame[PostconditionFailed])(implicit val o: Origin) extends ModelDeclaration[G] with Applicable[G] with ModelProcessImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final class ModelAction[G]( val args: Seq[Variable[G]], val requires: Expr[G], @@ -838,6 +872,7 @@ sealed trait ADTDeclaration[G] extends Declaration[G] with ADTDeclarationImpl[G] final class ADTAxiom[G](val axiom: Expr[G])(implicit val o: Origin) extends ADTDeclaration[G] with ADTAxiomImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final class ADTFunction[G](val args: Seq[Variable[G]], val returnType: Type[G])( implicit val o: Origin ) extends Applicable[G] with ADTDeclaration[G] with ADTFunctionImpl[G] @@ -846,6 +881,9 @@ final class ADTFunction[G](val args: Seq[Variable[G]], val returnType: Type[G])( final class Variable[G](val t: Type[G])(implicit val o: Origin) extends Declaration[G] with VariableImpl[G] @family +final class LocalHeapVariable[G](val t: Type[G])(implicit val o: Origin) + extends Declaration[G] with LocalHeapVariableImpl[G] +@family final class LabelDecl[G]()(implicit val o: Origin) extends Declaration[G] with LabelDeclImpl[G] @family @@ -872,6 +910,7 @@ sealed trait AbstractMethod[G] sealed trait Field[G] extends FieldImpl[G] @family @scopes[Variable] +@scopes[LocalHeapVariable] final case class SignalsClause[G](binding: Variable[G], assn: Expr[G])( implicit val o: Origin ) extends NodeFamily[G] with SignalsClauseImpl[G] @@ -973,6 +1012,9 @@ final case class CoerceNullAnyClass[G]()(implicit val o: Origin) final case class CoerceNullPointer[G](pointerElementType: Type[G])( implicit val o: Origin ) extends Coercion[G] with CoerceNullPointerImpl[G] +final case class CoerceNonNullPointer[G](elementType: Type[G])( + implicit val o: Origin +) extends Coercion[G] with CoerceNonNullPointerImpl[G] final case class CoerceNullEnum[G](targetEnum: Ref[G, Enum[G]])( implicit val o: Origin ) extends Coercion[G] with CoerceNullEnumImpl[G] @@ -1260,6 +1302,7 @@ final case class MapRemove[G](map: Expr[G], k: Expr[G])(implicit val o: Origin) sealed trait Binder[G] extends Expr[G] with BinderImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final case class Forall[G]( bindings: Seq[Variable[G]], triggers: Seq[Seq[Expr[G]]], @@ -1267,6 +1310,7 @@ final case class Forall[G]( )(implicit val o: Origin) extends Binder[G] with ForallImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final case class Starall[G]( bindings: Seq[Variable[G]], triggers: Seq[Seq[Expr[G]]], @@ -1274,6 +1318,7 @@ final case class Starall[G]( )(val blame: Blame[ReceiverNotInjective])(implicit val o: Origin) extends Binder[G] with StarallImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final case class Exists[G]( bindings: Seq[Variable[G]], triggers: Seq[Seq[Expr[G]]], @@ -1281,6 +1326,7 @@ final case class Exists[G]( )(implicit val o: Origin) extends Binder[G] with ExistsImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final case class Sum[G]( bindings: Seq[Variable[G]], condition: Expr[G], @@ -1288,6 +1334,7 @@ final case class Sum[G]( )(implicit val o: Origin) extends Binder[G] with SumImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final case class Product[G]( bindings: Seq[Variable[G]], condition: Expr[G], @@ -1295,6 +1342,7 @@ final case class Product[G]( )(implicit val o: Origin) extends Binder[G] with ProductImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final case class ForPerm[G]( bindings: Seq[Variable[G]], loc: Location[G], @@ -1302,10 +1350,12 @@ final case class ForPerm[G]( )(implicit val o: Origin) extends Binder[G] with ForPermImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final case class ForPermWithValue[G](binding: Variable[G], body: Expr[G])( implicit val o: Origin ) extends Binder[G] with ForPermWithValueImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final case class Let[G](binding: Variable[G], value: Expr[G], main: Expr[G])( implicit val o: Origin ) extends Binder[G] with LetImpl[G] @@ -1317,12 +1367,17 @@ final case class InlinePattern[G]( extends Expr[G] with InlinePatternImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final case class ScopedExpr[G](declarations: Seq[Variable[G]], body: Expr[G])( implicit val o: Origin ) extends Declarator[G] with Expr[G] with ScopedExprImpl[G] final case class Local[G](ref: Ref[G, Variable[G]])(implicit val o: Origin) extends Expr[G] with LocalImpl[G] +final case class HeapLocal[G](ref: Ref[G, LocalHeapVariable[G]])( + implicit val o: Origin +) extends Expr[G] with HeapLocalImpl[G] + final case class EnumUse[G]( enum: Ref[G, Enum[G]], const: Ref[G, EnumConstant[G]], @@ -1345,6 +1400,10 @@ final case class DerefPointer[G](pointer: Expr[G])( val blame: Blame[PointerDerefError] )(implicit val o: Origin) extends Expr[G] with DerefPointerImpl[G] +final case class RawDerefPointer[G](pointer: Expr[G])( + val blame: Blame[PointerDerefError] +)(implicit val o: Origin) + extends Expr[G] with RawDerefPointerImpl[G] final case class PointerAdd[G](pointer: Expr[G], offset: Expr[G])( val blame: Blame[PointerAddError] )(implicit val o: Origin) @@ -1698,6 +1757,10 @@ final case class PointerLocation[G](pointer: Expr[G])( val blame: Blame[PointerLocationError] )(implicit val o: Origin) extends Location[G] with PointerLocationImpl[G] +final case class ByValueClassLocation[G](expr: Expr[G])( + val blame: Blame[PointerLocationError] +)(implicit val o: Origin) + extends Location[G] with ByValueClassLocationImpl[G] final case class PredicateLocation[G](inv: ApplyAnyPredicate[G])( implicit val o: Origin ) extends Location[G] with PredicateLocationImpl[G] @@ -1824,6 +1887,10 @@ final case class NewPointerArray[G](element: Type[G], size: Expr[G])( val blame: Blame[ArraySizeError] )(implicit val o: Origin) extends Expr[G] with NewPointerArrayImpl[G] +final case class NewNonNullPointerArray[G](element: Type[G], size: Expr[G])( + val blame: Blame[ArraySizeError] +)(implicit val o: Origin) + extends Expr[G] with NewNonNullPointerArrayImpl[G] final case class FreePointer[G](pointer: Expr[G])( val blame: Blame[PointerFreeError] )(implicit val o: Origin) @@ -2716,10 +2783,9 @@ final case class GpgpuAtomic[G]( extends CStatement[G] with GpgpuAtomicImpl[G] sealed trait CExpr[G] extends Expr[G] with CExprImpl[G] -final case class CLocal[G](name: String)( - val blame: Blame[DerefInsufficientPermission] -)(implicit val o: Origin) - extends CExpr[G] with CLocalImpl[G] { +final case class CLocal[G](name: String)(val blame: Blame[FrontendDerefError])( + implicit val o: Origin +) extends CExpr[G] with CLocalImpl[G] { var ref: Option[CNameTarget[G]] = None } final case class CInvocation[G]( @@ -3108,6 +3174,7 @@ sealed trait JavaClassOrInterface[G] with Declarator[G] with JavaClassOrInterfaceImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final class JavaClass[G]( val name: String, val modifiers: Seq[JavaModifier[G]], @@ -3119,6 +3186,7 @@ final class JavaClass[G]( )(val blame: Blame[JavaImplicitConstructorFailure])(implicit val o: Origin) extends JavaClassOrInterface[G] with JavaClassImpl[G] @scopes[Variable] +@scopes[LocalHeapVariable] final class JavaInterface[G]( val name: String, val modifiers: Seq[JavaModifier[G]], diff --git a/src/col/vct/col/ast/declaration/global/ByReferenceClassImpl.scala b/src/col/vct/col/ast/declaration/global/ByReferenceClassImpl.scala new file mode 100644 index 0000000000..ec95adbe7c --- /dev/null +++ b/src/col/vct/col/ast/declaration/global/ByReferenceClassImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.declaration.global + +import vct.col.ast.{ByReferenceClass, TByReferenceClass, Type} +import vct.col.ast.ops.ByReferenceClassOps + +trait ByReferenceClassImpl[G] extends ByReferenceClassOps[G] { + this: ByReferenceClass[G] => + override def classType(typeArgs: Seq[Type[G]]): TByReferenceClass[G] = + TByReferenceClass[G](this.ref, typeArgs) +} diff --git a/src/col/vct/col/ast/declaration/global/ByValueClassImpl.scala b/src/col/vct/col/ast/declaration/global/ByValueClassImpl.scala new file mode 100644 index 0000000000..e776781309 --- /dev/null +++ b/src/col/vct/col/ast/declaration/global/ByValueClassImpl.scala @@ -0,0 +1,12 @@ +package vct.col.ast.declaration.global + +import vct.col.ast.{ByValueClass, Expr, InstanceField, TByValueClass, Type} +import vct.col.ast.ops.ByValueClassOps +import vct.col.util.AstBuildHelpers._ + +trait ByValueClassImpl[G] extends ByValueClassOps[G] { + this: ByValueClass[G] => + override def intrinsicLockInvariant: Expr[G] = tt + override def classType(typeArgs: Seq[Type[G]]): TByValueClass[G] = + TByValueClass[G](this.ref, typeArgs) +} diff --git a/src/col/vct/col/ast/declaration/global/ClassImpl.scala b/src/col/vct/col/ast/declaration/global/ClassImpl.scala index 5e05d78d80..251557ee8d 100644 --- a/src/col/vct/col/ast/declaration/global/ClassImpl.scala +++ b/src/col/vct/col/ast/declaration/global/ClassImpl.scala @@ -1,18 +1,37 @@ package vct.col.ast.declaration.global -import vct.col.ast.{Class, Declaration, InstanceField, TClass, TVar} +import vct.col.ast.{ + Class, + ClassDeclaration, + Declaration, + Expr, + InstanceField, + TByReferenceClass, + TClass, + TVar, + Type, + Variable, +} import vct.col.ast.util.Declarator import vct.col.print._ import vct.col.util.AstBuildHelpers.tt -import vct.result.VerificationError.Unreachable -import vct.col.ast.ops.ClassOps -trait ClassImpl[G] extends Declarator[G] with ClassOps[G] { +trait ClassImpl[G] extends Declarator[G] { this: Class[G] => + def typeArgs: Seq[Variable[G]] + def decls: Seq[ClassDeclaration[G]] + def supports: Seq[Type[G]] + def intrinsicLockInvariant: Expr[G] + + def classType(typeArgs: Seq[Type[G]]): TClass[G] + def transSupportArrowsHelper( seen: Set[TClass[G]] ): Seq[(TClass[G], TClass[G])] = { - val t: TClass[G] = TClass(this.ref, typeArgs.map(v => TVar(v.ref))) + // TODO: Does this break things if we have a ByValueClass with supers? + val t: TClass[G] = classType( + typeArgs.map((v: Variable[G]) => TVar(v.ref[Variable[G]])) + ) if (seen.contains(t)) Nil else diff --git a/src/col/vct/col/ast/declaration/singular/EndpointImpl.scala b/src/col/vct/col/ast/declaration/singular/EndpointImpl.scala index 944ad3d7bf..8701db45e9 100644 --- a/src/col/vct/col/ast/declaration/singular/EndpointImpl.scala +++ b/src/col/vct/col/ast/declaration/singular/EndpointImpl.scala @@ -1,7 +1,7 @@ package vct.col.ast.declaration.singular import vct.col.ast.declaration.DeclarationImpl -import vct.col.ast.{Endpoint, TClass, Type} +import vct.col.ast.{Endpoint, TByReferenceClass, TClass, Type} import vct.col.print._ import vct.col.ast.ops.{EndpointFamilyOps, EndpointOps} import vct.col.check.{CheckContext, CheckError} @@ -12,7 +12,7 @@ trait EndpointImpl[G] override def layout(implicit ctx: Ctx): Doc = Group(Text("endpoint") <+> ctx.name(this) <+> "=" <+> init) - def t: TClass[G] = TClass(cls, typeArgs) + def t: TClass[G] = TByReferenceClass(cls, typeArgs) override def check(ctx: CheckContext[G]): Seq[CheckError] = super.check(ctx) diff --git a/src/col/vct/col/ast/declaration/singular/LocalHeapVariableImpl.scala b/src/col/vct/col/ast/declaration/singular/LocalHeapVariableImpl.scala new file mode 100644 index 0000000000..2814eed660 --- /dev/null +++ b/src/col/vct/col/ast/declaration/singular/LocalHeapVariableImpl.scala @@ -0,0 +1,18 @@ +package vct.col.ast.declaration.singular + +import vct.col.ast.LocalHeapVariable +import vct.col.print._ +import vct.col.ast.ops.{LocalHeapVariableOps, VariableFamilyOps} +import vct.col.ast.ops.{LocalHeapVariableOps, LocalHeapVariableFamilyOps} + +trait LocalHeapVariableImpl[G] extends LocalHeapVariableOps[G] with LocalHeapVariableFamilyOps[G] { + this: LocalHeapVariable[G] => + override def layout(implicit ctx: Ctx): Doc = + Text("@heap") <+> (ctx.syntax match { + case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP => + val (spec, decl) = t.layoutSplitDeclarator + spec <+> decl <> ctx.name(this) + case Ctx.PVL | Ctx.Java => t.show <+> ctx.name(this) + case Ctx.Silver => Text(ctx.name(this)) <> ":" <+> t + }) +} diff --git a/src/col/vct/col/ast/expr/ambiguous/AmbiguousPlusImpl.scala b/src/col/vct/col/ast/expr/ambiguous/AmbiguousPlusImpl.scala index 8a227e7898..73233d9105 100644 --- a/src/col/vct/col/ast/expr/ambiguous/AmbiguousPlusImpl.scala +++ b/src/col/vct/col/ast/expr/ambiguous/AmbiguousPlusImpl.scala @@ -20,7 +20,7 @@ trait AmbiguousPlusImpl[G] extends AmbiguousPlusOps[G] { right val decls = subject.t match { - case TClass(Ref(cls), _) => cls.decls + case t: TClass[G] => t.cls.decl.decls case JavaTClass(Ref(cls), _) => cls.decls case _ => return None } @@ -62,6 +62,18 @@ trait AmbiguousPlusImpl[G] extends AmbiguousPlusOps[G] { getCustomPlusOpType().get else getNumericType + if (isProcessOp) + TProcess() + else if (isSeqOp || isBagOp || isSetOp || isVectorOp) + Types.leastCommonSuperType(left.t, right.t) + else if (isPointerOp) + left.t + else if (isStringOp) + TString() + else if (getCustomPlusOpType().isDefined) + getCustomPlusOpType().get + else + getNumericType } override def precedence: Int = Precedence.ADDITIVE diff --git a/src/col/vct/col/ast/expr/context/AmbiguousThisImpl.scala b/src/col/vct/col/ast/expr/context/AmbiguousThisImpl.scala index 01b0ab843c..18cad16207 100644 --- a/src/col/vct/col/ast/expr/context/AmbiguousThisImpl.scala +++ b/src/col/vct/col/ast/expr/context/AmbiguousThisImpl.scala @@ -17,9 +17,8 @@ trait AmbiguousThisImpl[G] extends AmbiguousThisOps[G] { ) match { case RefJavaClass(decl) => JavaTClass(decl.ref, Nil) case RefClass(decl) => - TClass( - decl.ref, - decl.typeArgs.map((v: Variable[G]) => TVar(v.ref[Variable[G]])), + decl.classType( + decl.typeArgs.map((v: Variable[G]) => TVar(v.ref[Variable[G]])) ) case RefModel(decl) => TModel(decl.ref) case RefPVLChoreography(decl) => TPVLChoreography(decl.ref) diff --git a/src/col/vct/col/ast/expr/context/ThisObjectImpl.scala b/src/col/vct/col/ast/expr/context/ThisObjectImpl.scala index 25e90414f7..74a515cf8d 100644 --- a/src/col/vct/col/ast/expr/context/ThisObjectImpl.scala +++ b/src/col/vct/col/ast/expr/context/ThisObjectImpl.scala @@ -8,7 +8,9 @@ import vct.col.check.{CheckContext, CheckError, ThisInConstructorPre} trait ThisObjectImpl[G] extends ThisDeclarationImpl[G] with ThisObjectOps[G] { this: ThisObject[G] => override def t: Type[G] = - TClass(cls, cls.decl.typeArgs.map(v => TVar(v.ref[Variable[G]]))) + cls.decl.classType(cls.decl.typeArgs.map((v: Variable[G]) => + TVar(v.ref[Variable[G]]) + )) override def check(context: CheckContext[G]): Seq[CheckError] = { val inConstructor = diff --git a/src/col/vct/col/ast/expr/heap/alloc/NewNonNullPointerArrayImpl.scala b/src/col/vct/col/ast/expr/heap/alloc/NewNonNullPointerArrayImpl.scala new file mode 100644 index 0000000000..abc8896755 --- /dev/null +++ b/src/col/vct/col/ast/expr/heap/alloc/NewNonNullPointerArrayImpl.scala @@ -0,0 +1,14 @@ +package vct.col.ast.expr.heap.alloc + +import vct.col.ast.ops.NewNonNullPointerArrayOps +import vct.col.ast.{NewNonNullPointerArray, TNonNullPointer, Type} +import vct.col.print._ + +trait NewNonNullPointerArrayImpl[G] extends NewNonNullPointerArrayOps[G] { + this: NewNonNullPointerArray[G] => + override lazy val t: Type[G] = TNonNullPointer(element) + + override def precedence: Int = Precedence.POSTFIX + override def layout(implicit ctx: Ctx): Doc = + Text("new") <+> element <> "[" <> size <> "]" +} diff --git a/src/col/vct/col/ast/expr/heap/alloc/NewObjectImpl.scala b/src/col/vct/col/ast/expr/heap/alloc/NewObjectImpl.scala index dbc0fa2953..f5e8ead476 100644 --- a/src/col/vct/col/ast/expr/heap/alloc/NewObjectImpl.scala +++ b/src/col/vct/col/ast/expr/heap/alloc/NewObjectImpl.scala @@ -1,12 +1,12 @@ package vct.col.ast.expr.heap.alloc -import vct.col.ast.{NewObject, TClass, Type} +import vct.col.ast.{NewObject, Type} import vct.col.print.{Ctx, Doc, Precedence, Text} import vct.col.ast.ops.NewObjectOps trait NewObjectImpl[G] extends NewObjectOps[G] { this: NewObject[G] => - override def t: Type[G] = TClass(cls, Seq()) + override def t: Type[G] = cls.decl.classType(Seq()) override def precedence: Int = Precedence.POSTFIX override def layout(implicit ctx: Ctx): Doc = diff --git a/src/col/vct/col/ast/expr/heap/read/RawDerefPointerImpl.scala b/src/col/vct/col/ast/expr/heap/read/RawDerefPointerImpl.scala new file mode 100644 index 0000000000..d270112e07 --- /dev/null +++ b/src/col/vct/col/ast/expr/heap/read/RawDerefPointerImpl.scala @@ -0,0 +1,14 @@ +package vct.col.ast.expr.heap.read + +import vct.col.ast.ops.RawDerefPointerOps +import vct.col.ast.{RawDerefPointer, TRef, Type} +import vct.col.print._ + +trait RawDerefPointerImpl[G] extends RawDerefPointerOps[G] { + this: RawDerefPointer[G] => + override def t: Type[G] = TRef() + + override def precedence: Int = Precedence.POSTFIX + override def layout(implicit ctx: Ctx): Doc = + Group(Text("ptr_deref(") <> pointer <> Text(")")) +} diff --git a/src/col/vct/col/ast/expr/misc/HeapLocalImpl.scala b/src/col/vct/col/ast/expr/misc/HeapLocalImpl.scala new file mode 100644 index 0000000000..d397452dc6 --- /dev/null +++ b/src/col/vct/col/ast/expr/misc/HeapLocalImpl.scala @@ -0,0 +1,17 @@ +package vct.col.ast.expr.misc + +import vct.col.ast.expr.ExprImpl +import vct.col.ast.{HeapLocal, Type} +import vct.col.check.{CheckContext, CheckError} +import vct.col.print.{Ctx, Doc, Precedence, Text} +import vct.col.ast.ops.HeapLocalOps + +trait HeapLocalImpl[G] extends ExprImpl[G] with HeapLocalOps[G] { + this: HeapLocal[G] => + override def t: Type[G] = ref.decl.t + override def check(context: CheckContext[G]): Seq[CheckError] = + context.checkInScope(this, ref) + + override def precedence: Int = Precedence.ATOMIC + override def layout(implicit ctx: Ctx): Doc = Text(ctx.name(ref)) +} diff --git a/src/col/vct/col/ast/family/coercion/CoerceNonNullPointerImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceNonNullPointerImpl.scala new file mode 100644 index 0000000000..2dd5617753 --- /dev/null +++ b/src/col/vct/col/ast/family/coercion/CoerceNonNullPointerImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.family.coercion + +import vct.col.ast.ops.CoerceNonNullPointerOps +import vct.col.ast.{CoerceNonNullPointer, TPointer} + +trait CoerceNonNullPointerImpl[G] extends CoerceNonNullPointerOps[G] { + this: CoerceNonNullPointer[G] => + override def target: TPointer[G] = TPointer(elementType) +} diff --git a/src/col/vct/col/ast/family/coercion/CoerceNullClassImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceNullClassImpl.scala index 4dc7f0662b..01b76c7319 100644 --- a/src/col/vct/col/ast/family/coercion/CoerceNullClassImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoerceNullClassImpl.scala @@ -5,5 +5,5 @@ import vct.col.ast.ops.CoerceNullClassOps trait CoerceNullClassImpl[G] extends CoerceNullClassOps[G] { this: CoerceNullClass[G] => - override def target: TClass[G] = TClass(targetClass, typeArgs) + override def target: TClass[G] = targetClass.decl.classType(typeArgs) } diff --git a/src/col/vct/col/ast/family/coercion/CoerceSupportsImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceSupportsImpl.scala index c24da04581..d9094cd3b7 100644 --- a/src/col/vct/col/ast/family/coercion/CoerceSupportsImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoerceSupportsImpl.scala @@ -7,5 +7,7 @@ trait CoerceSupportsImpl[G] extends CoerceSupportsOps[G] { this: CoerceSupports[G] => // TODO: Generics are not properly taken into account here override def target: TClass[G] = - TClass(targetClass, { assert(sourceClass.decl.typeArgs.isEmpty); Seq() }) + targetClass.decl.classType({ + assert(sourceClass.decl.typeArgs.isEmpty); Seq() + }) } diff --git a/src/col/vct/col/ast/family/location/ByValueClassLocationImpl.scala b/src/col/vct/col/ast/family/location/ByValueClassLocationImpl.scala new file mode 100644 index 0000000000..225d574c96 --- /dev/null +++ b/src/col/vct/col/ast/family/location/ByValueClassLocationImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.family.location + +import vct.col.ast.ByValueClassLocation +import vct.col.ast.ops.ByValueClassLocationOps +import vct.col.print.{Ctx, Doc} + +trait ByValueClassLocationImpl[G] extends ByValueClassLocationOps[G] { + this: ByValueClassLocation[G] => + override def layout(implicit ctx: Ctx): Doc = expr.show +} diff --git a/src/col/vct/col/ast/lang/pvl/PVLEndpointImpl.scala b/src/col/vct/col/ast/lang/pvl/PVLEndpointImpl.scala index 24231f18cf..f7ac1f1470 100644 --- a/src/col/vct/col/ast/lang/pvl/PVLEndpointImpl.scala +++ b/src/col/vct/col/ast/lang/pvl/PVLEndpointImpl.scala @@ -7,5 +7,5 @@ trait PVLEndpointImpl[G] extends PVLEndpointOps[G] { this: PVLEndpoint[G] => // override def layout(implicit ctx: Ctx): Doc = ??? - def t: TClass[G] = TClass(cls, typeArgs) + def t: TClass[G] = cls.decl.classType(typeArgs) } diff --git a/src/col/vct/col/ast/statement/nonexecutable/HeapLocalDeclImpl.scala b/src/col/vct/col/ast/statement/nonexecutable/HeapLocalDeclImpl.scala new file mode 100644 index 0000000000..2b7e8650fd --- /dev/null +++ b/src/col/vct/col/ast/statement/nonexecutable/HeapLocalDeclImpl.scala @@ -0,0 +1,14 @@ +package vct.col.ast.statement.nonexecutable + +import vct.col.ast.HeapLocalDecl +import vct.col.print.{Ctx, Doc, Text} +import vct.col.ast.ops.HeapLocalDeclOps + +trait HeapLocalDeclImpl[G] extends HeapLocalDeclOps[G] { + this: HeapLocalDecl[G] => + override def layout(implicit ctx: Ctx): Doc = + ctx.syntax match { + case Ctx.Silver => Text("var") <+> local.show + case _ => local.show <> ";" + } +} diff --git a/src/col/vct/col/ast/type/TByReferenceClassImpl.scala b/src/col/vct/col/ast/type/TByReferenceClassImpl.scala new file mode 100644 index 0000000000..8a800321e9 --- /dev/null +++ b/src/col/vct/col/ast/type/TByReferenceClassImpl.scala @@ -0,0 +1,8 @@ +package vct.col.ast.`type` + +import vct.col.ast.TByReferenceClass +import vct.col.ast.ops.TByReferenceClassOps + +trait TByReferenceClassImpl[G] extends TByReferenceClassOps[G] { + this: TByReferenceClass[G] => +} diff --git a/src/col/vct/col/ast/type/TByValueClassImpl.scala b/src/col/vct/col/ast/type/TByValueClassImpl.scala new file mode 100644 index 0000000000..0f8e0f6bdc --- /dev/null +++ b/src/col/vct/col/ast/type/TByValueClassImpl.scala @@ -0,0 +1,8 @@ +package vct.col.ast.`type` + +import vct.col.ast.TByValueClass +import vct.col.ast.ops.TByValueClassOps + +trait TByValueClassImpl[G] extends TByValueClassOps[G] { + this: TByValueClass[G] => +} diff --git a/src/col/vct/col/ast/type/TClassImpl.scala b/src/col/vct/col/ast/type/TClassImpl.scala index 42a03d7983..1fd098e9c2 100644 --- a/src/col/vct/col/ast/type/TClassImpl.scala +++ b/src/col/vct/col/ast/type/TClassImpl.scala @@ -1,27 +1,23 @@ package vct.col.ast.`type` import vct.col.ast.{ - Applicable, Class, - ClassDeclaration, - Constructor, - ContractApplicable, InstanceField, - InstanceFunction, - InstanceMethod, - InstanceOperatorFunction, - InstanceOperatorMethod, + TByReferenceClass, + TByValueClass, TClass, Type, Variable, } -import vct.col.print.{Ctx, Doc, Empty, Group, Text} -import vct.col.ast.ops.TClassOps +import vct.col.print._ import vct.col.ref.Ref -import vct.result.VerificationError.Unreachable -trait TClassImpl[G] extends TClassOps[G] { +trait TClassImpl[G] { this: TClass[G] => + def cls: Ref[G, Class[G]] + + def typeArgs: Seq[Type[G]] + def transSupportArrowsHelper( seen: Set[TClass[G]] ): Seq[(TClass[G], TClass[G])] = @@ -45,7 +41,9 @@ trait TClassImpl[G] extends TClassOps[G] { def instantiate(t: Type[G]): Type[G] = this match { - case TClass(Ref(cls), typeArgs) if typeArgs.nonEmpty => + case TByReferenceClass(Ref(cls), typeArgs) if typeArgs.nonEmpty => + t.particularize(cls.typeArgs.zip(typeArgs).toMap) + case TByValueClass(Ref(cls), typeArgs) if typeArgs.nonEmpty => t.particularize(cls.typeArgs.zip(typeArgs).toMap) case _ => t } diff --git a/src/col/vct/col/ast/type/TNonNullPointerImpl.scala b/src/col/vct/col/ast/type/TNonNullPointerImpl.scala new file mode 100644 index 0000000000..cd769efa94 --- /dev/null +++ b/src/col/vct/col/ast/type/TNonNullPointerImpl.scala @@ -0,0 +1,16 @@ +package vct.col.ast.`type` + +import vct.col.ast.TNonNullPointer +import vct.col.ast.ops.TNonNullPointerOps +import vct.col.print._ + +trait TNonNullPointerImpl[G] extends TNonNullPointerOps[G] { + this: TNonNullPointer[G] => + override def layoutSplitDeclarator(implicit ctx: Ctx): (Doc, Doc) = { + val (spec, decl) = element.layoutSplitDeclarator + (spec, decl <> "*") + } + + override def layout(implicit ctx: Ctx): Doc = + Group(Text("NonNull") <> open <> element <> close) +} diff --git a/src/col/vct/col/ast/unsorted/ConstructorImpl.scala b/src/col/vct/col/ast/unsorted/ConstructorImpl.scala index af05d740ae..b21395c865 100644 --- a/src/col/vct/col/ast/unsorted/ConstructorImpl.scala +++ b/src/col/vct/col/ast/unsorted/ConstructorImpl.scala @@ -8,7 +8,7 @@ trait ConstructorImpl[G] extends ConstructorOps[G] { this: Constructor[G] => override def pure: Boolean = false override def returnType: TClass[G] = - TClass(cls, cls.decl.typeArgs.map((v: Variable[G]) => TVar(v.ref))) + cls.decl.classType(cls.decl.typeArgs.map((v: Variable[G]) => TVar(v.ref))) def layoutJava(implicit ctx: Ctx): Doc = Doc.stack(Seq( diff --git a/src/col/vct/col/origin/Blame.scala b/src/col/vct/col/origin/Blame.scala index 85c9cc182a..2620fd152d 100644 --- a/src/col/vct/col/origin/Blame.scala +++ b/src/col/vct/col/origin/Blame.scala @@ -158,22 +158,27 @@ case class AssignFieldFailed(node: SilverFieldAssign[_]) s"Insufficient permission for assignment `$source`." } -case class CopyStructFailed(node: Expr[_], field: String) - extends AssignFailed with NodeVerificationFailure { - override def code: String = "copyStructFailed" +case class CopyClassFailed(node: Node[_], clazz: ByValueClass[_], field: String) + extends PointerDerefError with NodeVerificationFailure { + override def code: String = "copyClassFailed" override def descInContext: String = - s"Insufficient read permission for field '$field' to copy struct." + s"Insufficient read permission for field '$field' to copy ${clazz.o + .find[TypeName].map(_.name).getOrElse("class")}." override def inlineDescWithSource(source: String): String = s"Insufficient permission for assignment `$source`." } -case class CopyStructFailedBeforeCall(node: Expr[_], field: String) - extends AssignFailed - with FrontendInvocationError +case class CopyClassFailedBeforeCall( + node: Node[_], + clazz: ByValueClass[_], + field: String, +) extends PointerDerefError + with InvocationFailure with NodeVerificationFailure { - override def code: String = "copyStructFailedBeforeCall" + override def code: String = "copyClassFailedBeforeCall" override def descInContext: String = - s"Insufficient read permission for field '$field' to copy struct before call." + s"Insufficient read permission for field '$field' to copy ${clazz.o + .find[TypeName].map(_.name).getOrElse("class")} before call." override def inlineDescWithSource(source: String): String = s"Insufficient permission for call `$source`." } @@ -1523,6 +1528,9 @@ object JavaArrayInitializerBlame "The explicit initialization of an array in Java should never generate an assignment that exceeds the bounds of the array" ) +object NonNullPointerNull + extends PanicBlame("A non-null pointer can never be null") + object UnsafeDontCare { case class Satisfiability(reason: String) extends UnsafeDontCare[NontrivialUnsatisfiable] diff --git a/src/col/vct/col/origin/Origin.scala b/src/col/vct/col/origin/Origin.scala index 987b16e1f4..fd9b9d993d 100644 --- a/src/col/vct/col/origin/Origin.scala +++ b/src/col/vct/col/origin/Origin.scala @@ -109,6 +109,9 @@ case class SourceName(name: String) extends NameStrategy { Some(SourceName.stringToName(name)) } +// Used to disambiguate whether to show a ByValueClass as a class or a struct +case class TypeName(name: String) extends OriginContent + /** Content that provides a bit of context here. By default, this assembles * further context from the remaining origin. contextHere and inlineContextHere * may optionally consume some more contents, otherwise they can just return diff --git a/src/col/vct/col/resolve/Resolve.scala b/src/col/vct/col/resolve/Resolve.scala index 9b4753bb3e..8ff29e8603 100644 --- a/src/col/vct/col/resolve/Resolve.scala +++ b/src/col/vct/col/resolve/Resolve.scala @@ -220,7 +220,12 @@ case object ResolveTypes { Spec.findModel(name, ctx) .getOrElse(throw NoSuchNameError("model", name, t)) ) - case t @ TClass(ref, _) => + case t @ TByReferenceClass(ref, _) => + ref.tryResolve(name => + Spec.findClass(name, ctx) + .getOrElse(throw NoSuchNameError("class", name, t)) + ) + case t @ TByValueClass(ref, _) => ref.tryResolve(name => Spec.findClass(name, ctx) .getOrElse(throw NoSuchNameError("class", name, t)) @@ -361,6 +366,7 @@ case object ResolveReferences extends LazyLogging { case CPPDeclarationStatement(decl) => Seq(decl) case JavaLocalDeclarationStatement(decl) => Seq(decl) case LocalDecl(v) => Seq(v) + case HeapLocalDecl(v) => Seq(v) case other => other.subnodes.flatMap(scanScope(ctx)) } @@ -641,7 +647,7 @@ case object ResolveReferences extends LazyLogging { case endpoint: PVLEndpoint[G] => endpoint.ref = Some( PVL.findConstructor( - TClass(endpoint.cls.decl.ref[Class[G]], Seq()), + TByReferenceClass(endpoint.cls.decl.ref[Class[G]], Seq()), Seq(), endpoint.args, ).getOrElse(throw ConstructorNotFound(endpoint)) diff --git a/src/col/vct/col/resolve/lang/Java.scala b/src/col/vct/col/resolve/lang/Java.scala index b65ced5463..1d734628a7 100644 --- a/src/col/vct/col/resolve/lang/Java.scala +++ b/src/col/vct/col/resolve/lang/Java.scala @@ -42,6 +42,7 @@ import vct.col.ast.{ TArray, TBag, TBool, + TByReferenceClass, TChar, TClass, TEnum, @@ -877,7 +878,7 @@ case object Java extends LazyLogging { case t: TFloat[G] => const(0) case TRational() => const(0) case TZFraction() => const(0) - case TClass(_, _) => Null() + case TByReferenceClass(_, _) => Null() case JavaTClass(_, _) => Null() case TEnum(_) => Null() case TAnyClass() => Null() diff --git a/src/col/vct/col/resolve/lang/PVL.scala b/src/col/vct/col/resolve/lang/PVL.scala index 9a8593e5a4..5de6ae8de2 100644 --- a/src/col/vct/col/resolve/lang/PVL.scala +++ b/src/col/vct/col/resolve/lang/PVL.scala @@ -13,8 +13,8 @@ case object PVL { args: Seq[Expr[G]], ): Option[PVLConstructorTarget[G]] = { t match { - case t @ TClass(Ref(cls), _) => - val resolvedCons = cls.decls.collectFirst { + case t: TClass[G] => + val resolvedCons = t.cls.decl.decls.collectFirst { case cons: PVLConstructor[G] if Util .compat(t.typeEnv, args, typeArgs, cons.args, cons.typeArgs) => @@ -23,7 +23,7 @@ case object PVL { args match { case Nil => - resolvedCons.orElse(Some(ImplicitDefaultPVLConstructor(cls))) + resolvedCons.orElse(Some(ImplicitDefaultPVLConstructor(t.cls.decl))) case _ => resolvedCons } case TModel(Ref(model)) if args.isEmpty => Some(RefModel(model)) @@ -69,7 +69,7 @@ case object PVL { ref.decl.declarations.flatMap(Referrable.from).collectFirst { case ref: RefModelField[G] if ref.name == name => ref } - case TClass(ref, _) => findDerefOfClass(ref.decl, name) + case t: TClass[G] => findDerefOfClass(t.cls.decl, name) case _ => Spec.builtinField(obj, name, blame) } @@ -94,8 +94,8 @@ case object PVL { case ref: RefModelAction[G] if ref.name == method => ref case ref: RefModelProcess[G] if ref.name == method => ref }.orElse(Spec.builtinInstanceMethod(obj, method, blame)) - case t @ TClass(ref, _) => - ref.decl.declarations.flatMap(Referrable.from).collectFirst { + case t: TClass[G] => + t.cls.decl.declarations.flatMap(Referrable.from).collectFirst { case ref: RefInstanceFunction[G] if ref.name == method && Util.compat(t.typeEnv, args, typeArgs, ref.decl) => diff --git a/src/col/vct/col/resolve/lang/Spec.scala b/src/col/vct/col/resolve/lang/Spec.scala index df62509925..52b6cd9a32 100644 --- a/src/col/vct/col/resolve/lang/Spec.scala +++ b/src/col/vct/col/resolve/lang/Spec.scala @@ -348,7 +348,11 @@ case object Spec { def findMethod[G](obj: Expr[G], name: String): Option[InstanceMethod[G]] = obj.t match { - case TClass(Ref(cls), _) => + case TByReferenceClass(Ref(cls), _) => + cls.decls.flatMap(Referrable.from).collectFirst { + case ref @ RefInstanceMethod(decl) if ref.name == name => decl + } + case TByValueClass(Ref(cls), _) => cls.decls.flatMap(Referrable.from).collectFirst { case ref @ RefInstanceMethod(decl) if ref.name == name => decl } @@ -360,7 +364,11 @@ case object Spec { name: String, ): Option[InstanceFunction[G]] = obj.t match { - case TClass(Ref(cls), _) => + case TByReferenceClass(Ref(cls), _) => + cls.decls.flatMap(Referrable.from).collectFirst { + case ref @ RefInstanceFunction(decl) if ref.name == name => decl + } + case TByValueClass(Ref(cls), _) => cls.decls.flatMap(Referrable.from).collectFirst { case ref @ RefInstanceFunction(decl) if ref.name == name => decl } @@ -372,7 +380,11 @@ case object Spec { name: String, ): Option[InstancePredicate[G]] = obj.t match { - case TClass(Ref(cls), _) => + case TByReferenceClass(Ref(cls), _) => + cls.decls.flatMap(Referrable.from).collectFirst { + case ref @ RefInstancePredicate(decl) if ref.name == name => decl + } + case TByValueClass(Ref(cls), _) => cls.decls.flatMap(Referrable.from).collectFirst { case ref @ RefInstancePredicate(decl) if ref.name == name => decl } @@ -385,7 +397,11 @@ case object Spec { def findField[G](obj: Expr[G], name: String): Option[InstanceField[G]] = obj.t match { - case TClass(Ref(cls), _) => + case TByReferenceClass(Ref(cls), _) => + cls.decls.flatMap(Referrable.from).collectFirst { + case ref @ RefField(decl) if ref.name == name => decl + } + case TByValueClass(Ref(cls), _) => cls.decls.flatMap(Referrable.from).collectFirst { case ref @ RefField(decl) if ref.name == name => decl } diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index 888e6a4708..f6e726230b 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -283,6 +283,7 @@ abstract class CoercingRewriter[Pre <: Generation]() case CoerceNullJavaClass(_) => e case CoerceNullAnyClass() => e case CoerceNullPointer(_) => e + case CoerceNonNullPointer(_) => e case CoerceFracZFrac() => e case CoerceZFracRat() => e case CoerceFloatRat(_) => e @@ -1247,6 +1248,8 @@ abstract class CoercingRewriter[Pre <: Generation]() case deref @ Deref(obj, ref) => Deref(cls(obj), ref)(deref.blame) case deref @ DerefHeapVariable(ref) => DerefHeapVariable(ref)(deref.blame) case deref @ DerefPointer(p) => DerefPointer(pointer(p)._1)(deref.blame) + case deref @ RawDerefPointer(p) => + RawDerefPointer(pointer(p)._1)(deref.blame) case Drop(xs, count) => Drop(seq(xs)._1, int(count)) case Empty(obj) => Empty(sized(obj)._1) case EmptyProcess() => EmptyProcess() @@ -1406,6 +1409,7 @@ abstract class CoercingRewriter[Pre <: Generation]() case LiteralTuple(ts, values) => LiteralTuple(ts, values.zip(ts).map { case (v, t) => coerce(v, t) }) case Local(ref) => Local(ref) + case HeapLocal(ref) => HeapLocal(ref) case LocalThreadId() => LocalThreadId() case MapCons(m, k, v) => val (coercedMap, mapType) = map(m) @@ -1554,6 +1558,8 @@ abstract class CoercingRewriter[Pre <: Generation]() NewArray(element, dims.map(int), moreDims, initialize)(na.blame) case na @ NewPointerArray(element, size) => NewPointerArray(element, size)(na.blame) + case na @ NewNonNullPointerArray(element, size) => + NewNonNullPointerArray(element, size)(na.blame) case NewObject(cls) => NewObject(cls) case NoPerm() => NoPerm() case Not(arg) => Not(bool(arg)) @@ -2178,7 +2184,6 @@ abstract class CoercingRewriter[Pre <: Generation]() givenMap, yields, ) => - val cls = TClass(ref.decl.cls, classTypeArgs) InvokeConstructor( ref, classTypeArgs, @@ -2228,6 +2233,7 @@ abstract class CoercingRewriter[Pre <: Generation]() case j @ Join(obj) => Join(cls(obj))(j.blame) case Label(decl, stat) => Label(decl, stat) case LocalDecl(local) => LocalDecl(local) + case HeapLocalDecl(local) => HeapLocalDecl(local) case l @ Lock(obj) => Lock(cls(obj))(l.blame) case Loop(init, cond, update, contract, body) => Loop(init, bool(cond), update, contract, body) @@ -2299,13 +2305,14 @@ abstract class CoercingRewriter[Pre <: Generation]() case rule: SimplificationRule[Pre] => new SimplificationRule[Pre](bool(rule.axiom)) case dataType: AxiomaticDataType[Pre] => dataType - case clazz: Class[Pre] => - new Class[Pre]( + case clazz: ByReferenceClass[Pre] => + new ByReferenceClass[Pre]( clazz.typeArgs, clazz.decls, clazz.supports, res(clazz.intrinsicLockInvariant), ) + case clazz: ByValueClass[Pre] => clazz case enum: Enum[Pre] => enum case enumConstant: EnumConstant[Pre] => enumConstant case model: Model[Pre] => model @@ -2424,6 +2431,7 @@ abstract class CoercingRewriter[Pre <: Generation]() case axiom: ADTAxiom[Pre] => new ADTAxiom[Pre](bool(axiom.axiom)) case function: ADTFunction[Pre] => function case variable: Variable[Pre] => variable + case variable: LocalHeapVariable[Pre] => variable case decl: LabelDecl[Pre] => decl case decl: SendDecl[Pre] => decl case decl: ParBlockDecl[Pre] => decl @@ -2570,7 +2578,9 @@ abstract class CoercingRewriter[Pre <: Generation]() // PB: types may very well contain expressions eventually, but for now they don't. def coerce(node: Type[Pre]): Type[Pre] = node match { - case t @ TClass(cls, args) => arity(TClass(cls, args)) + case t @ TByReferenceClass(cls, args) => + arity(TByReferenceClass(cls, args)) + case t @ TByValueClass(cls, args) => arity(TByValueClass(cls, args)) case _ => node } @@ -2664,6 +2674,7 @@ abstract class CoercingRewriter[Pre <: Generation]() ArrayLocation(array(arrayObj)._1, int(subscript))(a.blame) case p @ PointerLocation(pointerExp) => PointerLocation(pointer(pointerExp)._1)(p.blame) + case ByValueClassLocation(expr) => node case PredicateLocation(inv) => PredicateLocation(inv) case al @ AmbiguousLocation(expr) => AmbiguousLocation(expr)(al.blame) case patLoc @ InLinePatternLocation(loc, pat) => diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index 47295af0af..ca97d5ef3f 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -117,7 +117,7 @@ case object CoercionUtils { case (TNull(), TRef()) => CoerceNullRef() case (TNull(), TArray(target)) => CoerceNullArray(target) - case (TNull(), TClass(target, typeArgs)) => + case (TNull(), TByReferenceClass(target, typeArgs)) => CoerceNullClass(target, typeArgs) case (TNull(), JavaTClass(target, _)) => CoerceNullJavaClass(target) case (TNull(), TAnyClass()) => CoerceNullAnyClass() @@ -140,6 +140,12 @@ case object CoercionUtils { TPointer(element), ) => // if element == innerType => getAnyCoercion(element, innerType).getOrElse(return None) + case (TNonNullPointer(innerType), TPointer(element)) + if innerType == element => + CoerceNonNullPointer(innerType) + case (TNonNullPointer(a), TNonNullPointer(b)) + if getAnyCoercion(a, b).isDefined => + CoerceIdentity(target) case ( TPointer(element), CTPointer(innerType), @@ -211,16 +217,15 @@ case object CoercionUtils { CoercionSequence(Seq(CoerceUnboundInt(source, TInt()), CoerceIntRat())) case (_: IntType[G], TRational()) => CoerceIntRat() - case ( - source @ TClass(sourceClass, Seq()), - target @ TClass(targetClass, Seq()), - ) if source.transSupportArrows.exists { case (_, supp) => - supp.cls.decl == targetClass.decl - } => - CoerceSupports(sourceClass, targetClass) + case (source: TClass[G], target: TClass[G]) + if source.typeArgs.isEmpty && target.typeArgs.isEmpty && + source.transSupportArrows().exists { case (_, supp) => + supp.cls.decl == target.cls.decl + } => + CoerceSupports(source.cls, target.cls) - case (source @ TClass(sourceClass, typeArgs), TAnyClass()) => - CoerceClassAnyClass(sourceClass, typeArgs) + case (source: TClass[G], TAnyClass()) => + CoerceClassAnyClass(source.cls, source.typeArgs) case ( source @ JavaTClass(sourceClass, Nil), @@ -431,6 +436,8 @@ case object CoercionUtils { case t: TPointer[G] => Some((CoerceIdentity(source), t)) case t: CTPointer[G] => Some((CoerceIdentity(source), TPointer(t.innerType))) + case t: TNonNullPointer[G] => + Some((CoerceIdentity(source), TPointer(t.element))) case t: CTArray[G] => Some((CoerceCArrayPointer(t.innerType), TPointer(t.innerType))) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyPointerCoercion) @@ -442,6 +449,18 @@ case object CoercionUtils { case _ => None } + def firstElementIsType[G](aggregate: Type[G], innerType: Type[G]): Boolean = + aggregate match { + case aggregate if getAnyCoercion(aggregate, innerType).isDefined => true + case clazz: TByValueClass[G] => + clazz.cls.decl.decls.collectFirst { case field: InstanceField[G] => + firstElementIsType(field.t, innerType) + }.getOrElse(false) + case TArray(element) => firstElementIsType(element, innerType) + // TODO: Add LLVM types + case _ => false + } + def getAnyCArrayCoercion[G]( source: Type[G] ): Option[(Coercion[G], CTArray[G])] = diff --git a/src/col/vct/col/typerules/Types.scala b/src/col/vct/col/typerules/Types.scala index c06bdb2e45..2aa301264d 100644 --- a/src/col/vct/col/typerules/Types.scala +++ b/src/col/vct/col/typerules/Types.scala @@ -56,7 +56,7 @@ object Types { case (TType(left), TType(right)) => TType(leastCommonSuperType(left, right)) - case (left @ TClass(_, _), right @ TClass(_, _)) => + case (left: TClass[G], right: TClass[G]) => val leftArrows = left.transSupportArrows val rightArrows = right.transSupportArrows // Shared support are classes where there is an incoming left-arrow and right-arrow @@ -79,7 +79,7 @@ object Types { case other => TUnion(other) } - case (TClass(_, _), TAnyClass()) | (TAnyClass(), TClass(_, _)) => + case (_: TClass[G], TAnyClass()) | (TAnyClass(), _: TClass[G]) => TAnyClass() // TODO similar stuff for JavaClass diff --git a/src/col/vct/col/util/AstBuildHelpers.scala b/src/col/vct/col/util/AstBuildHelpers.scala index 6a7f1d29b3..80475a5e54 100644 --- a/src/col/vct/col/util/AstBuildHelpers.scala +++ b/src/col/vct/col/util/AstBuildHelpers.scala @@ -116,6 +116,12 @@ object AstBuildHelpers { SilverLocalAssign(new DirectRef(left), right) } + implicit class LocalHeapVarBuildHelpers[G](left: LocalHeapVariable[G]) { + def get(blame: Blame[PointerDerefError])( + implicit origin: Origin + ): DerefPointer[G] = DerefPointer(HeapLocal[G](new DirectRef(left)))(blame) + } + implicit class FieldBuildHelpers[G](left: SilverDeref[G]) { def <~(right: Expr[G])( implicit blame: Blame[AssignFailed], @@ -718,6 +724,13 @@ object AstBuildHelpers { )(implicit o: Origin): FunctionInvocation[G] = FunctionInvocation(ref, args, typeArgs, givenMap, yields)(blame) + def adtFunctionInvocation[G]( + ref: Ref[G, ADTFunction[G]], + typeArgs: Option[(Ref[G, AxiomaticDataType[G]], Seq[Type[G]])] = None, + args: Seq[Expr[G]] = Nil, + )(implicit o: Origin): ADTFunctionInvocation[G] = + ADTFunctionInvocation(typeArgs, ref, args) + def methodInvocation[G]( blame: Blame[InstanceInvocationFailure], obj: Expr[G], diff --git a/src/llvm/tools/vcllvm/VCLLVM.cpp b/src/llvm/tools/vcllvm/VCLLVM.cpp index af755ba71f..5cb289dc5b 100644 --- a/src/llvm/tools/vcllvm/VCLLVM.cpp +++ b/src/llvm/tools/vcllvm/VCLLVM.cpp @@ -26,12 +26,12 @@ col::Program sampleCol(bool returnBool) { // class col::GlobalDeclaration *classDeclaration = program.add_declarations(); - col::VctClass *vctClass = classDeclaration->mutable_vct_class(); - llvm2Col::setColNodeId(vctClass); - col::BooleanValue *lockInvariant = vctClass->mutable_intrinsic_lock_invariant()->mutable_boolean_value(); + col::ByReferenceClass *clazz = classDeclaration->mutable_by_reference_class(); + llvm2Col::setColNodeId(clazz); + col::BooleanValue *lockInvariant = clazz->mutable_intrinsic_lock_invariant()->mutable_boolean_value(); lockInvariant->set_value(true); // class>method - col::ClassDeclaration *methodDeclaration = vctClass->add_decls(); + col::ClassDeclaration *methodDeclaration = clazz->add_decls(); col::InstanceMethod *method = methodDeclaration->mutable_instance_method(); llvm2Col::setColNodeId(method); // class>method>return_type diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index fa0ac0c3bd..22058a0f81 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/src/main/vct/main/stages/Transformation.scala @@ -29,13 +29,16 @@ import vct.rewrite.adt.ImportSetCompat import vct.rewrite.{ DisambiguatePredicateExpression, EncodeAutoValue, + PrepareByValueClass, EncodeRange, EncodeResourceValues, ExplicitResourceValues, HeapVariableToRef, + LowerLocalHeapVariables, InlineTrivialLets, MonomorphizeClass, SmtlibToProverTypes, + VariableToPointer, GenerateSingleOwnerPermissions, } import vct.rewrite.lang.ReplaceSYCLTypes @@ -338,6 +341,8 @@ case class SilverTransformation( EncodeString, // Encode spec string as seq EncodeChar, CollectLocalDeclarations, // all decls in Scope +// EncodeByValueClass, + VariableToPointer, // should happen before ParBlockEncoder so it can distinguish between variables which can and can't altered in a parallel block DesugarPermissionOperators, // no PointsTo, \pointer, etc. ReadToValue, // resolve wildcard into fractional permission TrivialAddrOf, @@ -406,7 +411,7 @@ case class SilverTransformation( // flatten out functions in the rhs of assignments, making it harder to detect final field assignments where the // value is pure and therefore be put in the contract of the constant function. ConstantifyFinalFields, - + PrepareByValueClass, // Resolve side effects including method invocations, for encodetrythrowsignals. ResolveExpressionSideChecks, ResolveExpressionSideEffects, @@ -416,6 +421,7 @@ case class SilverTransformation( // No more classes ClassToRef, HeapVariableToRef, + LowerLocalHeapVariables, CheckContractSatisfiability.withArg(checkSat), DesugarCollectionOperators, EncodeNdIndex, diff --git a/src/parsers/vct/parsers/transform/PVLToCol.scala b/src/parsers/vct/parsers/transform/PVLToCol.scala index a4ecf4d03b..362831779f 100644 --- a/src/parsers/vct/parsers/transform/PVLToCol.scala +++ b/src/parsers/vct/parsers/transform/PVLToCol.scala @@ -159,7 +159,7 @@ case class PVLToCol[G]( withContract( contract, contract => { - new Class( + new ByReferenceClass( decls = decls.flatMap(convert(_)), supports = Nil, intrinsicLockInvariant = AstBuildHelpers diff --git a/src/parsers/vct/parsers/transform/systemctocol/colmodel/COLSystem.java b/src/parsers/vct/parsers/transform/systemctocol/colmodel/COLSystem.java index 018844b9ee..81987267e0 100644 --- a/src/parsers/vct/parsers/transform/systemctocol/colmodel/COLSystem.java +++ b/src/parsers/vct/parsers/transform/systemctocol/colmodel/COLSystem.java @@ -59,7 +59,7 @@ public class COLSystem { /** Constant empty list of signals clauses */ public final List> NO_SIGNALS; /** Constant empty list of class references */ - public final List>> NO_CLS_REFS; + public final List>> NO_CLS_REFS; /** Constant empty list of mappings from variable references to expressions */ public final List>, Expr>> NO_GIVEN; /** Constant empty list of mappings from expressions to variable references */ @@ -312,7 +312,7 @@ else if (size_expr instanceof SCVariableExpression var_expr && is_parameter(var_ /** * The Main class of the COL encoding. */ - private Class main; + private ByReferenceClass main; /** * The scheduler method in the Main class. @@ -373,7 +373,7 @@ else if (size_expr instanceof SCVariableExpression var_expr && is_parameter(var_ /** * A map from the intermediate representation of an intermediate representation class to its encoding in COL. */ - private final java.util.Map> col_class_translation; + private final java.util.Map> col_class_translation; /** * A map from SystemC class instances to the state class that is generated for them. Since each SystemC instance can @@ -536,7 +536,7 @@ public COLSystem() { this.NO_TYPES = List.from(CollectionConverters.asScala(no_types)); java.util.List> no_signals = java.util.List.of(); this.NO_SIGNALS = List.from(CollectionConverters.asScala(no_signals)); - java.util.List>> no_cls_refs = java.util.List.of(); + java.util.List>> no_cls_refs = java.util.List.of(); this.NO_CLS_REFS = List.from(CollectionConverters.asScala(no_cls_refs)); java.util.List>, Expr>> no_given = java.util.List.of(); this.NO_GIVEN = List.from(CollectionConverters.asScala(no_given)); @@ -563,7 +563,7 @@ public void create_vesuv_entry() { java.util.List> body = new java.util.ArrayList<>(); // Create variable of Main class - TClass main_type = new TClass<>(new DirectRef<>(main, ClassTag$.MODULE$.apply(Class.class)), Seqs.empty(), OriGen.create()); + TByReferenceClass main_type = new TByReferenceClass<>(new DirectRef<>(main, ClassTag$.MODULE$.apply(Class.class)), Seqs.empty(), OriGen.create()); Variable var = new Variable<>(main_type, OriGen.create("design")); // Constructor call @@ -602,7 +602,7 @@ public void add_enum(String enum_type_name) { * * @param main_cls Main class */ - public void set_main(Class main_cls) { + public void set_main(ByReferenceClass main_cls) { this.main = main_cls; } @@ -612,7 +612,7 @@ public void set_main(Class main_cls) { * * @return Main class of the encoded system */ - public Class get_main() { + public ByReferenceClass get_main() { return main; } @@ -831,7 +831,7 @@ public java.util.List get_processes(SCClassInstance sc_inst) { * @param col_class Intermediate representation class * @param translation Finalized COL class object */ - public void add_col_class_translation(COLClass col_class, Class translation) { + public void add_col_class_translation(COLClass col_class, ByReferenceClass translation) { this.col_class_translation.put(col_class, translation); } @@ -841,7 +841,7 @@ public void add_col_class_translation(COLClass col_class, Class translation) * @param col_class Intermediate representation class * @return Finalized COL class object */ - public Class get_col_class_translation(COLClass col_class) { + public ByReferenceClass get_col_class_translation(COLClass col_class) { return this.col_class_translation.get(col_class); } diff --git a/src/parsers/vct/parsers/transform/systemctocol/engine/ClassTransformer.java b/src/parsers/vct/parsers/transform/systemctocol/engine/ClassTransformer.java index b23134a1df..8e468d69d4 100644 --- a/src/parsers/vct/parsers/transform/systemctocol/engine/ClassTransformer.java +++ b/src/parsers/vct/parsers/transform/systemctocol/engine/ClassTransformer.java @@ -45,12 +45,12 @@ public ClassTransformer(COLSystem col_system) { * @param process Process class in intermediate representation * @return A COL class encoding the semantics of the given process class */ - public Class create_process_class(ProcessClass process) { + public ByReferenceClass create_process_class(ProcessClass process) { java.util.List> declarations = new java.util.ArrayList<>(); // Transform class attributes Ref> main_cls_ref = new LazyRef<>(col_system::get_main, Option.empty(), ClassTag$.MODULE$.apply(Class.class)); - InstanceField m = new InstanceField<>(new TClass<>(main_cls_ref, Seqs.empty(), OriGen.create()), col_system.NO_FLAGS, OriGen.create("m")); + InstanceField m = new InstanceField<>(new TByReferenceClass<>(main_cls_ref, Seqs.empty(), OriGen.create()), col_system.NO_FLAGS, OriGen.create("m")); declarations.add(m); col_system.add_class_main_ref(process, m); java.util.Map> fields = create_fields(process.get_generating_function(), process.get_methods(), @@ -75,7 +75,7 @@ public Class create_process_class(ProcessClass process) { // Add all newly generated methods to the declarations as well declarations.addAll(generated_instance_methods); - return new Class<>(Seqs.empty(), + return new ByReferenceClass<>(Seqs.empty(), List.from(CollectionConverters.asScala(declarations)), Seqs.empty(), col_system.TRUE, OriGen.create(create_name(process.get_generating_instance(), process.get_generating_function()))); } @@ -86,12 +86,12 @@ public Class create_process_class(ProcessClass process) { * @param state_class State class in intermediate representation * @return A COL class encoding the semantics of the given state class */ - public Class create_state_class(StateClass state_class) { + public ByReferenceClass create_state_class(StateClass state_class) { java.util.List> declarations = new java.util.ArrayList<>(); // Transform class attributes Ref> main_cls_ref = new LazyRef<>(col_system::get_main, Option.empty(), ClassTag$.MODULE$.apply(Class.class)); - InstanceField m = new InstanceField<>(new TClass<>(main_cls_ref, Seqs.empty(), OriGen.create()), col_system.NO_FLAGS, OriGen.create("m")); + InstanceField m = new InstanceField<>(new TByReferenceClass<>(main_cls_ref, Seqs.empty(), OriGen.create()), col_system.NO_FLAGS, OriGen.create("m")); declarations.add(m); col_system.add_class_main_ref(state_class, m); java.util.Map> fields = create_fields(null, state_class.get_methods(), @@ -126,7 +126,7 @@ public Class create_state_class(StateClass state_class) { // Add newly generated methods to declaration list declarations.addAll(generated_instance_methods); - return new Class<>(Seqs.empty(), + return new ByReferenceClass<>(Seqs.empty(), List.from(CollectionConverters.asScala(declarations)), Seqs.empty(), col_system.TRUE, OriGen.create(create_name(state_class.get_generating_instance()))); } diff --git a/src/parsers/vct/parsers/transform/systemctocol/engine/KnownTypeTransformer.java b/src/parsers/vct/parsers/transform/systemctocol/engine/KnownTypeTransformer.java index a6688fc107..f426bdae27 100644 --- a/src/parsers/vct/parsers/transform/systemctocol/engine/KnownTypeTransformer.java +++ b/src/parsers/vct/parsers/transform/systemctocol/engine/KnownTypeTransformer.java @@ -92,7 +92,7 @@ public void transform() { // Add channel field to COL system Ref> ref_to_cls = new DirectRef<>(cls, ClassTag$.MODULE$.apply(Class.class)); - col_system.add_primitive_channel(sc_inst, new InstanceField<>(new TClass<>(ref_to_cls, Seqs.empty(), OriGen.create()), col_system.NO_FLAGS, + col_system.add_primitive_channel(sc_inst, new InstanceField<>(new TByReferenceClass<>(ref_to_cls, Seqs.empty(), OriGen.create()), col_system.NO_FLAGS, OriGen.create(name.toLowerCase()))); } @@ -119,7 +119,7 @@ private String generate_class_name() { private Class transform_fifo(Origin o, Type t) { // Class fields Ref> main_cls_ref = new LazyRef<>(col_system::get_main, Option.empty(), ClassTag$.MODULE$.apply(Class.class)); - InstanceField m = new InstanceField<>(new TClass<>(main_cls_ref, Seqs.empty(), OriGen.create()), col_system.NO_FLAGS, OriGen.create("m")); + InstanceField m = new InstanceField<>(new TByReferenceClass<>(main_cls_ref, Seqs.empty(), OriGen.create()), col_system.NO_FLAGS, OriGen.create("m")); InstanceField buf = new InstanceField<>(new TSeq<>(t, OriGen.create()), col_system.NO_FLAGS, OriGen.create("buffer")); InstanceField nr_read = new InstanceField<>(col_system.T_INT, col_system.NO_FLAGS, OriGen.create("num_read")); InstanceField written = new InstanceField<>(new TSeq<>(t, OriGen.create()), col_system.NO_FLAGS, OriGen.create("written")); @@ -144,7 +144,7 @@ private Class transform_fifo(Origin o, Type t) { // Create the class java.util.List> declarations = java.util.List.of(m, buf, nr_read, written, constructor, fifo_read, fifo_write, fifo_update); - return new Class<>(Seqs.empty(), List.from(CollectionConverters.asScala(declarations)), Seqs.empty(), col_system.TRUE, o); + return new ByReferenceClass<>(Seqs.empty(), List.from(CollectionConverters.asScala(declarations)), Seqs.empty(), col_system.TRUE, o); } /** @@ -524,7 +524,7 @@ private InstanceMethod create_fifo_update_method(InstanceField m, Instance private Class transform_signal(Origin o, Type t) { // Class fields Ref> main_cls_ref = new LazyRef<>(col_system::get_main, Option.empty(), ClassTag$.MODULE$.apply(Class.class)); - InstanceField m = new InstanceField<>(new TClass<>(main_cls_ref, Seqs.empty(), OriGen.create()), col_system.NO_FLAGS, OriGen.create("m")); + InstanceField m = new InstanceField<>(new TByReferenceClass<>(main_cls_ref, Seqs.empty(), OriGen.create()), col_system.NO_FLAGS, OriGen.create("m")); InstanceField val = new InstanceField<>(t, col_system.NO_FLAGS, OriGen.create("val")); InstanceField _val = new InstanceField<>(t, col_system.NO_FLAGS, OriGen.create("_val")); @@ -545,7 +545,7 @@ private Class transform_signal(Origin o, Type t) { // Create the class java.util.List> class_content = java.util.List.of(m, val, _val, constructor, signal_read, signal_write, signal_update); - return new Class<>(Seqs.empty(), + return new ByReferenceClass<>(Seqs.empty(), List.from(CollectionConverters.asScala(class_content)), Seqs.empty(), col_system.TRUE, o); } diff --git a/src/parsers/vct/parsers/transform/systemctocol/engine/MainTransformer.java b/src/parsers/vct/parsers/transform/systemctocol/engine/MainTransformer.java index 334575a099..03f726b875 100644 --- a/src/parsers/vct/parsers/transform/systemctocol/engine/MainTransformer.java +++ b/src/parsers/vct/parsers/transform/systemctocol/engine/MainTransformer.java @@ -15,6 +15,7 @@ import scala.reflect.ClassTag$; import vct.col.ast.*; import vct.col.ast.Class; +import vct.col.ast.ByReferenceClass; import vct.col.ref.DirectRef; import vct.col.ref.LazyRef; import vct.col.ref.Ref; @@ -192,9 +193,9 @@ private void create_instances() { if (process_classes != null) { for (ProcessClass process_class : process_classes) { // Get field type - Class transformed_class = col_system.get_col_class_translation(process_class); - Ref> ref_to_class = new DirectRef<>(transformed_class, ClassTag$.MODULE$.apply(Class.class)); - Type t = new TClass<>(ref_to_class, Seqs.empty(), OriGen.create()); + ByReferenceClass transformed_class = col_system.get_col_class_translation(process_class); + Ref> ref_to_class = new DirectRef<>(transformed_class, ClassTag$.MODULE$.apply(ByReferenceClass.class)); + Type t = new TByReferenceClass<>(ref_to_class, Seqs.empty(), OriGen.create()); // Generate instance field InstanceField inst = new InstanceField<>(t, col_system.NO_FLAGS, OriGen.create(create_instance_name(process_class))); @@ -207,9 +208,9 @@ private void create_instances() { // Transform the state class for this instance, if there is any if (state_class != null) { // Get field type - Class transformed_class = col_system.get_col_class_translation(state_class); - Ref> ref_to_class = new DirectRef<>(transformed_class, ClassTag$.MODULE$.apply(Class.class)); - Type t = new TClass<>(ref_to_class, Seqs.empty(), OriGen.create()); + ByReferenceClass transformed_class = col_system.get_col_class_translation(state_class); + Ref> ref_to_class = new DirectRef<>(transformed_class, ClassTag$.MODULE$.apply(ByReferenceClass.class)); + Type t = new TByReferenceClass<>(ref_to_class, Seqs.empty(), OriGen.create()); // Generate instance field InstanceField inst = new InstanceField<>(t, col_system.NO_FLAGS, OriGen.create(create_instance_name(state_class))); @@ -1297,7 +1298,7 @@ private void assemble_main() { Expr lock_invariant = col_system.fold_preds(new InstancePredicateApply<>(col_system.THIS, global_invariant_ref, col_system.NO_EXPRS, OriGen.create())); // Assemble class - Class main_class = new Class<>(Seqs.empty(), List.from(CollectionConverters.asScala(declarations)), + ByReferenceClass main_class = new ByReferenceClass<>(Seqs.empty(), List.from(CollectionConverters.asScala(declarations)), Seqs.empty(), lock_invariant, OriGen.create("Main")); // Register Main class in COL system context diff --git a/src/parsers/vct/parsers/transform/systemctocol/engine/Transformer.java b/src/parsers/vct/parsers/transform/systemctocol/engine/Transformer.java index 4cfca17cae..34767dcc33 100644 --- a/src/parsers/vct/parsers/transform/systemctocol/engine/Transformer.java +++ b/src/parsers/vct/parsers/transform/systemctocol/engine/Transformer.java @@ -8,7 +8,7 @@ import de.tub.pes.syscir.sc_model.variables.SCEvent; import de.tub.pes.syscir.sc_model.variables.SCKnownType; import de.tub.pes.syscir.sc_model.variables.SCTIMEUNIT; -import vct.col.ast.Class; +import vct.col.ast.ByReferenceClass; import vct.col.ast.InstanceField; import vct.parsers.transform.systemctocol.exceptions.SystemCFormatException; import vct.parsers.transform.systemctocol.exceptions.UnsupportedException; @@ -324,14 +324,14 @@ private void transform_classes() { // Transform state class first, since process classes might call state class methods, but not the other way around if (state_cls != null) { - Class state_class = class_transformer.create_state_class(state_cls); + ByReferenceClass state_class = class_transformer.create_state_class(state_cls); col_system.add_global_declaration(state_class); col_system.add_col_class_translation(state_cls, state_class); } // Then transform all process classes for (ProcessClass process : col_system.get_processes(sc_inst)) { - Class process_class = class_transformer.create_process_class(process); + ByReferenceClass process_class = class_transformer.create_process_class(process); col_system.add_global_declaration(process_class); col_system.add_col_class_translation(process, process_class); } diff --git a/src/rewrite/vct/rewrite/CheckContractSatisfiability.scala b/src/rewrite/vct/rewrite/CheckContractSatisfiability.scala index 04f5e18c17..0f8b9ffe4a 100644 --- a/src/rewrite/vct/rewrite/CheckContractSatisfiability.scala +++ b/src/rewrite/vct/rewrite/CheckContractSatisfiability.scala @@ -97,23 +97,25 @@ case class CheckContractSatisfiability[Pre <: Generation]( val result = extractObj.extract(pred) val extractObj.Data(ts, in, _, _, _) = extractObj.finish() variables.scope { - globalDeclarations.declare(procedure( - blame = PanicBlame( - "The postcondition of a method checking satisfiability is empty" - ), - contractBlame = UnsafeDontCare.Satisfiability( - "the precondition of a check-sat method is only there to check it." - ), - requires = - UnitAccountedPredicate( - wellFormednessBlame.having(NotWellFormedIgnoreCheckSat(err)) { - dispatch(result) - } - )(result.o), - typeArgs = variables.dispatch(ts.keys), - args = variables.dispatch(in.keys), - body = Some(Scope[Post](Nil, Assert(ff)(onlyAssertBlame))), - )) + localHeapVariables.scope { + globalDeclarations.declare(procedure( + blame = PanicBlame( + "The postcondition of a method checking satisfiability is empty" + ), + contractBlame = UnsafeDontCare.Satisfiability( + "the precondition of a check-sat method is only there to check it." + ), + requires = + UnitAccountedPredicate( + wellFormednessBlame.having(NotWellFormedIgnoreCheckSat(err)) { + dispatch(result) + } + )(result.o), + typeArgs = variables.dispatch(ts.keys), + args = variables.dispatch(in.keys), + body = Some(Scope[Post](Nil, Assert(ff)(onlyAssertBlame))), + )) + } } } } diff --git a/src/rewrite/vct/rewrite/CheckProcessAlgebra.scala b/src/rewrite/vct/rewrite/CheckProcessAlgebra.scala index 87f378717b..a38730d7be 100644 --- a/src/rewrite/vct/rewrite/CheckProcessAlgebra.scala +++ b/src/rewrite/vct/rewrite/CheckProcessAlgebra.scala @@ -95,7 +95,7 @@ case class CheckProcessAlgebra[Pre <: Generation]() val newClass = currentModel.having(model) { - new Class( + new ByReferenceClass( Seq(), classDeclarations.collect { model.declarations.foreach(dispatch(_)) diff --git a/src/rewrite/vct/rewrite/ClassToRef.scala b/src/rewrite/vct/rewrite/ClassToRef.scala index eb9eba8428..bdb3f6e026 100644 --- a/src/rewrite/vct/rewrite/ClassToRef.scala +++ b/src/rewrite/vct/rewrite/ClassToRef.scala @@ -2,13 +2,13 @@ package vct.col.rewrite import vct.col.ast._ import vct.col.origin._ +import vct.result.VerificationError import vct.col.util.AstBuildHelpers._ import hre.util.ScopedStack import vct.col.rewrite.error.{ExcludedByPassOrder, ExtraNode} import vct.col.ref.Ref -import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} +import vct.col.resolve.ctx.Referrable import vct.col.util.SuccessionMap -import RewriteHelpers._ import scala.collection.mutable @@ -23,6 +23,12 @@ case object ClassToRef extends RewriterBuilder { private def InstanceOfOrigin: Origin = Origin(Seq(PreferredName(Seq("subtype")), LabelContext("classToRef"))) + private def ValueAdtOrigin: Origin = + Origin(Seq(PreferredName(Seq("Value")), LabelContext("classToRef"))) + + private def CastHelperOrigin: Origin = + Origin(Seq(LabelContext("classToRef cast helpers"))) + case class InstanceNullPreconditionFailed( inner: Blame[InstanceNull], inv: InvokingNode[_], @@ -30,6 +36,17 @@ case object ClassToRef extends RewriterBuilder { override def blame(error: PreconditionFailed): Unit = inner.blame(InstanceNull(inv)) } + + case class DerefFieldPointerBlame( + inner: Blame[InsufficientPermission], + node: HeapDeref[_], + clazz: ByValueClass[_], + field: String, + ) extends Blame[PointerDerefError] { + override def blame(error: PointerDerefError): Unit = { + inner.blame(InsufficientPermission(node)) + } + } } case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { @@ -38,11 +55,19 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { private def This: Origin = Origin(Seq(PreferredName(Seq("this")), LabelContext("classToRef"))) - val fieldSucc: SuccessionMap[Field[Pre], SilverField[Post]] = SuccessionMap() + val byRefFieldSucc: SuccessionMap[Field[Pre], SilverField[Post]] = + SuccessionMap() + val byValFieldSucc: SuccessionMap[Field[Pre], ADTFunction[Post]] = + SuccessionMap() + val byValClassSucc + : SuccessionMap[ByValueClass[Pre], AxiomaticDataType[Post]] = + SuccessionMap() val methodSucc: SuccessionMap[InstanceMethod[Pre], Procedure[Post]] = SuccessionMap() val consSucc: SuccessionMap[Constructor[Pre], Procedure[Post]] = SuccessionMap() + val byValConsSucc: SuccessionMap[ByValueClass[Pre], ADTFunction[Post]] = + SuccessionMap() val functionSucc: SuccessionMap[InstanceFunction[Pre], Function[Post]] = SuccessionMap() val predicateSucc: SuccessionMap[InstancePredicate[Pre], Predicate[Post]] = @@ -54,6 +79,15 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { val typeOf: SuccessionMap[Unit, Function[Post]] = SuccessionMap() val instanceOf: SuccessionMap[Unit, Function[Post]] = SuccessionMap() + val valueAdt: SuccessionMap[Unit, AxiomaticDataType[Post]] = SuccessionMap() + val valueAdtTypeArgument: Variable[Post] = + new Variable(TType(TAnyValue()))(ValueAdtOrigin.where(name = "V")) + val valueAsFunctions: mutable.Map[Type[Pre], ADTFunction[Post]] = mutable + .Map() + + val castHelpers: SuccessionMap[Type[Pre], Procedure[Post]] = SuccessionMap() + val requiredCastHelpers: ScopedStack[mutable.Set[Type[Pre]]] = ScopedStack() + def typeNumber(cls: Class[Pre]): Int = typeNumberStore.getOrElseUpdate(cls, typeNumberStore.size + 1) @@ -75,6 +109,27 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { ) } + private def transitiveByValuePermissions( + obj: Expr[Pre], + t: TByValueClass[Pre], + amount: Expr[Pre], + )(implicit o: Origin): Expr[Pre] = { + t.cls.decl.decls.collect[Expr[Pre]] { case field: InstanceField[Pre] => + field.t match { + case field_t: TByValueClass[Pre] => + fieldPerm[Pre](obj, field.ref, amount) &* + transitiveByValuePermissions( + Deref[Pre](obj, field.ref)(PanicBlame( + "Permission should already be ensured" + )), + field_t, + amount, + ) + case _ => fieldPerm(obj, field.ref, amount) + } + }.reduce[Expr[Pre]] { (a, b) => a &* b } + } + def makeInstanceOf: Function[Post] = { implicit val o: Origin = InstanceOfOrigin val sub = new Variable[Post](TInt()) @@ -101,15 +156,68 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { ) } + private def makeValueAdt: AxiomaticDataType[Post] = { + new AxiomaticDataType[Post]( + valueAsFunctions.values.toSeq, + Seq(valueAdtTypeArgument), + )(ValueAdtOrigin) + } + + // TODO: Also generate value as axioms for arrays once those are properly supported for C/CPP/LLVM + private def makeValueAsFunction( + typeName: String, + t: Type[Post], + ): ADTFunction[Post] = { + new ADTFunction[Post]( + Seq(new Variable(TVar[Post](valueAdtTypeArgument.ref))( + ValueAdtOrigin.where(name = "v") + )), + TNonNullPointer(t), + )(ValueAdtOrigin.where(name = "value_as_" + typeName)) + } + + private def unwrapValueAs( + axiomType: TAxiomatic[Post], + oldT: Type[Pre], + newT: Type[Post], + fieldRef: Ref[Post, ADTFunction[Post]], + )(implicit o: Origin): Seq[ADTAxiom[Post]] = { + (oldT match { + case t: TByValueClass[Pre] => { + // TODO: If there are no fields we should ignore the first field and add the axioms for the second field + t.cls.decl.decls.collectFirst({ case field: InstanceField[Pre] => + unwrapValueAs(axiomType, field.t, dispatch(field.t), fieldRef) + }).getOrElse(Nil) + } + case _ => Nil + }) :+ new ADTAxiom[Post](forall( + axiomType, + body = { a => + InlinePattern(adtFunctionInvocation[Post]( + valueAsFunctions + .getOrElseUpdate(oldT, makeValueAsFunction(oldT.toString, newT)) + .ref, + typeArgs = Some((valueAdt.ref(()), Seq(axiomType))), + args = Seq(a), + )) === Cast( + adtFunctionInvocation(fieldRef, args = Seq(a)), + TypeValue(TNonNullPointer(newT)), + ) + }, + )) + } + override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] = program.rewrite(declarations = globalDeclarations.collect { program.declarations.foreach(dispatch) - implicit val o: Origin = TypeOfOrigin typeOf(()) = makeTypeOf globalDeclarations.declare(typeOf(())) instanceOf(()) = makeInstanceOf globalDeclarations.declare(instanceOf(())) + if (valueAsFunctions.nonEmpty) { + globalDeclarations.declare(valueAdt.getOrElseUpdate((), makeValueAdt)) + } }._1 ) @@ -117,16 +225,17 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { decl match { case cls: Class[Pre] => if (cls.typeArgs.nonEmpty) - throw vct.result.VerificationError.Unreachable( + throw VerificationError.Unreachable( "Class type parameters should be encoded using monomorphization earlier" ) typeNumber(cls) - cls.drop() + + val thisType = dispatch(cls.classType(Nil)) cls.decls.foreach { case function: InstanceFunction[Pre] => implicit val o: Origin = function.o - val thisVar = new Variable[Post](TRef())(This) + val thisVar = new Variable[Post](thisType)(This) diz.having(thisVar.get) { functionSucc(function) = globalDeclarations .declare(labelDecls.scope { @@ -161,7 +270,7 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { } case method: InstanceMethod[Pre] => implicit val o: Origin = method.o - val thisVar = new Variable[Post](TRef())(This) + val thisVar = new Variable[Post](thisType)(This) diz.having(thisVar.get) { methodSucc(method) = globalDeclarations.declare(labelDecls.scope { new Procedure( @@ -197,7 +306,7 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { } case cons: Constructor[Pre] => implicit val o: Origin = cons.o - val thisVar = new Variable[Post](TRef())(This) + val thisVar = new Variable[Post](thisType)(This) consSucc(cons) = globalDeclarations.declare(labelDecls.scope { new Procedure( returnType = TVoid(), @@ -241,7 +350,7 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { )) }) case predicate: InstancePredicate[Pre] => - val thisVar = new Variable[Post](TRef())(This) + val thisVar = new Variable[Post](thisType)(This) diz.having(thisVar.get(predicate.o)) { predicateSucc(predicate) = globalDeclarations.declare( new Predicate( @@ -257,85 +366,338 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { ) } case field: Field[Pre] => - fieldSucc(field) = new SilverField(dispatch(field.t))(field.o) - globalDeclarations.declare(fieldSucc(field)) + if (cls.isInstanceOf[ByReferenceClass[Pre]]) { + byRefFieldSucc(field) = + new SilverField(dispatch(field.t))(field.o) + globalDeclarations.declare(byRefFieldSucc(field)) + } case _ => throw ExtraNode } - case decl => rewriteDefault(decl) + cls match { + case cls: ByValueClass[Pre] => + implicit val o: Origin = cls.o + val axiomType = TAxiomatic[Post](byValClassSucc.ref(cls), Nil) + var valueAsAxioms: Seq[ADTAxiom[Post]] = Seq() + val (fieldFunctions, fieldInverses, fieldTypes) = + cls.decls.collect { case field: Field[Pre] => + val newT = dispatch(field.t) + val nonnullT = TNonNullPointer(newT) + byValFieldSucc(field) = + new ADTFunction[Post]( + Seq(new Variable(axiomType)(field.o)), + nonnullT, + )(field.o) + if (valueAsAxioms.isEmpty) { + // This is the first field + valueAsAxioms = + valueAsAxioms :+ new ADTAxiom[Post](forall( + axiomType, + body = { a => + InlinePattern(adtFunctionInvocation[Post]( + valueAsFunctions.getOrElseUpdate( + field.t, + makeValueAsFunction(field.t.toString, newT), + ).ref, + typeArgs = Some((valueAdt.ref(()), Seq(axiomType))), + args = Seq(a), + )) === adtFunctionInvocation( + byValFieldSucc.ref(field), + args = Seq(a), + ) + }, + )) + + valueAsAxioms = + valueAsAxioms ++ + (field.t match { + case t: TByValueClass[Pre] => + // TODO: If there are no fields we should ignore the first field and add the axioms for the second field + t.cls.decl.decls + .collectFirst({ case innerF: InstanceField[Pre] => + unwrapValueAs( + axiomType, + innerF.t, + dispatch(innerF.t), + byValFieldSucc.ref(field), + ) + }).getOrElse(Nil) + case _ => Nil + }) + } + ( + byValFieldSucc(field), + new ADTFunction[Post]( + Seq(new Variable(nonnullT)(field.o)), + axiomType, + )( + field.o.copy( + field.o.originContents + .filterNot(_.isInstanceOf[SourceName]) + ).where(name = + "inv_" + field.o.find[SourceName].map(_.name) + .getOrElse("unknown") + ) + ), + nonnullT, + ) + }.unzip3 + val constructor = + new ADTFunction[Post]( + fieldTypes.zipWithIndex.map { case (t, i) => + new Variable(t)(Origin(Seq( + PreferredName(Seq("p_" + i)), + LabelContext("classToRef"), + ))) + }, + axiomType, + )( + cls.o.copy( + cls.o.originContents.filterNot(_.isInstanceOf[SourceName]) + ).where(name = + "new_" + cls.o.find[SourceName].map(_.name) + .getOrElse("unknown") + ) + ) + // TAnyValue is a placeholder the pointer adt doesn't have type parameters + val indexFunction = + new ADTFunction[Post]( + Seq(new Variable(TNonNullPointer(TAnyValue()))(Origin( + Seq(PreferredName(Seq("pointer")), LabelContext("classToRef")) + ))), + TInt(), + )( + cls.o.copy( + cls.o.originContents.filterNot(_.isInstanceOf[SourceName]) + ).where(name = + "index_" + cls.o.find[SourceName].map(_.name) + .getOrElse("unknown") + ) + ) + val injectivityAxiom = + new ADTAxiom[Post](foralls( + Seq(axiomType, axiomType), + body = { case Seq(a0, a1) => + foldAnd(fieldFunctions.map { f => + Implies( + Eq( + adtFunctionInvocation[Post](f.ref, args = Seq(a0)), + adtFunctionInvocation[Post](f.ref, args = Seq(a1)), + ), + a0 === a1, + ) + }) + }, + triggers = { case Seq(a0, a1) => + fieldFunctions.map { f => + Seq( + adtFunctionInvocation[Post](f.ref, None, args = Seq(a0)), + adtFunctionInvocation[Post](f.ref, None, args = Seq(a1)), + ) + } + }, + )) + val destructorAxioms = fieldFunctions.zip(fieldInverses).map { + case (f, inv) => + new ADTAxiom[Post](forall( + axiomType, + body = { a => + adtFunctionInvocation[Post]( + inv.ref, + None, + args = Seq( + adtFunctionInvocation[Post](f.ref, None, args = Seq(a)) + ), + ) === a + }, + triggers = { a => + Seq(Seq( + adtFunctionInvocation[Post](f.ref, None, args = Seq(a)) + )) + }, + )) + } + val indexAxioms = fieldFunctions.zipWithIndex.map { case (f, i) => + new ADTAxiom[Post](forall( + axiomType, + body = { a => + adtFunctionInvocation[Post]( + indexFunction.ref, + None, + args = Seq( + adtFunctionInvocation[Post](f.ref, None, args = Seq(a)) + ), + ) === const(i) + }, + triggers = { a => + Seq( + Seq(adtFunctionInvocation[Post](f.ref, None, args = Seq(a))) + ) + }, + )) + } + byValConsSucc(cls) = constructor + byValClassSucc(cls) = + new AxiomaticDataType[Post]( + Seq(indexFunction, injectivityAxiom) ++ destructorAxioms ++ + indexAxioms ++ fieldFunctions ++ fieldInverses ++ + valueAsAxioms, + Nil, + ) + globalDeclarations.succeed(cls, byValClassSucc(cls)) + case _ => cls.drop() + } + case decl => super.dispatch(decl) } def instantiate(cls: Class[Pre], target: Ref[Post, Variable[Post]])( implicit o: Origin ): Statement[Post] = { - Block(Seq( - SilverNewRef[Post]( - target, - cls.decls.collect { case field: InstanceField[Pre] => - fieldSucc.ref(field) - }, - ), - Inhale( - FunctionInvocation[Post]( - typeOf.ref(()), - Seq(Local(target)), + cls match { + case cls: ByReferenceClass[Pre] => + Block(Seq( + SilverNewRef[Post]( + target, + cls.decls.collect { case field: InstanceField[Pre] => + byRefFieldSucc.ref(field) + }, + ), + Inhale( + FunctionInvocation[Post]( + typeOf.ref(()), + Seq(Local(target)), + Nil, + Nil, + Nil, + )(PanicBlame("typeOf requires nothing.")) === const(typeNumber(cls)) + ), + )) + case _: ByValueClass[Pre] => throw ExtraNode + } + } + + private def addCastConstraints( + expr: Expr[Pre], + totalHelpers: mutable.Set[Type[Pre]], + ): Expr[Post] = { + val helpers: mutable.Set[Type[Pre]] = mutable.Set() + var result: Seq[Expr[Post]] = Nil + for (clause <- expr.unfoldStar) { + val newClause = requiredCastHelpers.having(helpers) { dispatch(clause) } + if (helpers.nonEmpty) { + result ++= helpers.map { t => + unwrapCastConstraints(dispatch(t), t)(CastHelperOrigin) + }.toSeq + totalHelpers.addAll(helpers) + helpers.clear() + } + result = result :+ newClause + } + foldStar(result)(expr.o) + } + + // For loops add cast helpers before and as an invariant (since otherwise the contract might not be well-formed) + override def dispatch(node: LoopContract[Pre]): LoopContract[Post] = { + val helpers: mutable.Set[Type[Pre]] = mutable.Set() + node match { + case inv @ LoopInvariant(invariant, decreases) => { + val result = + LoopInvariant( + addCastConstraints(invariant, helpers), + decreases.map(dispatch), + )(inv.blame)(node.o) + if (requiredCastHelpers.nonEmpty) { + requiredCastHelpers.top.addAll(helpers) + } + result + } +// case contract @ IterationContract( +// requires, +// ensures, +// context_everywhere, +// ) => { +// val result = +// IterationContract( +// addCastConstraints(requires, helpers), +// addCastConstraints(ensures, helpers), +// addCastConstraints(context_everywhere, helpers), +// )(contract.blame)(node.o) +// if (requiredCastHelpers.nonEmpty) { +// requiredCastHelpers.top.addAll(helpers) +// } +// result +// } + case _: IterationContract[Pre] => throw ExtraNode + } + } + + override def dispatch(stat: Statement[Pre]): Statement[Post] = { + val helpers: mutable.Set[Type[Pre]] = mutable.Set() + val result = + requiredCastHelpers.having(helpers) { + stat match { + case Instantiate(Ref(cls), Local(Ref(v))) => + instantiate(cls, succ(v))(stat.o) + case inv @ InvokeMethod( + obj, + Ref(method), + args, + outArgs, + typeArgs, + givenMap, + yields, + ) => + InvokeProcedure[Post]( + ref = methodSucc.ref(method), + args = dispatch(obj) +: args.map(dispatch), + outArgs = outArgs.map(dispatch), + typeArgs = typeArgs.map(dispatch), + givenMap = givenMap.map { case (Ref(v), e) => + (succ(v), dispatch(e)) + }, + yields = yields.map { case (e, Ref(v)) => (dispatch(e), succ(v)) }, + )(PreBlameSplit.left( + InstanceNullPreconditionFailed(inv.blame, inv), + PreBlameSplit + .left(PanicBlame("incorrect instance method type?"), inv.blame), + ))(inv.o) + case inv @ InvokeConstructor( + Ref(cons), + _, + out, + args, + outArgs, + typeArgs, + givenMap, + yields, + ) => + InvokeProcedure[Post]( + ref = consSucc.ref(cons), + args = args.map(dispatch), + outArgs = dispatch(out) +: outArgs.map(dispatch), + typeArgs = typeArgs.map(dispatch), + givenMap = givenMap.map { case (Ref(v), e) => + (succ(v), dispatch(e)) + }, + yields = yields.map { case (e, Ref(v)) => (dispatch(e), succ(v)) }, + )(inv.blame)(inv.o) + case other => super.dispatch(other) + } + } + + if (helpers.nonEmpty) { + Block(helpers.map { t => + InvokeProcedure[Post]( + castHelpers.getOrElseUpdate(t, makeCastHelper(t)).ref, Nil, Nil, Nil, - )(PanicBlame("typeOf requires nothing.")) === const(typeNumber(cls)) - ), - )) + Nil, + Nil, + )(TrueSatisfiable)(CastHelperOrigin) + }.toSeq :+ result)(stat.o) + } else { result } } - override def dispatch(stat: Statement[Pre]): Statement[Post] = - stat match { - case Instantiate(Ref(cls), Local(Ref(v))) => - instantiate(cls, succ(v))(stat.o) - case inv @ InvokeMethod( - obj, - Ref(method), - args, - outArgs, - typeArgs, - givenMap, - yields, - ) => - InvokeProcedure[Post]( - ref = methodSucc.ref(method), - args = dispatch(obj) +: args.map(dispatch), - outArgs = outArgs.map(dispatch), - typeArgs = typeArgs.map(dispatch), - givenMap = givenMap.map { case (Ref(v), e) => - (succ(v), dispatch(e)) - }, - yields = yields.map { case (e, Ref(v)) => (dispatch(e), succ(v)) }, - )(PreBlameSplit.left( - InstanceNullPreconditionFailed(inv.blame, inv), - PreBlameSplit - .left(PanicBlame("incorrect instance method type?"), inv.blame), - ))(inv.o) - case inv @ InvokeConstructor( - Ref(cons), - _, - out, - args, - outArgs, - typeArgs, - givenMap, - yields, - ) => - InvokeProcedure[Post]( - ref = consSucc.ref(cons), - args = args.map(dispatch), - outArgs = dispatch(out) +: outArgs.map(dispatch), - typeArgs = typeArgs.map(dispatch), - givenMap = givenMap.map { case (Ref(v), e) => - (succ(v), dispatch(e)) - }, - yields = yields.map { case (e, Ref(v)) => (dispatch(e), succ(v)) }, - )(inv.blame)(inv.o) - case other => rewriteDefault(other) - } - override def dispatch(node: ApplyAnyPredicate[Pre]): ApplyAnyPredicate[Post] = node match { case inv: InstancePredicateApply[Pre] => @@ -346,6 +708,69 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { case other => other.rewriteDefault() } + private def unwrapCastConstraints(outerType: Type[Post], t: Type[Pre])( + implicit o: Origin + ): Expr[Post] = { + val newT = dispatch(t) + val constraint = forall[Post]( + TNonNullPointer(outerType), + body = { p => + PolarityDependent( + Greater( + CurPerm(PointerLocation(p)(PanicBlame( + "Referring to a non-null pointer should not cause any verification failures" + ))), + NoPerm(), + ) ==> + (InlinePattern(Cast(p, TypeValue(TNonNullPointer(newT)))) === + adtFunctionInvocation( + valueAsFunctions + .getOrElseUpdate(t, makeValueAsFunction(t.toString, newT)) + .ref, + typeArgs = Some((valueAdt.ref(()), Seq(outerType))), + args = Seq(DerefPointer(p)(PanicBlame( + "Pointer deref is safe since the permission is framed" + ))), + )), + tt, + ) + }, + ) + + if (t.isInstanceOf[TByValueClass[Pre]]) { + constraint &* + t.asInstanceOf[TByValueClass[Pre]].cls.decl.decls.collectFirst { + case field: InstanceField[Pre] => + unwrapCastConstraints(outerType, field.t) + }.getOrElse(tt) + } else { constraint } + } + + private def makeCastHelper(t: Type[Pre]): Procedure[Post] = { + implicit val o: Origin = CastHelperOrigin + .where(name = "constraints_" + t.toString) + globalDeclarations.declare(procedure( + AbstractApplicable, + TrueSatisfiable, + ensures = UnitAccountedPredicate(unwrapCastConstraints(dispatch(t), t)), + )) + } + + private def addCastHelpers( + t: Type[Pre], + helpers: mutable.Set[Type[Pre]], + ): Unit = { + t match { + case cls: TByValueClass[Pre] => { + helpers.add(t) + cls.cls.decl.decls.collectFirst { case field: InstanceField[Pre] => + addCastHelpers(field.t, helpers) + } + } + case _ => + } + } + override def dispatch(e: Expr[Pre]): Expr[Post] = e match { case inv @ MethodInvocation( @@ -393,23 +818,52 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { .left(PanicBlame("incorrect instance function type?"), inv.blame), ))(inv.o) case ThisObject(_) => diz.top + case ptrOf @ AddrOf(Deref(obj, Ref(field))) + if obj.t.isInstanceOf[TByValueClass[Pre]] => + adtFunctionInvocation[Post]( + byValFieldSucc.ref(field), + args = Seq(dispatch(obj)), + )(ptrOf.o) case deref @ Deref(obj, Ref(field)) => - SilverDeref[Post](dispatch(obj), fieldSucc.ref(field))(deref.blame)( - deref.o - ) + obj.t match { + case _: TByReferenceClass[Pre] => + SilverDeref[Post](dispatch(obj), byRefFieldSucc.ref(field))( + deref.blame + )(deref.o) + case t: TByValueClass[Pre] => + DerefPointer( + adtFunctionInvocation[Post]( + byValFieldSucc.ref(field), + args = Seq(dispatch(obj)), + )(deref.o) + )(DerefFieldPointerBlame( + deref.blame, + deref, + t.cls.decl.asInstanceOf[ByValueClass[Pre]], + Referrable.originNameOrEmpty(field), + ))(deref.o) + } case TypeValue(t) => t match { - case TClass(Ref(cls), Seq()) => const(typeNumber(cls))(e.o) + case t: TClass[Pre] if t.typeArgs.isEmpty => + const(typeNumber(t.cls.decl))(e.o) + // Keep pointer casts intact for the adtPointer stage + case _: TPointer[Pre] | _: TNonNullPointer[Pre] => e.rewriteDefault() case other => ??? } case TypeOf(value) => - FunctionInvocation[Post]( - typeOf.ref(()), - Seq(dispatch(value)), - Nil, - Nil, - Nil, - )(PanicBlame("typeOf requires nothing"))(e.o) + value.t match { + case cls: TByReferenceClass[Pre] => + FunctionInvocation[Post]( + typeOf.ref(()), + Seq(dispatch(value)), + Nil, + Nil, + Nil, + )(PanicBlame("typeOf requires nothing"))(e.o) + case cls: TByValueClass[Pre] => + const[Post](typeNumber(cls.cls.decl))(e.o) + } case InstanceOf(value, TypeValue(TUnion(ts))) => implicit val o: Origin = e.o dispatch(foldOr(ts.map(t => InstanceOf(value, TypeValue(t))))) @@ -430,6 +884,14 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { Nil, Nil, )(PanicBlame("instanceOf requires nothing"))(e.o) + case Cast(value, typeValue) if value.t.asPointer.isDefined => { + // Keep pointer casts and add extra annotations + if (requiredCastHelpers.nonEmpty) { + addCastHelpers(value.t.asPointer.get.element, requiredCastHelpers.top) + } + + e.rewriteDefault() + } case Cast(value, typeValue) => dispatch( value @@ -464,22 +926,38 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { case v @ Value(PredicateLocation(inv: InstancePredicateApply[Pre])) => implicit val o: Origin = e.o Star[Post](v.rewrite(), dispatch(inv.obj) !== Null()) - case _ => rewriteDefault(e) + case _ => super.dispatch(e) } override def dispatch(t: Type[Pre]): Type[Post] = t match { - case TClass(_, _) => TRef() + case _: TByReferenceClass[Pre] => TRef() + case t: TByValueClass[Pre] => + TAxiomatic( + byValClassSucc.ref(t.cls.decl.asInstanceOf[ByValueClass[Pre]]), + Nil, + ) case TAnyClass() => TRef() - case t => rewriteDefault(t) + case t => super.dispatch(t) } override def dispatch(loc: Location[Pre]): Location[Post] = loc match { - case FieldLocation(obj, field) => - SilverFieldLocation[Post](dispatch(obj), fieldSucc.ref(field.decl))( - loc.o - ) - case default => rewriteDefault(default) + case FieldLocation(obj, Ref(field)) => + obj.t match { + case _: TByReferenceClass[Pre] => + SilverFieldLocation[Post](dispatch(obj), byRefFieldSucc.ref(field))( + loc.o + ) + case _: TByValueClass[Pre] => + PointerLocation[Post]( + adtFunctionInvocation[Post]( + byValFieldSucc.ref(field), + None, + args = Seq(dispatch(obj)), + )(loc.o) + )(NonNullPointerNull)(loc.o) + } + case default => super.dispatch(default) } } diff --git a/src/rewrite/vct/rewrite/ConstantifyFinalFields.scala b/src/rewrite/vct/rewrite/ConstantifyFinalFields.scala index 101046cbf5..3405775b89 100644 --- a/src/rewrite/vct/rewrite/ConstantifyFinalFields.scala +++ b/src/rewrite/vct/rewrite/ConstantifyFinalFields.scala @@ -80,12 +80,22 @@ case class ConstantifyFinalFields[Pre <: Generation]() extends Rewriter[Pre] { implicit val o: Origin = field.o if (isFinal(field)) { val `this` = - new Variable[Post](TClass( - succ(currentClass.top), - currentClass.top.typeArgs.map { v: Variable[Pre] => - TVar(succ(v)) - }, - )) + currentClass.top match { + case _: ByReferenceClass[Pre] => + new Variable[Post](TByReferenceClass( + succ(currentClass.top), + currentClass.top.typeArgs.map { v: Variable[Pre] => + TVar(succ(v)) + }, + )) + case _: ByValueClass[Pre] => + new Variable[Post](TByValueClass( + succ(currentClass.top), + currentClass.top.typeArgs.map { v: Variable[Pre] => + TVar(succ(v)) + }, + )) + } fieldFunction(field) = globalDeclarations .declare(withResult((result: Result[Post]) => function[Post]( diff --git a/src/rewrite/vct/rewrite/DisambiguateLocation.scala b/src/rewrite/vct/rewrite/DisambiguateLocation.scala index 085d57a9c3..f6e40c4f94 100644 --- a/src/rewrite/vct/rewrite/DisambiguateLocation.scala +++ b/src/rewrite/vct/rewrite/DisambiguateLocation.scala @@ -36,6 +36,10 @@ case class DisambiguateLocation[Pre <: Generation]() extends Rewriter[Pre] { implicit o: Origin ): Location[Post] = expr match { + case expr if expr.t.asPointer.isDefined => + PointerLocation(dispatch(expr))(blame) + case expr if expr.t.isInstanceOf[TByValueClass[Pre]] => + ByValueClassLocation(dispatch(expr))(blame) case DerefHeapVariable(ref) => HeapVariableLocation(succ(ref.decl)) case Deref(obj, ref) => FieldLocation(dispatch(obj), succ(ref.decl)) case ModelDeref(obj, ref) => ModelLocation(dispatch(obj), succ(ref.decl)) @@ -43,10 +47,7 @@ case class DisambiguateLocation[Pre <: Generation]() extends Rewriter[Pre] { SilverFieldLocation(dispatch(obj), succ(ref.decl)) case expr @ ArraySubscript(arr, index) => ArrayLocation(dispatch(arr), dispatch(index))(expr.blame) - case expr if expr.t.asPointer.isDefined => - PointerLocation(dispatch(expr))(blame) case PredicateApplyExpr(inv) => PredicateLocation(dispatch(inv)) - case InlinePattern(inner, pattern, group) => InLinePatternLocation( exprToLoc(inner, blame), diff --git a/src/rewrite/vct/rewrite/EncodeArrayValues.scala b/src/rewrite/vct/rewrite/EncodeArrayValues.scala index dcb8e47ab8..afc4a6b820 100644 --- a/src/rewrite/vct/rewrite/EncodeArrayValues.scala +++ b/src/rewrite/vct/rewrite/EncodeArrayValues.scala @@ -60,13 +60,15 @@ case object EncodeArrayValues extends RewriterBuilder { } } - case class PointerArrayCreationFailed(arr: NewPointerArray[_]) - extends Blame[InvocationFailure] { + case class PointerArrayCreationFailed( + arr: Expr[_], + blame: Blame[ArraySizeError], + ) extends Blame[InvocationFailure] { override def blame(error: InvocationFailure): Unit = error match { - case PreconditionFailed(_, _, _) => arr.blame.blame(ArraySize(arr)) + case PreconditionFailed(_, _, _) => blame.blame(ArraySize(arr)) case ContextEverywhereFailedInPre(_, _) => - arr.blame.blame(ArraySize(arr)) // Unnecessary? + blame.blame(ArraySize(arr)) // Unnecessary? case other => throw Unreachable(s"Invalid invocation failure: $other") } } @@ -106,6 +108,8 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { val pointerArrayCreationMethods: mutable.Map[Type[Pre], Procedure[Post]] = mutable.Map() + val nonNullPointerArrayCreationMethods + : mutable.Map[Type[Pre], Procedure[Post]] = mutable.Map() val freeMethods: mutable.Map[Type[ Post @@ -113,14 +117,15 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { .Map() def makeFree( - t: Type[Post] + t: Type[Pre], + newT: Type[Post], ): (Procedure[Post], FreePointer[Pre] => PointerFreeFailed[Pre]) = { implicit val o: Origin = freeFuncOrigin var errors: Seq[Expr[Pre] => PointerFreeError] = Seq() val proc = globalDeclarations.declare({ val (vars, ptr) = variables.collect { - val a_var = new Variable[Post](TPointer(t))(o.where(name = "p")) + val a_var = new Variable[Post](TPointer(newT))(o.where(name = "p")) variables.declare(a_var) Local[Post](a_var.ref) } @@ -166,15 +171,6 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { (p: Expr[Pre]) => PointerInsufficientFreePermission(p), ), ) - var requires = (ptr !== Null()) &* - (PointerBlockOffset(ptr)(FramedPtrBlockOffset) === zero) &* - makeStruct.makePerm( - i => - PointerLocation(PointerAdd(ptr, i.get)(FramedPtrOffset))( - FramedPtrOffset - ), - IteratedPtrInjective, - ) requiresT = if (!typeIsRef(t)) requiresT @@ -189,7 +185,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { // If structure contains structs, the permission for those fields need to be released as well val permFields = t match { - case t: TClass[Post] => unwrapStructPerm(access, t, o, makeStruct) + case t: TClass[Pre] => unwrapStructPerm(access, t, o, makeStruct) case _ => Seq() } requiresT = @@ -210,7 +206,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { body = None, requires = requiresPred, decreases = Some(DecreasesClauseNoRecursion[Post]()), - )(o.where("free_" + t.toString)) + )(o.where(name = "free_" + t.toString)) }) (proc, (node: FreePointer[Pre]) => PointerFreeFailed(node, errors)) } @@ -410,31 +406,26 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { def unwrapStructPerm( struct: Variable[Post] => Expr[Post], - structType: TClass[Post], + structType: TClass[Pre], origin: Origin, makeStruct: MakeAnns, - visited: Seq[TClass[Post]] = Seq(), + visited: Seq[TClass[Pre]] = Seq(), ): Seq[(Expr[Post], Expr[Pre] => PointerFreeError)] = { - if (visited.contains(structType)) - throw UnsupportedStructPerm( - origin - ) // We do not allow this notation for recursive structs + if (visited.contains(structType)) { + // We do not allow this notation for recursive structs + throw UnsupportedStructPerm(origin) + } implicit val o: Origin = origin - val fields = - structType match { - case TClass(ref, _) => - ref.decl.declarations.collect { case field: InstanceField[Post] => - field - } - case _ => Seq() - } + val fields = structType.cls.decl.declarations.collect { + case field: InstanceField[Pre] => field + } val newFieldPerms = fields.map(member => { val loc = - (i: Variable[Post]) => Deref[Post](struct(i), member.ref)(DerefPerm) + (i: Variable[Post]) => Deref[Post](struct(i), succ(member))(DerefPerm) var anns: Seq[(Expr[Post], Expr[Pre] => PointerFreeError)] = Seq(( makeStruct.makePerm( - i => FieldLocation[Post](struct(i), member.ref), + i => FieldLocation[Post](struct(i), succ(member)), IteratedPtrInjective, ), (p: Expr[Pre]) => @@ -453,7 +444,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { else anns member.t match { - case newStruct: TClass[Post] => + case newStruct: TClass[Pre] => // We recurse, since a field is another struct anns ++ unwrapStructPerm( loc, @@ -492,8 +483,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { val zero = const[Post](0) val pre1 = zero <= i.get && i.get < size val pre2 = zero <= j.get && j.get < size - val body = - (pre1 && pre2 && (i.get !== j.get)) ==> (access(i) !== access(j)) + val body = (pre1 && pre2 && access(i) === access(j)) ==> (i.get === j.get) Forall(Seq(i, j), Seq(triggerUnique), body) } } @@ -504,7 +494,10 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { case _ => false } - def makePointerCreationMethodFor(elementType: Type[Pre]) = { + def makePointerCreationMethodFor( + elementType: Type[Pre], + nullable: Boolean, + ) = { implicit val o: Origin = arrayCreationOrigin // ar != null // ar.length == dim0 @@ -520,6 +513,8 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { val j = new Variable[Post](TInt())(o.where(name = "j")) val access = (i: Variable[Post]) => PointerSubscript(result, i.get)(FramedPtrOffset) + val pointerAccess = + (i: Variable[Post]) => PointerAdd(result, i.get)(FramedPtrOffset) val makeStruct = MakeAnns( i, @@ -529,9 +524,11 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { Seq(access(i), access(j)), ) - var ensures = (result !== Null()) &* + var ensures = (PointerBlockLength(result)(FramedPtrBlockLength) === sizeArg.get) &* - (PointerBlockOffset(result)(FramedPtrBlockOffset) === zero) + (PointerBlockOffset(result)(FramedPtrBlockOffset) === zero) + + if (nullable) { ensures = (result !== Null()) &* ensures } // Pointer location needs pointer add, not pointer subscript ensures = ensures &* makeStruct.makePerm( @@ -547,9 +544,9 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { else { ensures &* makeStruct.makeUnique(access) } val permFields = - dispatch(elementType) match { - case t: TClass[Post] => unwrapStructPerm(access, t, o, makeStruct) - case _ => Seq() + elementType match { + case t: TClass[Pre] => unwrapStructPerm(access, t, o, makeStruct) + case _ => Nil } ensures = @@ -561,7 +558,9 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { procedure( blame = AbstractApplicable, contractBlame = TrueSatisfiable, - returnType = TPointer(dispatch(elementType)), + returnType = + if (nullable) { TPointer(dispatch(elementType)) } + else { TNonNullPointer(dispatch(elementType)) }, args = Seq(sizeArg), requires = UnitAccountedPredicate(requires), ensures = UnitAccountedPredicate(ensures), @@ -597,8 +596,23 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { Nil, )(ArrayCreationFailed(newArr)) case newPointerArr @ NewPointerArray(element, size) => - val method = pointerArrayCreationMethods - .getOrElseUpdate(element, makePointerCreationMethodFor(element)) + val method = pointerArrayCreationMethods.getOrElseUpdate( + element, + makePointerCreationMethodFor(element, nullable = true), + ) + ProcedureInvocation[Post]( + method.ref, + Seq(dispatch(size)), + Nil, + Nil, + Nil, + Nil, + )(PointerArrayCreationFailed(newPointerArr, newPointerArr.blame)) + case newPointerArr @ NewNonNullPointerArray(element, size) => + val method = nonNullPointerArrayCreationMethods.getOrElseUpdate( + element, + makePointerCreationMethodFor(element, nullable = false), + ) ProcedureInvocation[Post]( method.ref, Seq(dispatch(size)), @@ -606,15 +620,16 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { Nil, Nil, Nil, - )(PointerArrayCreationFailed(newPointerArr)) + )(PointerArrayCreationFailed(newPointerArr, newPointerArr.blame)) case free @ FreePointer(xs) => val newXs = dispatch(xs) val TPointer(t) = newXs.t - val (freeFunc, freeBlame) = freeMethods.getOrElseUpdate(t, makeFree(t)) + val (freeFunc, freeBlame) = freeMethods + .getOrElseUpdate(t, makeFree(xs.t.asPointer.get.element, t)) ProcedureInvocation[Post](freeFunc.ref, Seq(newXs), Nil, Nil, Nil, Nil)( freeBlame(free) )(free.o) - case other => rewriteDefault(other) + case other => super.dispatch(other) } } } diff --git a/src/rewrite/vct/rewrite/EncodeAutoValue.scala b/src/rewrite/vct/rewrite/EncodeAutoValue.scala index 0e2beaf27f..c9c71db2e5 100644 --- a/src/rewrite/vct/rewrite/EncodeAutoValue.scala +++ b/src/rewrite/vct/rewrite/EncodeAutoValue.scala @@ -179,31 +179,33 @@ case class EncodeAutoValue[Pre <: Generation]() extends Rewriter[Pre] { } case Let(binding, value, main) => variables.scope { - val top = conditionContext.pop() - val (b, v) = - try { (variables.dispatch(binding), dispatch(value)) } - finally { conditionContext.push(top) } - val mMap = mutable.ArrayBuffer[(Expr[Pre], Expr[Post])]() - val m = - conditionContext.having((conditionContext.top._1, mMap)) { - dispatch(main) - } - if (mMap.isEmpty) { Let(b, v, m) } - else { - mMap.foreach(postM => - conditionContext.top._2 - .append((Let(binding, value, postM._1), Let(b, v, postM._2))) - ) - conditionContext.top._1 match { - case InPrecondition() => Let(b, v, m) - case InPostcondition() => - Let( - b, - Old(v, None)(PanicBlame( - "Old should always be valid in a postcondition" - )), - m, - ) + localHeapVariables.scope { + val top = conditionContext.pop() + val (b, v) = + try { (variables.dispatch(binding), dispatch(value)) } + finally { conditionContext.push(top) } + val mMap = mutable.ArrayBuffer[(Expr[Pre], Expr[Post])]() + val m = + conditionContext.having((conditionContext.top._1, mMap)) { + dispatch(main) + } + if (mMap.isEmpty) { Let(b, v, m) } + else { + mMap.foreach(postM => + conditionContext.top._2 + .append((Let(binding, value, postM._1), Let(b, v, postM._2))) + ) + conditionContext.top._1 match { + case InPrecondition() => Let(b, v, m) + case InPostcondition() => + Let( + b, + Old(v, None)(PanicBlame( + "Old should always be valid in a postcondition" + )), + m, + ) + } } } } diff --git a/src/rewrite/vct/rewrite/EncodeForkJoin.scala b/src/rewrite/vct/rewrite/EncodeForkJoin.scala index 9284aafbd5..d41770483d 100644 --- a/src/rewrite/vct/rewrite/EncodeForkJoin.scala +++ b/src/rewrite/vct/rewrite/EncodeForkJoin.scala @@ -131,7 +131,13 @@ case class EncodeForkJoin[Pre <: Generation]() extends Rewriter[Pre] { implicit val o: Origin = e.o cls.decls.collectFirst { case run: RunMethod[Pre] => run } match { case Some(_) => - val obj = new Variable[Post](TClass(succ(cls), Seq())) + val obj = + cls match { + case _: ByReferenceClass[Pre] => + new Variable[Post](TByReferenceClass(succ(cls), Seq())) + case _: ByValueClass[Pre] => + new Variable[Post](TByValueClass(succ(cls), Seq())) + } ScopedExpr( Seq(obj), With( diff --git a/src/rewrite/vct/rewrite/EncodeIntrinsicLock.scala b/src/rewrite/vct/rewrite/EncodeIntrinsicLock.scala index e92c1b8b19..1cc1b3a7ab 100644 --- a/src/rewrite/vct/rewrite/EncodeIntrinsicLock.scala +++ b/src/rewrite/vct/rewrite/EncodeIntrinsicLock.scala @@ -85,7 +85,7 @@ case class EncodeIntrinsicLock[Pre <: Generation]() extends Rewriter[Pre] { def getClass(obj: Expr[Pre]): Class[Pre] = obj.t match { - case TClass(Ref(cls), _) => cls + case t: TClass[Pre] => t.cls.decl case _ => throw UnreachableAfterTypeCheck( "This argument is not a class type.", @@ -143,7 +143,7 @@ case class EncodeIntrinsicLock[Pre <: Generation]() extends Rewriter[Pre] { override def dispatch(decl: Declaration[Pre]): Unit = decl match { - case cls: Class[Pre] => + case cls: ByReferenceClass[Pre] => globalDeclarations.succeed( cls, cls.rewrite( diff --git a/src/rewrite/vct/rewrite/EncodeResourceValues.scala b/src/rewrite/vct/rewrite/EncodeResourceValues.scala index ca6436d11a..0c307bb3a2 100644 --- a/src/rewrite/vct/rewrite/EncodeResourceValues.scala +++ b/src/rewrite/vct/rewrite/EncodeResourceValues.scala @@ -184,7 +184,11 @@ case class EncodeResourceValues[Pre <: Generation]() case ResourcePattern.HeapVariableLocation(_) => Nil case ResourcePattern.FieldLocation(f) => nonGeneric(fieldOwner(f)) - Seq(TClass(succ(fieldOwner(f)), Seq())) + Seq(fieldOwner(f) match { + case cls: ByReferenceClass[Pre] => + TByReferenceClass(succ(cls), Seq()) + case cls: ByValueClass[Pre] => TByValueClass(succ(cls), Seq()) + }) case ResourcePattern.ModelLocation(f) => Seq(TModel(succ(modelFieldOwner(f)))) case ResourcePattern.SilverFieldLocation(_) => Seq(TRef()) @@ -196,8 +200,12 @@ case class EncodeResourceValues[Pre <: Generation]() ref.args.map(_.t).map(dispatch) case ResourcePattern.InstancePredicateLocation(ref) => nonGeneric(predicateOwner(ref)) - TClass[Post](succ(predicateOwner(ref)), Seq()) +: - ref.args.map(_.t).map(dispatch) + (predicateOwner(ref) match { + case cls: ByReferenceClass[Pre] => + TByReferenceClass(succ[Class[Post]](cls), Seq()) + case cls: ByValueClass[Pre] => + TByValueClass(succ[Class[Post]](cls), Seq()) + }) +: ref.args.map(_.t).map(dispatch) } def freeTypes(pattern: ResourcePattern): Seq[Type[Post]] = diff --git a/src/rewrite/vct/rewrite/ExtractInlineQuantifierPatterns.scala b/src/rewrite/vct/rewrite/ExtractInlineQuantifierPatterns.scala index a3341e5eb1..a039f7d600 100644 --- a/src/rewrite/vct/rewrite/ExtractInlineQuantifierPatterns.scala +++ b/src/rewrite/vct/rewrite/ExtractInlineQuantifierPatterns.scala @@ -106,50 +106,56 @@ case class ExtractInlineQuantifierPatterns[Pre <: Generation]() case f: Forall[Pre] => variables.scope { - val (patternsHere, body) = patterns.collect { - // We only want to inline lets that are defined inside the quantifier - letBindings.having(ScopedStack()) { dispatch(f.body) } + localHeapVariables.scope { + val (patternsHere, body) = patterns.collect { + // We only want to inline lets that are defined inside the quantifier + letBindings.having(ScopedStack()) { dispatch(f.body) } + } + val unsortedGroups = patternsHere.groupBy(_.group) + val sortedGroups = unsortedGroups.toSeq.sortBy(_._1).map(_._2) + val triggers = sortedGroups.map(_.map(_.make())) + Forall( + bindings = variables.collect { f.bindings.foreach(dispatch) }._1, + triggers = f.triggers.map(_.map(dispatch)) ++ triggers, + body = body, + )(f.o) } - val unsortedGroups = patternsHere.groupBy(_.group) - val sortedGroups = unsortedGroups.toSeq.sortBy(_._1).map(_._2) - val triggers = sortedGroups.map(_.map(_.make())) - Forall( - bindings = variables.collect { f.bindings.foreach(dispatch) }._1, - triggers = f.triggers.map(_.map(dispatch)) ++ triggers, - body = body, - )(f.o) } case f: Starall[Pre] => variables.scope { - val (patternsHere, body) = patterns.collect { - // We only want to inline lets that are defined inside the quantifier - letBindings.having(ScopedStack()) { dispatch(f.body) } + localHeapVariables.scope { + val (patternsHere, body) = patterns.collect { + // We only want to inline lets that are defined inside the quantifier + letBindings.having(ScopedStack()) { dispatch(f.body) } + } + val unsortedGroups = patternsHere.groupBy(_.group) + val sortedGroups = unsortedGroups.toSeq.sortBy(_._1).map(_._2) + val triggers = sortedGroups.map(_.map(_.make())) + Starall( + bindings = variables.collect { f.bindings.foreach(dispatch) }._1, + triggers = f.triggers.map(_.map(dispatch)) ++ triggers, + body = body, + )(f.blame)(f.o) } - val unsortedGroups = patternsHere.groupBy(_.group) - val sortedGroups = unsortedGroups.toSeq.sortBy(_._1).map(_._2) - val triggers = sortedGroups.map(_.map(_.make())) - Starall( - bindings = variables.collect { f.bindings.foreach(dispatch) }._1, - triggers = f.triggers.map(_.map(dispatch)) ++ triggers, - body = body, - )(f.blame)(f.o) } case f: Exists[Pre] => variables.scope { - val (patternsHere, body) = patterns.collect { - // We only want to inline lets that are defined inside the quantifier - letBindings.having(ScopedStack()) { dispatch(f.body) } + localHeapVariables.scope { + val (patternsHere, body) = patterns.collect { + // We only want to inline lets that are defined inside the quantifier + letBindings.having(ScopedStack()) { dispatch(f.body) } + } + val unsortedGroups = patternsHere.groupBy(_.group) + val sortedGroups = unsortedGroups.toSeq.sortBy(_._1).map(_._2) + val triggers = sortedGroups.map(_.map(_.make())) + Exists( + bindings = variables.collect { f.bindings.foreach(dispatch) }._1, + triggers = f.triggers.map(_.map(dispatch)) ++ triggers, + body = body, + )(f.o) } - val unsortedGroups = patternsHere.groupBy(_.group) - val sortedGroups = unsortedGroups.toSeq.sortBy(_._1).map(_._2) - val triggers = sortedGroups.map(_.map(_.make())) - Exists( - bindings = variables.collect { f.bindings.foreach(dispatch) }._1, - triggers = f.triggers.map(_.map(dispatch)) ++ triggers, - body = body, - )(f.o) } case other => rewriteDefault(other) diff --git a/src/rewrite/vct/rewrite/GenerateSingleOwnerPermissions.scala b/src/rewrite/vct/rewrite/GenerateSingleOwnerPermissions.scala index 29d24c34b1..24ba02e8ff 100644 --- a/src/rewrite/vct/rewrite/GenerateSingleOwnerPermissions.scala +++ b/src/rewrite/vct/rewrite/GenerateSingleOwnerPermissions.scala @@ -82,7 +82,7 @@ case class GenerateSingleOwnerPermissions[Pre <: Generation]( ), ) - case cls: Class[Pre] if enabled => + case cls: ByReferenceClass[Pre] if enabled => currentPerm.having(classPerm(cls)) { cls.rewriteDefault().succeed(cls) } case fun: InstanceFunction[Pre] if enabled => @@ -238,8 +238,8 @@ case class GenerateSingleOwnerPermissions[Pre <: Generation]( def resultPerm(app: ContractApplicable[Pre])(implicit o: Origin): Expr[Post] = transitivePerm(Result[Post](anySucc(app)), app.returnType) - def classPerm(cls: Class[Pre]): Expr[Post] = - transitivePerm(ThisObject[Post](succ(cls))(cls.o), TClass(cls.ref, Seq()))( + def classPerm(cls: ByReferenceClass[Pre]): Expr[Post] = + transitivePerm(ThisObject[Post](succ(cls))(cls.o), cls.classType(Seq()))( cls.o ) @@ -287,20 +287,22 @@ case class GenerateSingleOwnerPermissions[Pre <: Generation]( u, )), ) - case TClass(Ref(cls), _) if !generatingClasses.contains(cls) => - generatingClasses.having(cls) { - foldStar(cls.collect { case f: InstanceField[Pre] => + case t: TByReferenceClass[Pre] + if !generatingClasses.contains(t.cls.decl) => + generatingClasses.having(t.cls.decl) { + foldStar(t.cls.decl.collect { case f: InstanceField[Pre] => fieldTransitivePerm(e, f)(f.o) }) } - case TClass(Ref(cls), _) => + case t: TByReferenceClass[Pre] => // The class we are generating permission for has already been encountered when going through the chain // of fields. So we cut off the computation - if (!warnedClasses.contains(cls)) { + if (!warnedClasses.contains(t.cls.decl)) { logger.warn( - s"Not generating permissions for recursive occurrence of ${cls.o.getPreferredNameOrElse().ucamel}. Circular datastructures are not supported by permission generation" + s"Not generating permissions for recursive occurrence of ${t.cls + .decl.o.getPreferredNameOrElse().ucamel}. Circular datastructures are not supported by permission generation" ) - warnedClasses.addOne(cls) + warnedClasses.addOne(t.cls.decl) } tt case _ => tt @@ -311,7 +313,7 @@ case class GenerateSingleOwnerPermissions[Pre <: Generation]( ): Expr[Post] = { val left = fieldPerm[Post](`this`, succ(f), WritePerm()) f.t match { - case _: TClass[Pre] | _: TArray[Pre] => + case _: TByReferenceClass[Pre] | _: TArray[Pre] => left &* transitivePerm( Deref[Post](`this`, succ(f))(PanicBlame( "Permission for this field is already established" diff --git a/src/rewrite/vct/rewrite/LowerLocalHeapVariables.scala b/src/rewrite/vct/rewrite/LowerLocalHeapVariables.scala new file mode 100644 index 0000000000..9e3fdad2a7 --- /dev/null +++ b/src/rewrite/vct/rewrite/LowerLocalHeapVariables.scala @@ -0,0 +1,111 @@ +package vct.rewrite + +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} +import vct.col.ast.{Variable, _} +import vct.col.origin.{AssignLocalOk, LabelContext, Origin, PanicBlame} +import vct.col.util.AstBuildHelpers._ +import vct.col.ref.Ref +import vct.col.util.{CurrentRewriteProgramContext, SuccessionMap} +import vct.result.VerificationError + +case object LowerLocalHeapVariables extends RewriterBuilder { + override def key: String = "lowerLocalHeapVariables" + + override def desc: String = + "Lower LocalHeapVariables to Variables if their address is never taken" + + private val pointerCreationOrigin: Origin = Origin( + Seq(LabelContext("pointer creation method")) + ) +} + +case class LowerLocalHeapVariables[Pre <: Generation]() extends Rewriter[Pre] { + import LowerLocalHeapVariables._ + + private val stripped: SuccessionMap[LocalHeapVariable[Pre], Variable[Post]] = + SuccessionMap() + private val lowered: SuccessionMap[LocalHeapVariable[Pre], Variable[Post]] = + SuccessionMap() +// private val pointerCreationMethods: SuccessionMap[Type[Pre], Procedure[Post]] = SuccessionMap() +// +// def makePointerCreationMethod(t: Type[Pre]): Procedure[Post] = { +// implicit val o: Origin = pointerCreationOrigin +// +// val proc = globalDeclarations.declare(withResult((result: Result[Post]) => { +// +// })) +// } + + override def dispatch(program: Program[Pre]): Program[Post] = { + val dereferencedHeapLocals = program.collect { + case DerefPointer(hl @ HeapLocal(_)) => System.identityHashCode(hl) + } + val nakedHeapLocals = program.collect { + case hl @ HeapLocal(Ref(v)) + if !dereferencedHeapLocals.contains(System.identityHashCode(hl)) => + v + } + VerificationError.withContext(CurrentRewriteProgramContext(program)) { + localHeapVariables.scope { + variables.scope { + enumConstants.scope { + modelDeclarations.scope { + aDTDeclarations.scope { + classDeclarations.scope { + globalDeclarations.scope { + program.collect { + case HeapLocal(Ref(v)) if !nakedHeapLocals.contains(v) => + v + }.foreach(v => + stripped(v) = + new Variable[Post](dispatch(v.t.asPointer.get.element))( + v.o + ) + ) + Program(globalDeclarations.dispatch(program.declarations))( + dispatch(program.blame) + )(program.o) + } + } + } + } + } + } + } + } + } + + override def dispatch(node: Statement[Pre]): Statement[Post] = { + implicit val o: Origin = node.o + node match { + // Same logic as CollectLocalDeclarations + case Scope(vars, impl) => + val (newVars, newImpl) = variables.collect { + vars.foreach(dispatch) + dispatch(impl) + } + Scope(newVars, newImpl) + case HeapLocalDecl(v) => + if (stripped.contains(v)) { variables.declare(stripped(v)) } + else { + lowered(v) = new Variable[Post](dispatch(v.t))(v.o) + variables.declare(lowered(v)) + } + Block(Nil) + case _ => node.rewriteDefault() + } + } + + override def dispatch(node: Expr[Pre]): Expr[Post] = { + implicit val o: Origin = node.o + node match { + case DerefPointer(HeapLocal(Ref(v))) if stripped.contains(v) => + stripped(v).get + case HeapLocal(Ref(v)) if lowered.contains(v) => { + // lowered.contains(v) should always be true since all stripped HeapLocals would be caught by DerefPointer(HeapLocal(Ref(v))) + Local(lowered.ref(v)) + } + case _ => node.rewriteDefault() + } + } +} diff --git a/src/rewrite/vct/rewrite/MonomorphizeClass.scala b/src/rewrite/vct/rewrite/MonomorphizeClass.scala index 779fa700e4..dd91b27be4 100644 --- a/src/rewrite/vct/rewrite/MonomorphizeClass.scala +++ b/src/rewrite/vct/rewrite/MonomorphizeClass.scala @@ -82,9 +82,16 @@ case class MonomorphizeClass[Pre <: Generation]() globalDeclarations.scope { classDeclarations.scope { variables.scope { - allScopes.anyDeclare( - allScopes.anySucceedOnly(cls, cls.rewrite(typeArgs = Seq())) - ) + localHeapVariables.scope { + allScopes.anyDeclare(allScopes.anySucceedOnly( + cls, + cls match { + case cls: ByReferenceClass[Pre] => + cls.rewrite(typeArgs = Seq()) + case cls: ByValueClass[Pre] => cls.rewrite(typeArgs = Seq()) + }, + )) + } } } } @@ -130,14 +137,25 @@ case class MonomorphizeClass[Pre <: Generation]() override def dispatch(t: Type[Pre]): Type[Post] = (t, ctx.topOption) match { - case (TClass(Ref(cls), typeArgs), ctx) if typeArgs.nonEmpty => + case (TByReferenceClass(Ref(cls), typeArgs), ctx) if typeArgs.nonEmpty => + val typeValues = + ctx match { + case Some(ctx) => typeArgs.map(ctx.substitute.dispatch) + case None => typeArgs + } + instantiate(cls, typeValues, false) + TByReferenceClass[Post]( + genericSucc.ref[Post, Class[Post]](((cls, typeValues), cls)), + Seq(), + ) + case (TByValueClass(Ref(cls), typeArgs), ctx) if typeArgs.nonEmpty => val typeValues = ctx match { case Some(ctx) => typeArgs.map(ctx.substitute.dispatch) case None => typeArgs } instantiate(cls, typeValues, false) - TClass[Post]( + TByValueClass[Post]( genericSucc.ref[Post, Class[Post]](((cls, typeValues), cls)), Seq(), ) @@ -158,13 +176,13 @@ case class MonomorphizeClass[Pre <: Generation]() ) case inv: InvokeMethod[Pre] => inv.obj.t match { - case TClass(Ref(cls), typeArgs) if typeArgs.nonEmpty => - val typeValues = ctx.topOption.map(_.evalTypes(typeArgs)) - .getOrElse(typeArgs) - instantiate(cls, typeValues, false) + case t: TClass[Pre] if t.typeArgs.nonEmpty => + val typeValues = ctx.topOption.map(_.evalTypes(t.typeArgs)) + .getOrElse(t.typeArgs) + instantiate(t.cls.decl, typeValues, false) inv.rewrite(ref = genericSucc.ref[Post, InstanceMethod[Post]]( - ((cls, typeValues), inv.ref.decl) + ((t.cls.decl, typeValues), inv.ref.decl) ) ) case _ => inv.rewriteDefault() @@ -176,13 +194,14 @@ case class MonomorphizeClass[Pre <: Generation]() loc match { case loc @ FieldLocation(obj, Ref(field)) => obj.t match { - case TClass(Ref(cls), typeArgs) if typeArgs.nonEmpty => - val typeArgs1 = ctx.topOption.map(_.evalTypes(typeArgs)) - .getOrElse(typeArgs) - instantiate(cls, typeArgs1, false) + case t: TClass[Pre] if t.typeArgs.nonEmpty => + val typeArgs1 = ctx.topOption.map(_.evalTypes(t.typeArgs)) + .getOrElse(t.typeArgs) + instantiate(t.cls.decl, typeArgs1, false) loc.rewrite(field = - genericSucc - .ref[Post, InstanceField[Post]](((cls, typeArgs1), field)) + genericSucc.ref[Post, InstanceField[Post]]( + ((t.cls.decl, typeArgs1), field) + ) ) case _ => loc.rewriteDefault() } @@ -193,13 +212,14 @@ case class MonomorphizeClass[Pre <: Generation]() expr match { case deref @ Deref(obj, Ref(field)) => obj.t match { - case TClass(Ref(cls), typeArgs) if typeArgs.nonEmpty => - val typeArgs1 = ctx.topOption.map(_.evalTypes(typeArgs)) - .getOrElse(typeArgs) - instantiate(cls, typeArgs1, false) + case t: TClass[Pre] if t.typeArgs.nonEmpty => + val typeArgs1 = ctx.topOption.map(_.evalTypes(t.typeArgs)) + .getOrElse(t.typeArgs) + instantiate(t.cls.decl, typeArgs1, false) deref.rewrite(ref = - genericSucc - .ref[Post, InstanceField[Post]](((cls, typeArgs1), field)) + genericSucc.ref[Post, InstanceField[Post]]( + ((t.cls.decl, typeArgs1), field) + ) ) case _ => deref.rewriteDefault() } diff --git a/src/rewrite/vct/rewrite/MonomorphizeContractApplicables.scala b/src/rewrite/vct/rewrite/MonomorphizeContractApplicables.scala index 23012710f3..a7175b4b49 100644 --- a/src/rewrite/vct/rewrite/MonomorphizeContractApplicables.scala +++ b/src/rewrite/vct/rewrite/MonomorphizeContractApplicables.scala @@ -46,9 +46,11 @@ case class MonomorphizeContractApplicables[Pre <: Generation]() globalDeclarations.scope { classDeclarations.scope { variables.scope { - allScopes.anyDeclare( - allScopes.anySucceedOnly(app, app.rewrite(typeArgs = Nil)) - ) + localHeapVariables.scope { + allScopes.anyDeclare( + allScopes.anySucceedOnly(app, app.rewrite(typeArgs = Nil)) + ) + } } } } diff --git a/src/rewrite/vct/rewrite/ParBlockEncoder.scala b/src/rewrite/vct/rewrite/ParBlockEncoder.scala index 20d4c358af..c872c993a9 100644 --- a/src/rewrite/vct/rewrite/ParBlockEncoder.scala +++ b/src/rewrite/vct/rewrite/ParBlockEncoder.scala @@ -151,29 +151,31 @@ case class ParBlockEncoder[Pre <: Generation]() extends Rewriter[Pre] { scale(dispatch(e)) else variables.scope { - val range = quantVars.map(v => - from(v) <= Local[Post](succ(v)) && Local[Post](succ(v)) < to(v) - ).reduceOption[Expr[Post]](And(_, _)).getOrElse(tt) - - e match { - case Forall(bindings, Nil, body) => - Forall( - variables.dispatch(bindings ++ quantVars), - Nil, - range ==> scale(dispatch(body)), - )(body.o) - case s @ Starall(bindings, Nil, body) => - Starall( - variables.dispatch(bindings ++ quantVars), - Nil, - range ==> scale(dispatch(body)), - )(s.blame)(body.o) - case other => - Starall( - variables.dispatch(quantVars), - Nil, - range ==> scale(dispatch(other)), - )(ParBlockNotInjective(block, other))(other.o) + localHeapVariables.scope { + val range = quantVars.map(v => + from(v) <= Local[Post](succ(v)) && Local[Post](succ(v)) < to(v) + ).reduceOption[Expr[Post]](And(_, _)).getOrElse(tt) + + e match { + case Forall(bindings, Nil, body) => + Forall( + variables.dispatch(bindings ++ quantVars), + Nil, + range ==> scale(dispatch(body)), + )(body.o) + case s @ Starall(bindings, Nil, body) => + Starall( + variables.dispatch(bindings ++ quantVars), + Nil, + range ==> scale(dispatch(body)), + )(s.blame)(body.o) + case other => + Starall( + variables.dispatch(quantVars), + Nil, + range ==> scale(dispatch(other)), + )(ParBlockNotInjective(block, other))(other.o) + } } } }) diff --git a/src/rewrite/vct/rewrite/PrepareByValueClass.scala b/src/rewrite/vct/rewrite/PrepareByValueClass.scala new file mode 100644 index 0000000000..cee61769a6 --- /dev/null +++ b/src/rewrite/vct/rewrite/PrepareByValueClass.scala @@ -0,0 +1,334 @@ +package vct.rewrite + +import hre.util.ScopedStack +import vct.col.ast._ +import vct.col.origin._ +import vct.col.ref.Ref +import vct.col.resolve.ctx.Referrable +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} +import vct.col.util.AstBuildHelpers._ +import vct.col.util.SuccessionMap +import vct.result.VerificationError.{Unreachable, UserError} + +// TODO: Think of a better name +case object PrepareByValueClass extends RewriterBuilder { + override def key: String = "prepareByValueClass" + + override def desc: String = + "Initialise ByValueClasses when they are declared and copy them whenever they're read" + + private case class ClassCopyInAssignmentFailed( + blame: Blame[PointerDerefError], + assign: Node[_], + clazz: ByValueClass[_], + field: InstanceField[_], + ) extends Blame[InsufficientPermission] { + override def blame(error: InsufficientPermission): Unit = { + if (blame.isInstanceOf[PanicBlame]) { + assign.o + .blame(CopyClassFailed(assign, clazz, Referrable.originName(field))) + } else { + blame + .blame(CopyClassFailed(assign, clazz, Referrable.originName(field))) + } + } + } + + private case class ClassCopyInCallFailed( + blame: Blame[PointerDerefError], + inv: Invocation[_], + clazz: ByValueClass[_], + field: InstanceField[_], + ) extends Blame[InsufficientPermission] { + override def blame(error: InsufficientPermission): Unit = { + blame.blame( + CopyClassFailedBeforeCall(inv, clazz, Referrable.originName(field)) + ) + } + } + + case class UnsupportedStructPerm(o: Origin) extends UserError { + override def code: String = "unsupportedStructPerm" + override def text: String = + o.messageInContext( + "Shorthand for Permissions for structs not possible, since the struct has a cyclic reference" + ) + } + + private sealed class CopyContext + + private case class InCall(invocation: Invocation[_]) extends CopyContext + + private case class InAssignmentExpression(assignment: AssignExpression[_]) + extends CopyContext + + private case class InAssignmentStatement(assignment: Assign[_]) + extends CopyContext + + private case class NoCopy() extends CopyContext +} + +case class PrepareByValueClass[Pre <: Generation]() extends Rewriter[Pre] { + + import PrepareByValueClass._ + + private val inAssignment: ScopedStack[Unit] = ScopedStack() + private val copyContext: ScopedStack[CopyContext] = ScopedStack() + private val classCreationMethods + : SuccessionMap[TByValueClass[Pre], Procedure[Post]] = SuccessionMap() + + def makeClassCreationMethod(t: TByValueClass[Pre]): Procedure[Post] = { + implicit val o: Origin = t.cls.decl.o + + globalDeclarations.declare(withResult((result: Result[Post]) => + procedure[Post]( + blame = AbstractApplicable, + contractBlame = TrueSatisfiable, + returnType = dispatch(t), + ensures = UnitAccountedPredicate( + unwrapClassPerm(result, WritePerm(), t) + ), + decreases = Some(DecreasesClauseNoRecursion[Post]()), + ) + )) + } + + override def dispatch(node: Statement[Pre]): Statement[Post] = { + implicit val o: Origin = node.o + node match { + case HeapLocalDecl(local) + if local.t.asPointer.get.element.isInstanceOf[TByValueClass[Pre]] => { + val t = local.t.asPointer.get.element.asInstanceOf[TByValueClass[Pre]] + val newLocal = localHeapVariables.dispatch(local) + Block(Seq( + HeapLocalDecl(newLocal), +// Assign( +// HeapLocal[Post](newLocal.ref), +// NewNonNullPointerArray(t, const(1))(PanicBlame("Size > 0")), +// )(AssignLocalOk), + // TODO: Only do this if the first use does not overwrite it again (do something similar to what I implemented in ImportPointer).... + Assign( + newLocal.get(DerefAssignTarget), + procedureInvocation[Post]( + TrueSatisfiable, + classCreationMethods + .getOrElseUpdate(t, makeClassCreationMethod(t)).ref, + ), + )(AssignLocalOk), + )) + } + case assign: Assign[Pre] => + val target = inAssignment.having(()) { dispatch(assign.target) } + if (assign.target.t.isInstanceOf[TByValueClass[Pre]]) { + copyContext.having(InAssignmentStatement(assign)) { + assign.rewrite(target = target) + } + } else { assign.rewrite(target = target) } + case Instantiate(Ref(cls), out) + if cls.isInstanceOf[ByValueClass[Pre]] => { + // AssignLocalOk doesn't make too much sense since we don't know if out is a local + val t = TByValueClass[Pre](cls.ref, Seq()) + Assign[Post]( + dispatch(out), + procedureInvocation( + TrueSatisfiable, + classCreationMethods.getOrElseUpdate(t, makeClassCreationMethod(t)) + .ref, + ), + )(AssignLocalOk) + } + case _ => node.rewriteDefault() + } + } + + private def copyClassValue( + obj: Expr[Post], + t: TByValueClass[Pre], + blame: InstanceField[Pre] => Blame[InsufficientPermission], + ): Expr[Post] = { + implicit val o: Origin = obj.o + val ov = new Variable[Post](obj.t)(o.where(name = "original")) + val v = new Variable[Post](dispatch(t))(o.where(name = "copy")) + val children = t.cls.decl.decls.collect { case f: InstanceField[Pre] => + f.t match { + case inner: TByValueClass[Pre] => + Assign[Post]( + Deref[Post](v.get, succ(f))(DerefAssignTarget), + copyClassValue(Deref[Post](ov.get, succ(f))(blame(f)), inner, blame), + )(AssignLocalOk) + case _ => + Assign[Post]( + Deref[Post](v.get, succ(f))(DerefAssignTarget), + Deref[Post](ov.get, succ(f))(blame(f)), + )(AssignLocalOk) + + } + } + ScopedExpr( + Seq(ov, v), + Then( + With( + assignLocal(ov.get, obj), + PreAssignExpression( + v.get, + procedureInvocation[Post]( + TrueSatisfiable, + classCreationMethods + .getOrElseUpdate(t, makeClassCreationMethod(t)).ref, + ), + )(AssignLocalOk), + ), + Block(children), + ), + ) + } + + private def unwrapClassPerm( + obj: Expr[Post], + perm: Expr[Post], + structType: TByValueClass[Pre], + visited: Seq[TByValueClass[Pre]] = Seq(), + ): Expr[Post] = { + if (visited.contains(structType)) + throw UnsupportedStructPerm( + obj.o + ) // We do not allow this notation for recursive structs + implicit val o: Origin = obj.o + val blame = PanicBlame("Field permission is framed") + val fields = structType.cls.decl.decls.collect { + case f: InstanceField[Pre] => f + } + val newFieldPerms = fields.map(member => { + val loc = FieldLocation[Post](obj, succ(member)) + member.t match { + case inner: TByValueClass[Pre] => + Perm[Post](loc, perm) &* unwrapClassPerm( + Deref[Post](obj, succ(member))(blame), + perm, + inner, + structType +: visited, + ) + case _ => Perm(loc, perm) + } + }) + + foldStar(newFieldPerms) + } + + override def dispatch(node: Expr[Pre]): Expr[Post] = { + implicit val o: Origin = node.o + node match { + case NewObject(Ref(cls)) if cls.isInstanceOf[ByValueClass[Pre]] => { + val t = TByValueClass[Pre](cls.ref, Seq()) + procedureInvocation[Post]( + TrueSatisfiable, + classCreationMethods.getOrElseUpdate(t, makeClassCreationMethod(t)) + .ref, + ) + } + case _ => + } + if (inAssignment.nonEmpty) + node.rewriteDefault() + else + node match { + case Perm(ByValueClassLocation(e), p) => + unwrapClassPerm( + dispatch(e), + dispatch(p), + e.t.asInstanceOf[TByValueClass[Pre]], + ) + case Perm(pl @ PointerLocation(dhv @ DerefHeapVariable(Ref(v))), p) + if v.t.isInstanceOf[TNonNullPointer[Pre]] => + val t = v.t.asInstanceOf[TNonNullPointer[Pre]] + if (t.element.isInstanceOf[TByValueClass[Pre]]) { + val newV: Ref[Post, HeapVariable[Post]] = succ(v) + val newP = dispatch(p) + Perm(HeapVariableLocation(newV), newP) &* Perm( + PointerLocation(DerefHeapVariable(newV)(dhv.blame))(pl.blame), + newP, + ) + } else { node.rewriteDefault() } + case assign: PreAssignExpression[Pre] => + val target = inAssignment.having(()) { dispatch(assign.target) } + if (assign.target.t.isInstanceOf[TByValueClass[Pre]]) { + copyContext.having(InAssignmentExpression(assign)) { + assign.rewrite(target = target) + } + } else { + // No need for copy semantics in this context + copyContext.having(NoCopy()) { assign.rewrite(target = target) } + } + case invocation: Invocation[Pre] => + invocation.rewrite(args = invocation.args.map { a => + if (a.t.isInstanceOf[TByValueClass[Pre]]) { + copyContext.having(InCall(invocation)) { dispatch(a) } + } else { copyContext.having(NoCopy()) { dispatch(a) } } + }) + case dp @ DerefPointer(HeapLocal(Ref(v))) + if v.t.asPointer.get.element.isInstanceOf[TByValueClass[Pre]] => + rewriteInCopyContext( + dp, + v.t.asPointer.get.element.asInstanceOf[TByValueClass[Pre]], + ) + // TODO: Check for copy semantics in inappropriate places (i.e. when the user has made this a pointer) + case dp @ DerefPointer(DerefHeapVariable(Ref(v))) + if v.t.asPointer.get.element.isInstanceOf[TByValueClass[Pre]] => + rewriteInCopyContext( + dp, + v.t.asPointer.get.element.asInstanceOf[TByValueClass[Pre]], + ) + case deref @ Deref(_, Ref(f)) if f.t.isInstanceOf[TByValueClass[Pre]] => + if (copyContext.isEmpty) { deref.rewriteDefault() } + else { + // TODO: Improve blame message here + copyClassValue( + deref.rewriteDefault(), + f.t.asInstanceOf[TByValueClass[Pre]], + f => deref.blame, + ) + } + case dp @ DerefPointer(Local(Ref(v))) + if v.t.asPointer.get.element.isInstanceOf[TByValueClass[Pre]] => + // This can happen if the user specifies a local of type pointer to TByValueClass + rewriteInCopyContext( + dp, + v.t.asPointer.get.element.asInstanceOf[TByValueClass[Pre]], + ) + case _ => node.rewriteDefault() + } + } + + private def rewriteInCopyContext( + dp: DerefPointer[Pre], + t: TByValueClass[Pre], + ): Expr[Post] = { + if (copyContext.isEmpty) { + // If we are in other kinds of expressions like if statements + return dp.rewriteDefault() + } + val clazz = t.cls.decl.asInstanceOf[ByValueClass[Pre]] + + copyContext.top match { + case InCall(invocation) => + copyClassValue( + dp.rewriteDefault(), + t, + f => ClassCopyInCallFailed(dp.blame, invocation, clazz, f), + ) + case InAssignmentExpression(assignment) => + copyClassValue( + dp.rewriteDefault(), + t, + f => ClassCopyInAssignmentFailed(dp.blame, assignment, clazz, f), + ) + case InAssignmentStatement(assignment) => + copyClassValue( + dp.rewriteDefault(), + t, + f => ClassCopyInAssignmentFailed(dp.blame, assignment, clazz, f), + ) + case NoCopy() => dp.rewriteDefault() + } + } +} diff --git a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala index 008ab82b88..78af1351ef 100644 --- a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala +++ b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala @@ -340,6 +340,7 @@ case class ResolveExpressionSideEffects[Pre <: Generation]() ), ) case decl: LocalDecl[Pre] => rewriteDefault(decl) + case decl: HeapLocalDecl[Pre] => decl.rewriteDefault() case Return(result) => frame( result, @@ -528,6 +529,7 @@ case class ResolveExpressionSideEffects[Pre <: Generation]() val result = target match { case Local(Ref(v)) => Local[Post](succ(v))(target.o) + case HeapLocal(Ref(v)) => HeapLocal[Post](succ(v))(target.o) case deref @ DerefHeapVariable(Ref(v)) => DerefHeapVariable[Post](succ(v))(deref.blame)(target.o) case Deref(obj, Ref(f)) => @@ -680,7 +682,19 @@ case class ResolveExpressionSideEffects[Pre <: Generation]() givenMap, yields, ) => - val typ = TClass[Post](succ(cons.cls.decl), classTypeArgs.map(dispatch)) + val typ = + cons.cls.decl match { + case cls: ByReferenceClass[Pre] => + TByReferenceClass[Post]( + succ[Class[Post]](cls), + classTypeArgs.map(dispatch), + ) + case cls: ByValueClass[Pre] => + TByValueClass[Post]( + succ[Class[Post]](cls), + classTypeArgs.map(dispatch), + ) + } val res = new Variable[Post](typ)(ResultVar) variables.succeed(res.asInstanceOf[Variable[Pre]], res) effect( @@ -695,12 +709,25 @@ case class ResolveExpressionSideEffects[Pre <: Generation]() yields.map { case (e, Ref(v)) => (inlined(e), succ(v)) }, )(inv.blame)(e.o) ) - stored(res.get(SideEffectOrigin), TClass(cons.cls, classTypeArgs)) + stored( + res.get(SideEffectOrigin), + cons.cls.decl.classType(classTypeArgs), + ) case NewObject(Ref(cls)) => - val res = new Variable[Post](TClass(succ(cls), Seq()))(ResultVar) + val res = + cls match { + case cls: ByReferenceClass[Pre] => + new Variable[Post]( + TByReferenceClass(succ[Class[Post]](cls), Seq()) + )(ResultVar) + case cls: ByValueClass[Pre] => + new Variable[Post](TByValueClass(succ[Class[Post]](cls), Seq()))( + ResultVar + ) + } variables.succeed(res.asInstanceOf[Variable[Pre]], res) effect(Instantiate[Post](succ(cls), res.get(ResultVar))(e.o)) - stored(res.get(SideEffectOrigin), TClass(cls.ref, Seq())) + stored(res.get(SideEffectOrigin), cls.ref.decl.classType(Seq())) case other => stored(ReInliner().dispatch(rewriteDefault(other)), other.t) } } diff --git a/src/rewrite/vct/rewrite/SimplifyNestedQuantifiers.scala b/src/rewrite/vct/rewrite/SimplifyNestedQuantifiers.scala index 968cd7d6e4..b85541768e 100644 --- a/src/rewrite/vct/rewrite/SimplifyNestedQuantifiers.scala +++ b/src/rewrite/vct/rewrite/SimplifyNestedQuantifiers.scala @@ -225,6 +225,18 @@ case class SimplifyNestedQuantifiers[Pre <: Generation]() )(contract.blame)(contract.o) } + private def hasTriggers(e: Binder[Pre]): Boolean = + e match { + case Forall(_, triggers, body) => + triggers.exists(_.nonEmpty) || body.exists { + case InlinePattern(_, _, _) | InLinePatternLocation(_, _) => true + } + case Starall(_, triggers, body) => + triggers.exists(_.nonEmpty) || body.exists { + case InlinePattern(_, _, _) | InLinePatternLocation(_, _) => true + } + } + def rewriteLinearArray(e: Binder[Pre]): Option[Expr[Post]] = { val originalBody = e match { @@ -237,11 +249,7 @@ case class SimplifyNestedQuantifiers[Pre <: Generation]() return None // PB: do not attempt to reshape quantifiers that already have patterns - if ( - originalBody.exists { - case InlinePattern(_, _, _) | InLinePatternLocation(_, _) => true - } - ) { + if (hasTriggers(e)) { logger.debug(s"Not rewriting $e because it contains patterns") return None } diff --git a/src/rewrite/vct/rewrite/TrivialAddrOf.scala b/src/rewrite/vct/rewrite/TrivialAddrOf.scala index edc400f193..6cf0e2c060 100644 --- a/src/rewrite/vct/rewrite/TrivialAddrOf.scala +++ b/src/rewrite/vct/rewrite/TrivialAddrOf.scala @@ -37,9 +37,10 @@ case class TrivialAddrOf[Pre <: Generation]() extends Rewriter[Pre] { case AddrOf(sub @ PointerSubscript(p, i)) => PointerAdd(dispatch(p), dispatch(i))(SubscriptErrorAddError(sub))(e.o) + case AddrOf(Deref(_, _)) => e.rewriteDefault() case AddrOf(other) => throw UnsupportedLocation(other) case assign @ PreAssignExpression(target, AddrOf(value)) - if value.t.isInstanceOf[TClass[Pre]] => + if value.t.isInstanceOf[TByReferenceClass[Pre]] => implicit val o: Origin = assign.o val (newPointer, newTarget, newValue) = rewriteAssign( target, @@ -61,7 +62,7 @@ case class TrivialAddrOf[Pre <: Generation]() extends Rewriter[Pre] { override def dispatch(s: Statement[Pre]): Statement[Post] = s match { case assign @ Assign(target, AddrOf(value)) - if value.t.isInstanceOf[TClass[Pre]] => + if value.t.isInstanceOf[TByReferenceClass[Pre]] => implicit val o: Origin = assign.o val (newPointer, newTarget, newValue) = rewriteAssign( target, diff --git a/src/rewrite/vct/rewrite/VariableToPointer.scala b/src/rewrite/vct/rewrite/VariableToPointer.scala new file mode 100644 index 0000000000..6e8546627c --- /dev/null +++ b/src/rewrite/vct/rewrite/VariableToPointer.scala @@ -0,0 +1,220 @@ +package vct.rewrite + +import vct.col.ast._ +import vct.col.ref._ +import vct.col.origin._ +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} +import vct.col.util.AstBuildHelpers._ +import vct.col.util.SuccessionMap +import vct.result.VerificationError.UserError + +import scala.collection.mutable + +case object VariableToPointer extends RewriterBuilder { + override def key: String = "variableToPointer" + + override def desc: String = + "Translate every local and field to a pointer such that it can have its address taken" + + case class UnsupportedAddrOf(loc: Expr[_]) extends UserError { + override def code: String = "unsupportedAddrOf" + + override def text: String = + loc.o.messageInContext( + "Taking an address of this expression is not supported" + ) + } +} + +case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] { + + import VariableToPointer._ + + val addressedSet: mutable.Set[Node[Pre]] = new mutable.HashSet[Node[Pre]]() + val heapVariableMap: SuccessionMap[HeapVariable[Pre], HeapVariable[Post]] = + SuccessionMap() + val variableMap: SuccessionMap[Variable[Pre], Variable[Post]] = + SuccessionMap() + val fieldMap: SuccessionMap[InstanceField[Pre], InstanceField[Post]] = + SuccessionMap() + + override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] = { + // TODO: Replace the isInstanceOf[TByReferenceClass] checks with something that more clearly communicates that we want to exclude all reference types + addressedSet.addAll(program.collect { + case AddrOf(Local(Ref(v))) if !v.t.isInstanceOf[TByReferenceClass[Pre]] => + v + case AddrOf(DerefHeapVariable(Ref(v))) + if !v.t.isInstanceOf[TByReferenceClass[Pre]] => + v + case AddrOf(Deref(o, Ref(f))) + if !f.t.isInstanceOf[TByReferenceClass[Pre]] && + !o.t.isInstanceOf[TByValueClass[Pre]] => + f + }) + super.dispatch(program) + } + + override def dispatch(decl: Declaration[Pre]): Unit = + decl match { + // TODO: Use some sort of NonNull pointer type instead + case v: HeapVariable[Pre] if addressedSet.contains(v) => + heapVariableMap(v) = globalDeclarations + .succeed(v, new HeapVariable(TNonNullPointer(dispatch(v.t)))(v.o)) + case v: Variable[Pre] if addressedSet.contains(v) => + variableMap(v) = variables + .succeed(v, new Variable(TNonNullPointer(dispatch(v.t)))(v.o)) + case f: InstanceField[Pre] if addressedSet.contains(f) => + fieldMap(f) = classDeclarations.succeed( + f, + new InstanceField( + TNonNullPointer(dispatch(f.t)), + f.flags.map { it => dispatch(it) }, + )(f.o), + ) + case other => allScopes.anySucceed(other, other.rewriteDefault()) + } + + override def dispatch(stat: Statement[Pre]): Statement[Post] = { + implicit val o: Origin = stat.o + stat match { + case s: Scope[Pre] => + s.rewrite( + locals = variables.dispatch(s.locals), + body = Block(s.locals.filter { local => addressedSet.contains(local) } + .map { local => + implicit val o: Origin = local.o + Assign( + Local[Post](variableMap.ref(local)), + NewNonNullPointerArray( + variableMap(local).t.asPointer.get.element, + const(1), + )(PanicBlame("Size is > 0")), + )(PanicBlame("Initialisation should always succeed")) + } ++ Seq(dispatch(s.body))), + ) + case i @ Instantiate(cls, out) => + // TODO: Make sure that we recursively build newobject for byvalueclasses + // maybe get rid this entirely and only have it in encode by value class + Block(Seq(i.rewriteDefault()) ++ cls.decl.declarations.flatMap { + case f: InstanceField[Pre] => + if (f.t.asClass.isDefined) { + Seq( + Assign( + Deref[Post](dispatch(out), fieldMap.ref(f))(PanicBlame( + "Initialisation should always succeed" + )), + NewPointerArray( + fieldMap(f).t.asPointer.get.element, + const(1), + )(PanicBlame("Size is > 0")), + )(PanicBlame("Initialisation should always succeed")), + Assign( + PointerSubscript( + Deref[Post](dispatch(out), fieldMap.ref(f))(PanicBlame( + "Initialisation should always succeed" + )), + const[Post](0), + )(PanicBlame("Size is > 0")), + dispatch(NewObject[Pre](f.t.asClass.get.cls)), + )(PanicBlame("Initialisation should always succeed")), + ) + } else if (addressedSet.contains(f)) { + Seq( + Assign( + Deref[Post](dispatch(out), fieldMap.ref(f))(PanicBlame( + "Initialisation should always succeed" + )), + NewPointerArray( + fieldMap(f).t.asPointer.get.element, + const(1), + )(PanicBlame("Size is > 0")), + )(PanicBlame("Initialisation should always succeed")) + ) + } else { Seq() } + case _ => Seq() + }) + case other => other.rewriteDefault() + } + } + + override def dispatch(expr: Expr[Pre]): Expr[Post] = { + implicit val o: Origin = expr.o + expr match { + case deref @ DerefHeapVariable(Ref(v)) if addressedSet.contains(v) => + DerefPointer( + DerefHeapVariable[Post](heapVariableMap.ref(v))(deref.blame) + )(PanicBlame("Should always be accessible")) + case Local(Ref(v)) if addressedSet.contains(v) => + DerefPointer(Local[Post](variableMap.ref(v)))(PanicBlame( + "Should always be accessible" + )) + case deref @ Deref(obj, Ref(f)) if addressedSet.contains(f) => + DerefPointer(Deref[Post](dispatch(obj), fieldMap.ref(f))(deref.blame))( + PanicBlame("Should always be accessible") + ) + case newObject @ NewObject(Ref(cls)) => + val obj = new Variable[Post](TByReferenceClass(succ(cls), Seq())) + ScopedExpr( + Seq(obj), + With( + Block( + Seq(assignLocal(obj.get, newObject.rewriteDefault())) ++ + cls.declarations.flatMap { + case f: InstanceField[Pre] => + if (f.t.asClass.isDefined) { + Seq( + Assign( + Deref[Post](obj.get, anySucc(f))(PanicBlame( + "Initialisation should always succeed" + )), + dispatch(NewObject[Pre](f.t.asClass.get.cls)), + )(PanicBlame("Initialisation should always succeed")) + ) + } else if (addressedSet.contains(f)) { + Seq( + Assign( + Deref[Post](obj.get, fieldMap.ref(f))(PanicBlame( + "Initialisation should always succeed" + )), + NewPointerArray( + fieldMap(f).t.asPointer.get.element, + const(1), + )(PanicBlame("Size is > 0")), + )(PanicBlame("Initialisation should always succeed")) + ) + } else { Seq() } + case _ => Seq() + } + ), + obj.get, + ), + ) + case other => other.rewriteDefault() + } + } + + override def dispatch(loc: Location[Pre]): Location[Post] = { + implicit val o: Origin = loc.o + loc match { + case HeapVariableLocation(Ref(v)) if addressedSet.contains(v) => + PointerLocation( + DerefHeapVariable[Post](heapVariableMap.ref(v))(PanicBlame( + "Should always be accessible" + )) + )(PanicBlame("Should always be accessible")) + case FieldLocation(obj, Ref(f)) if addressedSet.contains(f) => + PointerLocation(Deref[Post](dispatch(obj), fieldMap.ref(f))(PanicBlame( + "Should always be accessible" + )))(PanicBlame("Should always be accessible")) + case PointerLocation(AddrOf(Deref(obj, Ref(f)))) + if addressedSet.contains(f) => + FieldLocation[Post](dispatch(obj), fieldMap.ref(f)) + case PointerLocation(AddrOf(DerefHeapVariable(Ref(v)))) + if addressedSet.contains(v) => + HeapVariableLocation[Post](heapVariableMap.ref(v)) + case PointerLocation(AddrOf(local @ Local(_))) => + throw UnsupportedAddrOf(local) + case other => other.rewriteDefault() + } + } +} diff --git a/src/rewrite/vct/rewrite/adt/ImportADT.scala b/src/rewrite/vct/rewrite/adt/ImportADT.scala index 444e9eae6c..2f7d73b34a 100644 --- a/src/rewrite/vct/rewrite/adt/ImportADT.scala +++ b/src/rewrite/vct/rewrite/adt/ImportADT.scala @@ -71,7 +71,7 @@ case object ImportADT { case TZFraction() => "zfract" case TMap(key, value) => "map$" + typeText(key) + "__" + typeText(value) + "$" - case TClass(Ref(cls), _) => cls.o.getPreferredNameOrElse().camel + case t: TClass[_] => t.cls.decl.o.getPreferredNameOrElse().camel case TVar(Ref(v)) => v.o.getPreferredNameOrElse().camel case TUnion(ts) => "union" + ts.map(typeText).mkString("$", "__", "$") case SilverPartialTAxiomatic(Ref(adt), _) => diff --git a/src/rewrite/vct/rewrite/adt/ImportOption.scala b/src/rewrite/vct/rewrite/adt/ImportOption.scala index 0ac9e05c37..8dd885426d 100644 --- a/src/rewrite/vct/rewrite/adt/ImportOption.scala +++ b/src/rewrite/vct/rewrite/adt/ImportOption.scala @@ -68,6 +68,19 @@ case class ImportOption[Pre <: Generation](importer: ImportADTImporter) case other => rewriteDefault(other) } + override def preCoerce(e: Expr[Pre]): Expr[Pre] = + e match { + case OptGet(OptSome(inner)) => inner + case OptGet(OptSomeTyped(_, inner)) => inner + case OptGetOrElse(OptSome(inner), _) => inner + case OptGetOrElse(OptSomeTyped(_, inner), _) => inner + case OptSomeTyped(t, OptGet(inner)) + if inner.t.asOption.get.element == t => + inner + case OptSome(OptGet(inner)) => inner + case _ => super.preCoerce(e) + } + override def postCoerce(e: Expr[Pre]): Expr[Post] = e match { case OptEmpty(opt) => diff --git a/src/rewrite/vct/rewrite/adt/ImportPointer.scala b/src/rewrite/vct/rewrite/adt/ImportPointer.scala index 2e81faf964..72b8432099 100644 --- a/src/rewrite/vct/rewrite/adt/ImportPointer.scala +++ b/src/rewrite/vct/rewrite/adt/ImportPointer.scala @@ -2,10 +2,12 @@ package vct.col.rewrite.adt import vct.col.ast._ import ImportADT.typeText +import hre.util.ScopedStack import vct.col.origin._ import vct.col.ref.Ref import vct.col.rewrite.Generation -import vct.col.util.AstBuildHelpers.{ExprBuildHelpers, const} +import vct.col.util.AstBuildHelpers.{functionInvocation, _} +import vct.col.util.SuccessionMap import scala.collection.mutable @@ -13,6 +15,14 @@ case object ImportPointer extends ImportADTBuilder("pointer") { private def PointerField(t: Type[_]): Origin = Origin(Seq(PreferredName(Seq(typeText(t))), LabelContext("pointer field"))) + private val PointerCreationOrigin: Origin = Origin( + Seq(LabelContext("adtPointer, pointer creation method")) + ) + + private val AsTypeOrigin: Origin = Origin( + Seq(LabelContext("classToRef, asType function")) + ) + case class PointerNullOptNone(inner: Blame[PointerNull], expr: Expr[_]) extends Blame[OptionNone] { override def blame(error: OptionNone): Unit = inner.blame(PointerNull(expr)) @@ -77,6 +87,77 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) val pointerField: mutable.Map[Type[Post], SilverField[Post]] = mutable.Map() + private val pointerCreationMethods + : SuccessionMap[Type[Pre], Procedure[Post]] = SuccessionMap() + + val asTypeFunctions: mutable.Map[Type[Pre], Function[Post]] = mutable.Map() + private val inAxiom: ScopedStack[Unit] = ScopedStack() + + private def makeAsTypeFunction(typeName: String): Function[Post] = { + val value = + new Variable[Post](TAxiomatic(pointerAdt.ref, Nil))( + AsTypeOrigin.where(name = "value") + ) + globalDeclarations.declare( + function[Post]( + AbstractApplicable, + TrueSatisfiable, + returnType = TAxiomatic(pointerAdt.ref, Nil), + args = Seq(value), + )(AsTypeOrigin.where(name = "as_" + typeName)) + ) + } + + private def makePointerCreationMethod(t: Type[Post]): Procedure[Post] = { + implicit val o: Origin = PointerCreationOrigin + .where(name = "create_nonnull_pointer_" + t.toString) + + val result = + new Variable[Post](TAxiomatic(pointerAdt.ref, Nil))(o.where(name = "res")) + globalDeclarations.declare(procedure[Post]( + blame = AbstractApplicable, + contractBlame = TrueSatisfiable, + returnType = TVoid(), + outArgs = Seq(result), + ensures = UnitAccountedPredicate( + (ADTFunctionInvocation[Post]( + typeArgs = Some((blockAdt.ref, Nil)), + ref = blockLength.ref, + args = Seq(ADTFunctionInvocation[Post]( + typeArgs = Some((pointerAdt.ref, Nil)), + ref = pointerBlock.ref, + args = Seq(result.get), + )), + ) === const(1)) &* + (ADTFunctionInvocation[Post]( + typeArgs = Some((pointerAdt.ref, Nil)), + ref = pointerOffset.ref, + args = Seq(result.get), + ) === const(0)) &* Perm( + SilverFieldLocation( + obj = + FunctionInvocation[Post]( + ref = pointerDeref.ref, + args = Seq(result.get), + typeArgs = Nil, + Nil, + Nil, + )(PanicBlame("ptr_deref requires nothing.")), + field = + pointerField.getOrElseUpdate( + t, { + globalDeclarations + .declare(new SilverField(t)(PointerField(t))) + }, + ).ref, + ), + WritePerm(), + ) + ), + decreases = Some(DecreasesClauseNoRecursion[Post]()), + )) + } + private def getPointerField(ptr: Expr[Pre]): Ref[Post, SilverField[Post]] = { val tElement = dispatch(ptr.t.asPointer.get.element) pointerField.getOrElseUpdate( @@ -87,44 +168,166 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) ).ref } + private def unwrapOption( + ptr: Expr[Pre], + blame: Blame[PointerNull], + ): Expr[Post] = { + ptr.t match { + case TPointer(_) => + OptGet(dispatch(ptr))(PointerNullOptNone(blame, ptr))(ptr.o) + case TNonNullPointer(_) => dispatch(ptr) + } + } + override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])( implicit o: Origin ): Expr[Post] = coercion match { case CoerceNullPointer(_) => OptNone() + case CoerceNonNullPointer(_) => OptSome(e) case other => super.applyCoercion(e, other) } + override def postCoerce(decl: Declaration[Pre]): Unit = { + decl match { + case axiom: ADTAxiom[Pre] => + inAxiom.having(()) { + allScopes.anySucceed(axiom, axiom.rewriteDefault()) + } + // TODO: This is an ugly way to exempt this one bit of generated code from having ptrAdd's added + case proc: Procedure[Pre] + if proc.o.find[LabelContext] + .exists(_.label == "classToRef cast helpers") => + inAxiom.having(()) { allScopes.anySucceed(proc, proc.rewriteDefault()) } + case _ => super.postCoerce(decl) + } + } + override def postCoerce(t: Type[Pre]): Type[Post] = t match { case TPointer(_) => TOption(TAxiomatic(pointerAdt.ref, Nil)) - case other => rewriteDefault(other) + case TNonNullPointer(_) => TAxiomatic(pointerAdt.ref, Nil) + case other => super.postCoerce(other) } - override def postCoerce(location: Location[Pre]): Location[Post] = + override def postCoerce(location: Location[Pre]): Location[Post] = { + implicit val o: Origin = location.o location match { case loc @ PointerLocation(pointer) => SilverFieldLocation( obj = FunctionInvocation[Post]( ref = pointerDeref.ref, - args = Seq( - OptGet(dispatch(pointer))( - PointerNullOptNone(loc.blame, pointer) - )(pointer.o) - ), + args = Seq(unwrapOption(pointer, loc.blame)), typeArgs = Nil, Nil, Nil, )(PanicBlame("ptr_deref requires nothing."))(pointer.o), field = getPointerField(pointer), - )(loc.o) + ) case other => rewriteDefault(other) } + } + + override def postCoerce(s: Statement[Pre]): Statement[Post] = { + implicit val o: Origin = s.o + s match { + case scope: Scope[Pre] => + scope.rewrite(body = Block(scope.locals.collect { + case v if v.t.isInstanceOf[TNonNullPointer[Pre]] => { + val firstUse = scope.body.collectFirst { + case l @ Local(Ref(variable)) if variable == v => l + } + if ( + firstUse.isDefined && scope.body.collectFirst { + case Assign(l @ Local(Ref(variable)), _) if variable == v => + System.identityHashCode(l) != + System.identityHashCode(firstUse.get) + }.getOrElse(true) + ) { + val oldT = v.t.asInstanceOf[TNonNullPointer[Pre]].element + val newT = dispatch(oldT) + Seq( + InvokeProcedure[Post]( + pointerCreationMethods + .getOrElseUpdate(oldT, makePointerCreationMethod(newT)).ref, + Nil, + Seq(Local(succ(v))), + Nil, + Nil, + Nil, + )(TrueSatisfiable) + ) + } else { Nil } + } + }.flatten :+ dispatch(scope.body))) + case _ => s.rewriteDefault() + } + } + + def rewriteTopLevelPointerSubscriptInTrigger(e: Expr[Pre]): Expr[Post] = { + implicit val o: Origin = e.o + e match { + case sub @ PointerSubscript(pointer, index) => + FunctionInvocation[Post]( + ref = pointerDeref.ref, + args = Seq( + FunctionInvocation[Post]( + ref = pointerAdd.ref, + args = Seq(unwrapOption(pointer, sub.blame), dispatch(index)), + typeArgs = Nil, + Nil, + Nil, + )(NoContext(PointerBoundsPreconditionFailed(sub.blame, index))) + ), + typeArgs = Nil, + Nil, + Nil, + )(PanicBlame("ptr_deref requires nothing.")) + case deref @ DerefPointer(pointer) => + FunctionInvocation[Post]( + ref = pointerDeref.ref, + args = Seq( + if ( + inAxiom.isEmpty && + !deref.o.find[LabelContext] + .exists(_.label == "classToRef cast helpers") + ) { + FunctionInvocation[Post]( + ref = pointerAdd.ref, + // Always index with zero, otherwise quantifiers with pointers do not get triggered + args = Seq(unwrapOption(pointer, deref.blame), const(0)), + typeArgs = Nil, + Nil, + Nil, + )(NoContext( + DerefPointerBoundsPreconditionFailed(deref.blame, pointer) + )) + } else { unwrapOption(pointer, deref.blame) } + ), + typeArgs = Nil, + Nil, + Nil, + )(PanicBlame("ptr_deref requires nothing.")) + case other => dispatch(other) + } + } override def postCoerce(e: Expr[Pre]): Expr[Post] = { implicit val o: Origin = e.o e match { + case f @ Forall(_, triggers, _) => + f.rewrite(triggers = + triggers.map(_.map(rewriteTopLevelPointerSubscriptInTrigger)) + ) + case s @ Starall(_, triggers, _) => + s.rewrite(triggers = + triggers.map(_.map(rewriteTopLevelPointerSubscriptInTrigger)) + ) + case e @ Exists(_, triggers, _) => + e.rewrite(triggers = + triggers.map(_.map(rewriteTopLevelPointerSubscriptInTrigger)) + ) case sub @ PointerSubscript(pointer, index) => SilverDeref( obj = @@ -133,12 +336,7 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) args = Seq( FunctionInvocation[Post]( ref = pointerAdd.ref, - args = Seq( - OptGet(dispatch(pointer))( - PointerNullOptNone(sub.blame, pointer) - ), - dispatch(index), - ), + args = Seq(unwrapOption(pointer, sub.blame), dispatch(index)), typeArgs = Nil, Nil, Nil, @@ -151,39 +349,40 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) field = getPointerField(pointer), )(PointerFieldInsufficientPermission(sub.blame, sub)) case add @ PointerAdd(pointer, offset) => - OptSome( + val inv = FunctionInvocation[Post]( ref = pointerAdd.ref, - args = Seq( - OptGet(dispatch(pointer))(PointerNullOptNone(add.blame, pointer)), - dispatch(offset), - ), + args = Seq(unwrapOption(pointer, add.blame), dispatch(offset)), typeArgs = Nil, Nil, Nil, )(NoContext(PointerBoundsPreconditionFailed(add.blame, pointer))) - ) + pointer.t match { + case TPointer(_) => OptSome(inv) + case TNonNullPointer(_) => inv + } case deref @ DerefPointer(pointer) => SilverDeref( obj = FunctionInvocation[Post]( ref = pointerDeref.ref, args = Seq( - FunctionInvocation[Post]( - ref = pointerAdd.ref, - // Always index with zero, otherwise quantifiers with pointers do not get triggered - args = Seq( - OptGet(dispatch(pointer))( - PointerNullOptNone(deref.blame, pointer) - ), - const(0), - ), - typeArgs = Nil, - Nil, - Nil, - )(NoContext( - DerefPointerBoundsPreconditionFailed(deref.blame, pointer) - )) + if ( + inAxiom.isEmpty && + !deref.o.find[LabelContext] + .exists(_.label == "classToRef cast helpers") + ) { + FunctionInvocation[Post]( + ref = pointerAdd.ref, + // Always index with zero, otherwise quantifiers with pointers do not get triggered + args = Seq(unwrapOption(pointer, deref.blame), const(0)), + typeArgs = Nil, + Nil, + Nil, + )(NoContext( + DerefPointerBoundsPreconditionFailed(deref.blame, pointer) + )) + } else { unwrapOption(pointer, deref.blame) } ), typeArgs = Nil, Nil, @@ -191,6 +390,31 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) )(PanicBlame("ptr_deref requires nothing.")), field = getPointerField(pointer), )(PointerFieldInsufficientPermission(deref.blame, deref)) + case deref @ RawDerefPointer(pointer) => + FunctionInvocation[Post]( + ref = pointerDeref.ref, + args = Seq( + if ( + inAxiom.isEmpty && + !deref.o.find[LabelContext] + .exists(_.label == "classToRef cast helpers") + ) { + FunctionInvocation[Post]( + ref = pointerAdd.ref, + // Always index with zero, otherwise quantifiers with pointers do not get triggered + args = Seq(unwrapOption(pointer, deref.blame), const(0)), + typeArgs = Nil, + Nil, + Nil, + )(NoContext( + DerefPointerBoundsPreconditionFailed(deref.blame, pointer) + )) + } else { unwrapOption(pointer, deref.blame) } + ), + typeArgs = Nil, + Nil, + Nil, + )(PanicBlame("ptr_deref requires nothing.")) case len @ PointerBlockLength(pointer) => ADTFunctionInvocation[Post]( typeArgs = Some((blockAdt.ref, Nil)), @@ -198,25 +422,84 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) args = Seq(ADTFunctionInvocation[Post]( typeArgs = Some((pointerAdt.ref, Nil)), ref = pointerBlock.ref, - args = Seq( - OptGet(dispatch(pointer))(PointerNullOptNone(len.blame, pointer)) - ), + args = Seq(unwrapOption(pointer, len.blame)), )), ) case off @ PointerBlockOffset(pointer) => ADTFunctionInvocation[Post]( typeArgs = Some((pointerAdt.ref, Nil)), ref = pointerOffset.ref, - args = Seq( - OptGet(dispatch(pointer))(PointerNullOptNone(off.blame, pointer)) - ), + args = Seq(unwrapOption(pointer, off.blame)), ) case pointerLen @ PointerLength(pointer) => postCoerce( PointerBlockLength(pointer)(pointerLen.blame) - PointerBlockOffset(pointer)(pointerLen.blame) ) - case other => rewriteDefault(other) + case Cast(value, typeValue) if value.t.asPointer.isDefined => + // TODO: Check if types are compatible + val targetType = typeValue.t.asInstanceOf[TType[Pre]].t + val innerType = targetType.asPointer.get.element + val newValue = dispatch(value) + (targetType, value.t) match { + case (TPointer(_), TPointer(_)) => + Select[Post]( + newValue === OptNone(), + OptNoneTyped(TAxiomatic(pointerAdt.ref, Nil)), + OptSome(applyAsTypeFunction( + innerType, + value, + OptGet(newValue)(PanicBlame( + "Can never be null since this is ensured in the conditional expression" + )), + )), + ) + case (TNonNullPointer(_), TPointer(_)) => + applyAsTypeFunction( + innerType, + value, + OptGet(newValue)(PanicBlame( + "Casting a pointer to a non-null pointer implies the pointer must be statically known to be non-null" + )), + ) + case (TPointer(_), TNonNullPointer(_)) => + OptSome(applyAsTypeFunction(innerType, value, newValue)) + case (TNonNullPointer(_), TNonNullPointer(_)) => + applyAsTypeFunction(innerType, value, newValue) + } + case other => super.postCoerce(other) } } + + private def applyAsTypeFunction( + innerType: Type[Pre], + preExpr: Expr[Pre], + postExpr: Expr[Post], + )(implicit o: Origin): Expr[Post] = { + functionInvocation[Post]( + PanicBlame("as_type requires nothing"), + asTypeFunctions + .getOrElseUpdate(innerType, makeAsTypeFunction(innerType.toString)).ref, + Seq(preExpr match { + case PointerAdd(_, _) => postExpr + // Don't add ptrAdd in an ADT axiom since we cannot use functions with preconditions there + case _ + if inAxiom.nonEmpty || + !preExpr.o.find[LabelContext] + .exists(_.label == "classToRef cast helpers") => + postExpr + case _ => + FunctionInvocation[Post]( + ref = pointerAdd.ref, + // Always index with zero, otherwise quantifiers with pointers do not get triggered + args = Seq(postExpr, const(0)), + typeArgs = Nil, + Nil, + Nil, + )(PanicBlame( + "Pointer out of bounds in pointer cast (no appropriate blame available)" + )) + }), + ) + } } diff --git a/src/rewrite/vct/rewrite/bip/EncodeBip.scala b/src/rewrite/vct/rewrite/bip/EncodeBip.scala index c859fdfdaf..6a3072c65e 100644 --- a/src/rewrite/vct/rewrite/bip/EncodeBip.scala +++ b/src/rewrite/vct/rewrite/bip/EncodeBip.scala @@ -407,7 +407,7 @@ case class EncodeBip[Pre <: Generation](results: VerificationResults) results.declare(component) implicit val o = DiagnosticOrigin val ref = succ[Class[Post]](classOf(constructor)) - val t = TClass[Post](ref, Seq()) + val t = TByReferenceClass[Post](ref, Seq()) rewritingBipConstructorBody.having(component) { constructorSucc(constructor) = globalDeclarations.declare( new Procedure[Post]( @@ -525,7 +525,7 @@ case class EncodeBip[Pre <: Generation](results: VerificationResults) transitions.flatMap { transition => val v = new Variable[Post]( - TClass(succ[Class[Post]](classOf(transition)), Seq()) + TByReferenceClass(succ[Class[Post]](classOf(transition)), Seq()) )(SynchronizationComponentVariableOrigin( synchronization, componentOf(transition), diff --git a/src/rewrite/vct/rewrite/cfg/Utils.scala b/src/rewrite/vct/rewrite/cfg/Utils.scala index d8da850cd9..2921e52a26 100644 --- a/src/rewrite/vct/rewrite/cfg/Utils.scala +++ b/src/rewrite/vct/rewrite/cfg/Utils.scala @@ -115,7 +115,11 @@ object Utils { } private def get_out_variable[G](cls: Ref[G, Class[G]], o: Origin): Local[G] = - Local(new DirectRef[G, Variable[G]](new Variable(TClass(cls, Seq()))(o)))(o) + Local( + new DirectRef[G, Variable[G]](new Variable(TByReferenceClass(cls, Seq()))( + o + )) + )(o) def find_all_cases[G]( body: Statement[G], diff --git a/src/rewrite/vct/rewrite/exc/EncodeBreakReturn.scala b/src/rewrite/vct/rewrite/exc/EncodeBreakReturn.scala index 3474e626f0..d4c146b3f1 100644 --- a/src/rewrite/vct/rewrite/exc/EncodeBreakReturn.scala +++ b/src/rewrite/vct/rewrite/exc/EncodeBreakReturn.scala @@ -130,7 +130,9 @@ case class EncodeBreakReturn[Pre <: Generation]() extends Rewriter[Pre] { after = Block(Nil), catches = Seq(CatchClause( decl = - new Variable(TClass(breakLabelException.ref(decl), Seq())), + new Variable( + TByReferenceClass(breakLabelException.ref(decl), Seq()) + ), body = Block(Nil), )), ) @@ -147,8 +149,9 @@ case class EncodeBreakReturn[Pre <: Generation]() extends Rewriter[Pre] { case Break(Some(Ref(label))) => val cls = breakLabelException.getOrElseUpdate( label, - globalDeclarations - .declare(new Class[Post](Nil, Nil, Nil, tt)(BreakException)), + globalDeclarations.declare( + new ByReferenceClass[Post](Nil, Nil, Nil, tt)(BreakException) + ), ) Throw(NewObject[Post](cls.ref))(PanicBlame( @@ -156,7 +159,7 @@ case class EncodeBreakReturn[Pre <: Generation]() extends Rewriter[Pre] { )) case Return(result) => - val exc = new Variable[Post](TClass(returnClass.get.ref, Seq())) + val exc = new Variable[Post](returnClass.get.classType(Seq())) Scope( Seq(exc), Block(Seq( @@ -196,13 +199,16 @@ case class EncodeBreakReturn[Pre <: Generation]() extends Rewriter[Pre] { ReturnField ) val returnClass = - new Class[Post](Nil, Seq(returnField), Nil, tt)( - ReturnClass - ) + new ByReferenceClass[Post]( + Nil, + Seq(returnField), + Nil, + tt, + )(ReturnClass) globalDeclarations.declare(returnClass) val caughtReturn = - new Variable[Post](TClass(returnClass.ref, Seq())) + new Variable[Post](returnClass.classType(Seq())) TryCatchFinally( body = BreakReturnToException( diff --git a/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala index 737d301e7c..3e1f1a2f75 100644 --- a/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala @@ -1350,7 +1350,8 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) // Create a class that can be used to create a 'this' object // It will be linked to the class made near the end of this method. - val preEventClass: Class[Pre] = new Class(Nil, Nil, Nil, tt)(commandGroup.o) + val preEventClass: Class[Pre] = + new ByValueClass(Nil, Nil, Nil)(commandGroup.o) this.currentThis = Some( rw.dispatch(ThisObject[Pre](preEventClass.ref)(preEventClass.o)) ) @@ -1477,8 +1478,9 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) )(KernelLambdaRunMethodBlame(kernelDeclaration))(commandGroup.o) // Create the surrounding class + // cl::sycl::event has a default copy constructor hence a ByValueClass val postEventClass = - new Class[Post]( + new ByValueClass[Post]( typeArgs = Seq(), decls = currentKernelType.get.getRangeFields ++ @@ -1486,13 +1488,12 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) .flatMap(acc => acc.instanceField +: acc.rangeIndexFields) ++ Seq(kernelRunner), supports = Seq(), - intrinsicLockInvariant = tt, )(commandGroup.o.where(name = "SYCL_EVENT_CLASS")) rw.globalDeclarations.succeed(preEventClass, postEventClass) // Create a variable to refer to the class instance val eventClassRef = - new Variable[Post](TClass(postEventClass.ref, Seq()))( + new Variable[Post](TByValueClass(postEventClass.ref, Seq()))( commandGroup.o.where(name = "sycl_event_ref") ) // Store the class ref and read-write accessors to be used when the kernel is done running @@ -1978,7 +1979,7 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) preClass: Class[Pre], commandGroupO: Origin, ): Procedure[Post] = { - val t = rw.dispatch(TClass[Pre](preClass.ref, Seq())) + val t = rw.dispatch(TByValueClass[Pre](preClass.ref, Seq())) rw.globalDeclarations.declare( withResult((result: Result[Post]) => { val constructorPostConditions: mutable.Buffer[Expr[Post]] = @@ -2144,22 +2145,24 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) scale(cond) else rw.variables.scope { - val range = quantVars.map(v => - rangesMap(v)._1 <= Local[Post](v.ref) && - Local[Post](v.ref) < rangesMap(v)._2 - ).reduceOption[Expr[Post]](And(_, _)).getOrElse(tt) - - cond match { - case Forall(bindings, Nil, body) => - Forall(bindings ++ quantVars, Nil, range ==> scale(body)) - case s @ Starall(bindings, Nil, body) => - Starall(bindings ++ quantVars, Nil, range ==> scale(body))( - s.blame - ) - case other => - Starall(quantVars.toSeq, Nil, range ==> scale(other))( - ParBlockNotInjective(block, other) - ) + rw.localHeapVariables.scope { + val range = quantVars.map(v => + rangesMap(v)._1 <= Local[Post](v.ref) && + Local[Post](v.ref) < rangesMap(v)._2 + ).reduceOption[Expr[Post]](And(_, _)).getOrElse(tt) + + cond match { + case Forall(bindings, Nil, body) => + Forall(bindings ++ quantVars, Nil, range ==> scale(body)) + case s @ Starall(bindings, Nil, body) => + Starall(bindings ++ quantVars, Nil, range ==> scale(body))( + s.blame + ) + case other => + Starall(quantVars.toSeq, Nil, range ==> scale(other))( + ParBlockNotInjective(block, other) + ) + } } } }) diff --git a/src/rewrite/vct/rewrite/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala index b187e5f7f4..3b98839ed6 100644 --- a/src/rewrite/vct/rewrite/lang/LangCToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCToCol.scala @@ -14,6 +14,7 @@ import vct.col.resolve.ctx._ import vct.col.resolve.lang.C.nameFromDeclarator import vct.col.resolve.lang.Java.logger import vct.col.rewrite.{Generation, Rewritten} +import vct.col.typerules.CoercionUtils import vct.col.typerules.CoercionUtils.getCoercion import vct.col.util.SuccessionMap import vct.col.util.AstBuildHelpers._ @@ -192,25 +193,6 @@ case object LangCToCol { } } - case class StructCopyFailed( - assign: PreAssignExpression[_], - field: InstanceField[_], - ) extends Blame[InsufficientPermission] { - override def blame(error: InsufficientPermission): Unit = { - assign.blame.blame(CopyStructFailed(assign, Referrable.originName(field))) - } - } - - case class StructCopyBeforeCallFailed( - inv: CInvocation[_], - field: InstanceField[_], - ) extends Blame[InsufficientPermission] { - override def blame(error: InsufficientPermission): Unit = { - inv.blame - .blame(CopyStructFailedBeforeCall(inv, Referrable.originName(field))) - } - } - case class VectorBoundFailed(subscript: AmbiguousSubscript[_]) extends Blame[InvocationFailure] { override def blame(error: InvocationFailure): Unit = @@ -273,6 +255,9 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) SuccessionMap() val cNameSuccessor: SuccessionMap[CNameTarget[Pre], Variable[Post]] = SuccessionMap() + val cLocalHeapNameSuccessor + : SuccessionMap[CNameTarget[Pre], LocalHeapVariable[Post]] = + SuccessionMap() val cGlobalNameSuccessor : SuccessionMap[CNameTarget[Pre], HeapVariable[Post]] = SuccessionMap() val cStructSuccessor: SuccessionMap[CGlobalDeclaration[Pre], Class[Post]] = @@ -303,7 +288,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) private var kernelSpecifier: Option[CGpgpuKernelSpecifier[Pre]] = None private def CStructOrigin(sdecl: CStructDeclaration[_]): Origin = - sdecl.o.sourceName(sdecl.name.get) + sdecl.o.sourceName(sdecl.name.get).withContent(TypeName("struct")) private def CStructFieldOrigin(cdecl: CDeclarator[_]): Origin = cdecl.o.sourceName(nameFromDeclarator(cdecl)) @@ -428,6 +413,16 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) case CCast(CInvocation(CLocal("__vercors_malloc"), _, _, _), _) => throw UnsupportedMalloc(c) case CCast(n @ Null(), t) if t.asPointer.isDefined => rw.dispatch(n) + case CCast(e, t) if e.t.asPointer.isDefined && t.asPointer.isDefined => + val newE = rw.dispatch(e) + val newT = rw.dispatch(t) + if ( + CoercionUtils.firstElementIsType( + newE.t.asPointer.get.element, + newT.asPointer.get.element, + ) + ) { Cast(newE, TypeValue(newT)(t.o))(c.o) } + else { throw UnsupportedCast(c) } case _ => throw UnsupportedCast(c) } @@ -999,7 +994,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) case _ => throw WrongStructType(decl) } val newStruct = - new Class[Post]( + new ByValueClass[Post]( Seq(), rw.classDeclarations.collect { decls.foreach { fieldDecl => @@ -1019,7 +1014,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) } }._1, Seq(), - tt[Post], )(CStructOrigin(sdecl)) rw.globalDeclarations.declare(newStruct) @@ -1056,12 +1050,16 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) contract = rw.dispatch(decl.decl.contract), pure = pure, inline = inline, - )(AbstractApplicable)(init.o) + )(AbstractApplicable)(init.o.sourceName(info.name)) ) ) case None => + val newT = + if (t.isInstanceOf[TByValueClass[Post]]) { TNonNullPointer(t) } + else { t } cGlobalNameSuccessor(RefCGlobalDeclaration(decl, idx)) = rw - .globalDeclarations.declare(new HeapVariable(t)(init.o)) + .globalDeclarations + .declare(new HeapVariable(newT)(init.o.sourceName(info.name))) } } } @@ -1109,6 +1107,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) } } + // TODO: (AS) Fixed-size arrays seem to become pointers but they're actually value types def rewriteArrayDeclaration( decl: CLocalDeclaration[Pre], cta: CTArray[Pre], @@ -1163,21 +1162,23 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) implicit val o: Origin = init.o val targetClass: Class[Post] = cStructSuccessor(ref.decl) - val t = TClass[Post](targetClass.ref, Seq()) + val t = TByValueClass[Post](targetClass.ref, Seq()) - val v = new Variable[Post](t)(o.sourceName(info.name)) - cNameSuccessor(RefCLocalDeclaration(decl, 0)) = v - - val initialVal = init.init.map(i => - createStructCopy( - rw.dispatch(i), - ref.decl, - (f: InstanceField[_]) => - PanicBlame("Cannot fail due to insufficient perm"), - ) - ).getOrElse(NewObject[Post](targetClass.ref)) - - Block(Seq(LocalDecl(v), assignLocal(v.get, initialVal))) + val v = + new LocalHeapVariable[Post](TNonNullPointer(t))(o.sourceName(info.name)) + cLocalHeapNameSuccessor(RefCLocalDeclaration(decl, 0)) = v + + if (init.init.isDefined) { + Block(Seq( + HeapLocalDecl(v), + Assign( + v.get(PanicBlame( + "Dereferencing freshly declared struct should never fail" + )), + rw.dispatch(init.init.get), + )(AssignLocalOk), + )) + } else { HeapLocalDecl(v) } } def rewriteLocal(decl: CLocalDeclaration[Pre]): Statement[Post] = { @@ -1337,9 +1338,28 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) case ref @ RefCGlobalDeclaration(decl, initIdx) => C.getDeclaratorInfo(decl.decl.inits(initIdx).decl).params match { case None => - DerefHeapVariable[Post](cGlobalNameSuccessor.ref(ref))(local.blame) + val t = + decl.decl.specs.collectFirst { case t: CSpecificationType[Pre] => + t.t + }.get + if (t.isInstanceOf[CTStruct[Pre]]) { + DerefPointer( + DerefHeapVariable[Post](cGlobalNameSuccessor.ref(ref))( + local.blame + ) + )(local.blame) + } else { + DerefHeapVariable[Post](cGlobalNameSuccessor.ref(ref))( + local.blame + ) + } case Some(_) => throw NotAValue(local) } + case ref: RefCLocalDeclaration[Pre] + if cLocalHeapNameSuccessor.contains(ref) => + DerefPointer(HeapLocal[Post](cLocalHeapNameSuccessor.ref(ref)))( + local.blame + ) case ref: RefCLocalDeclaration[Pre] => Local(cNameSuccessor.ref(ref)) case _: RefCudaVec[Pre] => throw NotAValue(local) } @@ -1460,59 +1480,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) foldStar(newFieldPerms) } - def createStructCopy( - value: Expr[Post], - struct: CGlobalDeclaration[Pre], - blame: InstanceField[_] => Blame[InsufficientPermission], - )(implicit o: Origin): Expr[Post] = { - val targetClass: Class[Post] = cStructSuccessor(struct) - val t = TClass[Post](targetClass.ref, Seq()) - - // Assign a new variable towards the value, such that methods do not get executed multiple times. - val vValue = new Variable[Post](t) - // The copy of the value - val vCopy = new Variable[Post](t) - - val fieldAssigns = targetClass.declarations.collect { - case field: InstanceField[Post] => - val ref: Ref[Post, InstanceField[Post]] = field.ref - assignField( - vCopy.get, - ref, - Deref[Post](vValue.get, field.ref)(blame(field)), - PanicBlame("Assignment should work"), - ) - } - - With( - Block( - Seq( - LocalDecl(vCopy), - LocalDecl(vValue), - assignLocal(vValue.get, value), - assignLocal(vCopy.get, NewObject[Post](targetClass.ref)), - ) ++ fieldAssigns - ), - vCopy.get, - ) - } - - def assignStruct(assign: PreAssignExpression[Pre]): Expr[Post] = { - getBaseType(assign.target.t) match { - case CTStruct(ref) => - val copy = - createStructCopy( - rw.dispatch(assign.value), - ref.decl, - (f: InstanceField[_]) => StructCopyFailed(assign, f), - )(assign.o) - PreAssignExpression(rw.dispatch(assign.target), copy)(AssignLocalOk)( - assign.o - ) - case _ => throw WrongStructType(assign.target) - } - } - def createUpdateVectorFunction(size: Int): Function[Post] = { implicit val o: Origin = Origin(Seq(LabelContext("vector update method"))) /* for instance for size 4: @@ -1748,18 +1715,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) case _ => } - // Create copy for any direct structure arguments - val newArgs = args.map(a => - getBaseType(a.t) match { - case CTStruct(ref) => - createStructCopy( - rw.dispatch(a), - ref.decl, - (f: InstanceField[_]) => StructCopyBeforeCallFailed(inv, f), - )(a.o) - case _ => rw.dispatch(a) - } - ) + val newArgs = args.map(a => rw.dispatch(a)) implicit val o: Origin = inv.o inv.ref.get match { @@ -1998,6 +1954,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) def structType(t: CTStruct[Pre]): Type[Post] = { val targetClass = new LazyRef[Post, Class[Post]](cStructSuccessor(t.ref.decl)) - TClass[Post](targetClass, Seq())(t.o) + TByValueClass[Post](targetClass, Seq())(t.o) } } diff --git a/src/rewrite/vct/rewrite/lang/LangJavaToCol.scala b/src/rewrite/vct/rewrite/lang/LangJavaToCol.scala index 7a65f46ca6..8b73dce94d 100644 --- a/src/rewrite/vct/rewrite/lang/LangJavaToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangJavaToCol.scala @@ -275,7 +275,7 @@ case class LangJavaToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) case cons: JavaConstructor[Pre] => logger.debug(s"Constructor for ${cons.o.inlineContextText}") implicit val o: Origin = cons.o - val t = TClass(ref, Seq()) + val t = TByReferenceClass(ref, Seq()) val `this` = ThisObject(ref) val results = currentJavaClass.top.modifiers.collect { @@ -429,7 +429,7 @@ case class LangJavaToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) val instanceClass = rw.currentThis.having(ThisObject(javaInstanceClassSuccessor.ref(cls))) { - new Class[Post]( + new ByReferenceClass[Post]( rw.variables.dispatch(cls.typeParams)(rw), rw.classDeclarations.collect { makeJavaClass( @@ -454,7 +454,7 @@ case class LangJavaToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) if (staticDecls.nonEmpty) { val staticsClass = - new Class[Post]( + new ByReferenceClass[Post]( Seq(), rw.classDeclarations.collect { rw.currentThis @@ -472,7 +472,7 @@ case class LangJavaToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) )(JavaStaticsClassOrigin(cls)) rw.globalDeclarations.declare(staticsClass) - val t = TClass[Post](staticsClass.ref, Seq()) + val t = TByReferenceClass[Post](staticsClass.ref, Seq()) val singleton = withResult((res: Result[Post]) => function( AbstractApplicable, @@ -754,7 +754,7 @@ case class LangJavaToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) def classType(t: JavaTClass[Pre]): Type[Post] = t.ref.decl match { case classOrInterface: JavaClassOrInterface[Pre] => - TClass( + TByReferenceClass( javaInstanceClassSuccessor.ref(classOrInterface), t.typeArgs.map(rw.dispatch), ) diff --git a/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala b/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala index 91b814282c..07f44d51a5 100644 --- a/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala @@ -179,7 +179,7 @@ case class LangPVLToCol[Pre <: Generation]( val PVLNew(t, typeArgs, args, givenMap, yields) = inv val classTypeArgs = t match { - case TClass(_, typeArgs) => typeArgs + case t: TClass[Pre] => t.typeArgs case _ => Seq() } implicit val o: Origin = inv.o diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala index 1f450177c2..687c3adc07 100644 --- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala @@ -203,7 +203,13 @@ case class LangSpecificToCol[Pre <: Generation]( pvl.maybeDeclareDefaultConstructor(cls) }._1 - globalDeclarations.succeed(cls, cls.rewrite(decls = decls)) + globalDeclarations.succeed( + cls, + cls match { + case cls: ByReferenceClass[Pre] => cls.rewrite(decls = decls) + case cls: ByValueClass[Pre] => cls.rewrite(decls = decls) + }, + ) } } @@ -323,17 +329,17 @@ case class LangSpecificToCol[Pre <: Generation]( case cast: CCast[Pre] => c.cast(cast) case sizeof: SizeOf[Pre] => throw LangCToCol.UnsupportedSizeof(sizeof) - case Perm(a @ AmbiguousLocation(expr), perm) - if c.getBaseType(expr.t).isInstanceOf[CTStruct[Pre]] => - c.getBaseType(expr.t) match { - case structType: CTStruct[Pre] => - c.unwrapStructPerm( - dispatch(a).asInstanceOf[AmbiguousLocation[Post]], - perm, - structType, - e.o, - ) - } +// case Perm(a @ AmbiguousLocation(expr), perm) +// if c.getBaseType(expr.t).isInstanceOf[CTStruct[Pre]] => +// c.getBaseType(expr.t) match { +// case structType: CTStruct[Pre] => +// c.unwrapStructPerm( +// dispatch(a).asInstanceOf[AmbiguousLocation[Post]], +// perm, +// structType, +// e.o, +// ) +// } case local: CPPLocal[Pre] => cpp.local(local) case deref: CPPClassMethodOrFieldAccess[Pre] => cpp.deref(deref) case inv: CPPInvocation[Pre] => cpp.invocation(inv) @@ -366,10 +372,6 @@ case class LangSpecificToCol[Pre <: Generation]( case _ => } assign.target.t match { - case CPrimitiveType(specs) if specs.collectFirst { - case CSpecificationType(_: CTStruct[Pre]) => () - }.isDefined => - c.assignStruct(assign) case CPPPrimitiveType(_) => cpp.preAssignExpr(assign) case _ => rewriteDefault(assign) } diff --git a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala index 6b7f9fe8eb..adfbeb4be1 100644 --- a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala @@ -88,7 +88,10 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] { case t @ PVLNamedType(_, typeArgs) => t.ref.get match { case spec: SpecTypeNameTarget[Pre] => specType(spec, typeArgs) - case RefClass(decl) => TClass(succ(decl), typeArgs.map(dispatch)) + case RefClass(decl: ByReferenceClass[Pre]) => + TByReferenceClass(succ[Class[Post]](decl), typeArgs.map(dispatch)) + case RefClass(decl: ByValueClass[Pre]) => + TByValueClass(succ[Class[Post]](decl), typeArgs.map(dispatch)) } case t @ CPrimitiveType(specs) => dispatch(C.getPrimitiveType(specs, context = Some(t))) diff --git a/src/rewrite/vct/rewrite/lang/NoSupportSelfLoop.scala b/src/rewrite/vct/rewrite/lang/NoSupportSelfLoop.scala index de0cfe57c6..f59b38fcb1 100644 --- a/src/rewrite/vct/rewrite/lang/NoSupportSelfLoop.scala +++ b/src/rewrite/vct/rewrite/lang/NoSupportSelfLoop.scala @@ -13,7 +13,15 @@ case object NoSupportSelfLoop extends RewriterBuilder { case class NoSupportSelfLoop[Pre <: Generation]() extends Rewriter[Pre] { override def dispatch(decl: Declaration[Pre]): Unit = decl match { - case cls: Class[Pre] => + case cls: ByReferenceClass[Pre] => + globalDeclarations.succeed( + cls, + cls.rewrite(supports = + cls.supports.filter(_.asClass.get.cls.decl != cls) + .map(_.rewriteDefault()) + ), + ) + case cls: ByValueClass[Pre] => globalDeclarations.succeed( cls, cls.rewrite(supports = diff --git a/src/rewrite/vct/rewrite/util/Extract.scala b/src/rewrite/vct/rewrite/util/Extract.scala index 95ef8f02d9..35ba7fe755 100644 --- a/src/rewrite/vct/rewrite/util/Extract.scala +++ b/src/rewrite/vct/rewrite/util/Extract.scala @@ -84,7 +84,9 @@ case class Extract[G]() { t -> Local( getOrElseUpdate( free, - new Variable(extract(TClass(t.cls, Seq())))(ExtractOrigin("this")), + new Variable(extract(t.cls.decl.classType(Seq())))(ExtractOrigin( + "this" + )), ).ref[Variable[G]] )(ExtractOrigin("")) case free @ FreeThisModel(t) => diff --git a/src/rewrite/vct/rewrite/veymont/generation/EncodeGlobalApplicables.scala b/src/rewrite/vct/rewrite/veymont/generation/EncodeGlobalApplicables.scala index 2174c03687..4ddfe8e7ae 100644 --- a/src/rewrite/vct/rewrite/veymont/generation/EncodeGlobalApplicables.scala +++ b/src/rewrite/vct/rewrite/veymont/generation/EncodeGlobalApplicables.scala @@ -6,6 +6,7 @@ import vct.col.ast.{ Block, Assert, Assume, + ByReferenceClass, Class, Constructor, Declaration, @@ -27,7 +28,7 @@ import vct.col.ast.{ Program, Result, Statement, - TClass, + TByReferenceClass, } import vct.col.origin.{ Blame, @@ -123,7 +124,7 @@ case class EncodeGlobalApplicables[Pre <: Generation]() extends Rewriter[Pre] { decl match { // Functions and procedures are moved into the global statics class case _: Function[Pre] | _: Procedure[Pre] => decl.drop() - case cls: Class[Pre] => + case cls: ByReferenceClass[Pre] => cls.rewrite(intrinsicLockInvariant = spec { cls.intrinsicLockInvariant.rewriteDefault() }).succeed(cls) @@ -153,7 +154,7 @@ case class EncodeGlobalApplicables[Pre <: Generation]() extends Rewriter[Pre] { def createGlobalClass(program: Program[Pre]): Unit = { globals.fill( - new Class( + new ByReferenceClass( decls = classDeclarations.collect { globalsConstructor.fill( @@ -181,7 +182,7 @@ case class EncodeGlobalApplicables[Pre <: Generation]() extends Rewriter[Pre] { blame = PanicBlame("Trivial contract"), contractBlame = TrueSatisfiable, ensures = (result !== Null()).accounted, - returnType = TClass[Post](globals.ref, Seq()), + returnType = TByReferenceClass[Post](globals.ref, Seq()), )(program.o.where(name = "g$")).declare() )) } diff --git a/src/rewrite/vct/rewrite/veymont/generation/GenerateAndEncodeChannels.scala b/src/rewrite/vct/rewrite/veymont/generation/GenerateAndEncodeChannels.scala index 1fb5c1ec94..3708ec05b2 100644 --- a/src/rewrite/vct/rewrite/veymont/generation/GenerateAndEncodeChannels.scala +++ b/src/rewrite/vct/rewrite/veymont/generation/GenerateAndEncodeChannels.scala @@ -5,6 +5,7 @@ import hre.util.ScopedStack import vct.col.ast.{ Assign, Block, + ByReferenceClass, ChorRun, Choreography, Class, @@ -37,6 +38,7 @@ import vct.col.ast.{ Scope, Sender, Statement, + TByReferenceClass, TClass, TVar, ThisObject, @@ -68,7 +70,10 @@ case class GenerateAndEncodeChannels[Pre <: Generation]( private lazy val channelPre = importer.loadAdt[Pre]("genericChannel").declarations - lazy val genericChannelClass = find[Pre, Class[Pre]](channelPre, "Channel") + lazy val genericChannelClass = find[Pre, ByReferenceClass[Pre]]( + channelPre, + "Channel", + ) lazy val genericChannelDecls = genericChannelClass.decls lazy val genericChannelConstructor = find[Pre, Constructor[Pre]]( genericChannelDecls @@ -90,7 +95,8 @@ case class GenerateAndEncodeChannels[Pre <: Generation]( "exchangeValue", ) - val channelClassSucc = SuccessionMap[Communicate[Pre], Class[Post]]() + val channelClassSucc = + SuccessionMap[Communicate[Pre], ByReferenceClass[Post]]() val channelConstructorSucc = SuccessionMap[Communicate[Pre], Constructor[Post]]() val channelWriteSucc = SuccessionMap[Communicate[Pre], InstanceMethod[Post]]() @@ -124,7 +130,7 @@ case class GenerateAndEncodeChannels[Pre <: Generation]( .LinkedHashMap[Communicate[Pre], Variable[Post]]() def channelType(comm: Communicate[Pre]): Type[Post] = - TClass[Post](channelClassSucc.ref(comm), Seq()) + TByReferenceClass[Post](channelClassSucc.ref(comm), Seq()) def generateChannel(comm: Communicate[Pre]): Unit = currentCommunicate.having(comm) { dispatch(genericChannelClass) } @@ -253,7 +259,7 @@ case class GenerateAndEncodeChannels[Pre <: Generation]( }).succeed(chor) } - case cls: Class[Pre] if isEndpointClass(cls) => + case cls: ByReferenceClass[Pre] if isEndpointClass(cls) => // For each communicate in a choreography, add fields for the communicate channel to classes // of endpoints participating in the choreography cls.rewrite(decls = @@ -294,7 +300,7 @@ case class GenerateAndEncodeChannels[Pre <: Generation]( ), ).succeed(cons) - case cls: Class[Pre] if cls == genericChannelClass => + case cls: ByReferenceClass[Pre] if cls == genericChannelClass => implicit val comm = currentCommunicate.top implicit val o = comm.o globalDeclarations.scope { diff --git a/src/rewrite/vct/rewrite/veymont/generation/GenerateImplementation.scala b/src/rewrite/vct/rewrite/veymont/generation/GenerateImplementation.scala index a286326e6b..b044431b1f 100644 --- a/src/rewrite/vct/rewrite/veymont/generation/GenerateImplementation.scala +++ b/src/rewrite/vct/rewrite/veymont/generation/GenerateImplementation.scala @@ -11,6 +11,7 @@ import vct.col.ast.{ Assume, Block, Branch, + ByReferenceClass, ChorPerm, ChorRun, ChorStatement, @@ -117,7 +118,7 @@ case class GenerateImplementation[Pre <: Generation]() override def dispatch(decl: Declaration[Pre]): Unit = { decl match { case p: Procedure[Pre] => super.dispatch(p) - case cls: Class[Pre] if isEndpointClass(cls) => + case cls: ByReferenceClass[Pre] if isEndpointClass(cls) => val chor = choreographyOf(cls) val endpoint = endpointOf(cls) currentThis.having(ThisObject[Post](succ(cls))(cls.o)) { diff --git a/src/rewrite/vct/rewrite/veymont/generation/SpecializeEndpointClasses.scala b/src/rewrite/vct/rewrite/veymont/generation/SpecializeEndpointClasses.scala index 46ff5fe24b..eef433d8ea 100644 --- a/src/rewrite/vct/rewrite/veymont/generation/SpecializeEndpointClasses.scala +++ b/src/rewrite/vct/rewrite/veymont/generation/SpecializeEndpointClasses.scala @@ -1,8 +1,9 @@ -package vct.rewrite.veymont.generation +package vct.rewrite.veymont import com.typesafe.scalalogging.LazyLogging import vct.col.ast.{ ChorRun, + ByReferenceClass, Choreography, Class, Communicate, @@ -111,7 +112,7 @@ case class SpecializeEndpointClasses[Pre <: Generation]() } val wrapperClass = - new Class[Post]( + new ByReferenceClass[Post]( typeArgs = Seq(), supports = Seq(), intrinsicLockInvariant = tt, diff --git a/src/rewrite/vct/rewrite/veymont/verification/EncodeChoreography.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodeChoreography.scala index f6135cc043..f22ed7dd10 100644 --- a/src/rewrite/vct/rewrite/veymont/verification/EncodeChoreography.scala +++ b/src/rewrite/vct/rewrite/veymont/verification/EncodeChoreography.scala @@ -30,7 +30,7 @@ import vct.col.ast.{ Scope, Sender, Statement, - TClass, + TByReferenceClass, TVoid, ThisChoreography, Value, @@ -197,9 +197,9 @@ case class EncodeChoreography[Pre <: Generation]() currentInstanceMethod.having(method) { for (endpoint <- prog.endpoints) { endpointSucc((mode, endpoint)) = - new Variable(TClass(succ[Class[Post]](endpoint.cls.decl), Seq()))( - endpoint.o - ) + new Variable( + TByReferenceClass(succ[Class[Post]](endpoint.cls.decl), Seq()) + )(endpoint.o) } prog.params.foreach(_.drop()) diff --git a/src/viper/viper/api/backend/SilverBackend.scala b/src/viper/viper/api/backend/SilverBackend.scala index d6de5f6324..59d8c03c93 100644 --- a/src/viper/viper/api/backend/SilverBackend.scala +++ b/src/viper/viper/api/backend/SilverBackend.scala @@ -393,7 +393,7 @@ trait SilverBackend .NegativePermissionValue( info(p).permissionValuePermissionNode.get ) // need to fetch access - case _ => ??? + case r => throw new NotImplementedError("Missing: " + r) } def getDecreasesClause(reason: ErrorReason): col.DecreasesClause[_] = diff --git a/src/viper/viper/api/transform/ColToSilver.scala b/src/viper/viper/api/transform/ColToSilver.scala index badc42b153..9e27216415 100644 --- a/src/viper/viper/api/transform/ColToSilver.scala +++ b/src/viper/viper/api/transform/ColToSilver.scala @@ -6,7 +6,7 @@ import vct.col.ref.Ref import vct.col.util.AstBuildHelpers.unfoldStar import vct.col.{ast => col} import vct.result.VerificationError.{SystemError, Unreachable} -import viper.silver.ast.{TypeVar, WildcardPerm} +import viper.silver.ast.{AnnotationInfo, ConsInfo, TypeVar, WildcardPerm} import viper.silver.plugin.standard.termination.{ DecreasesClause, DecreasesTuple, diff --git a/test/main/vct/helper/SimpleProgramGenerator.scala b/test/main/vct/helper/SimpleProgramGenerator.scala index f0587c3abd..3aee073fe9 100644 --- a/test/main/vct/helper/SimpleProgramGenerator.scala +++ b/test/main/vct/helper/SimpleProgramGenerator.scala @@ -20,7 +20,7 @@ object SimpleProgramGenerator { val contract1 = generateSimpleApplicableContract[G]() val blame1 = origin val method1 = new InstanceMethod(TVoid(), Nil, Nil, Nil, Option(body), contract1)(blame1) - val classNode1 = new Class(Nil, Seq(method1), Nil, tt) + val classNode1 = new ByReferenceClass(Nil, Seq(method1), Nil, tt) Program(Seq(classNode1))(DiagnosticOrigin) } diff --git a/test/main/vct/test/integration/examples/CSpec.scala b/test/main/vct/test/integration/examples/CSpec.scala index d4cfd0de4e..02abb280ad 100644 --- a/test/main/vct/test/integration/examples/CSpec.scala +++ b/test/main/vct/test/integration/examples/CSpec.scala @@ -11,6 +11,7 @@ class CSpec extends VercorsSpec { vercors should verify using silicon example "concepts/c/structs.c" vercors should verify using silicon example "concepts/c/vector_add.c" vercors should verify using silicon example "concepts/c/vector_type.c" + vercors should verify using silicon example "concepts/c/pointer_casts.c" vercors should error withCode "resolutionError:type" in "float should not be demoted" c """ @@ -18,7 +19,7 @@ class CSpec extends VercorsSpec { int x = 4.0 % 1; } """ - vercors should fail withCode "assignFieldFailed" using silicon in "cannot access field of struct after freeing" c + vercors should fail withCode "ptrPerm" using silicon in "cannot access field of struct after freeing" c """ #include @@ -76,7 +77,7 @@ class CSpec extends VercorsSpec { int main(){ struct d* xs = (struct d*) malloc(sizeof(struct d)*3); struct d* ys = (struct d*) malloc(sizeof(struct d)*3); - //@ exhale Perm(xs[0].x, 1\2); + //@ exhale Perm(&xs[0].x, 1\2); free(xs); } """ @@ -112,7 +113,7 @@ class CSpec extends VercorsSpec { int main(){ struct d s1; struct d* s2 = &s1; - //@ exhale Perm(s2->x, 1\1); + //@ exhale Perm(&s2->x, 1\1); s2->x = 1; } """ @@ -124,7 +125,7 @@ class CSpec extends VercorsSpec { }; int main(){ struct d s; - //@ exhale Perm(s.x, 1\1); + //@ exhale Perm(&s.x, 1\1); s.x = 1; } """ @@ -136,12 +137,12 @@ class CSpec extends VercorsSpec { int main(){ struct d s; s.x = 1; - //@ exhale Perm(s.x, 1\1); + //@ exhale Perm(&s.x, 1\1); int x = s.x; } """ - vercors should error withCode "unsupportedCast" in "Cast ptr struct to int" c + vercors should verify using silicon in "Cast ptr struct to int" c """ struct d{ int x; @@ -310,7 +311,7 @@ class CSpec extends VercorsSpec { } """ - vercors should fail withCode "copyStructFailedBeforeCall" using silicon in "Insufficient permission for field x to copy struct before call" c + vercors should fail withCode "copyClassFailedBeforeCall" using silicon in "Insufficient permission for field x to copy struct before call" c """ struct d { int x; @@ -323,12 +324,12 @@ class CSpec extends VercorsSpec { int main(){ struct d s; - //@ exhale Perm(s.x, 1\1); + //@ exhale Perm(&s.x, 1\1); test(s); } """ - vercors should fail withCode "copyStructFailed" using silicon in "Insufficient permission for field x to copy struct" c + vercors should fail withCode "copyClassFailed" using silicon in "Insufficient permission for field x to copy struct" c """ struct d { int x; @@ -341,7 +342,7 @@ class CSpec extends VercorsSpec { int main(){ struct d s, t; - //@ exhale Perm(s.x, 1\1); + //@ exhale Perm(&s.x, 1\1); t = s; } """ @@ -377,17 +378,17 @@ class CSpec extends VercorsSpec { #include struct nested { - struct nested *inner; + struct nested *inner; }; void main() { - int *ip = NULL; - double *dp = NULL; - struct nested *np = NULL; - np = (struct nested*) NULL; + int *ip = NULL; + double *dp = NULL; + struct nested *np = NULL; + np = (struct nested*) NULL; np = (struct nested*) malloc(sizeof(struct nested)); np->inner = NULL; - np->inner = (struct nested*) NULL; + np->inner = (struct nested*) NULL; } """ @@ -562,4 +563,22 @@ class CSpec extends VercorsSpec { return; } """ -} \ No newline at end of file + + vercors should error withCode "unsupportedCast" in "Casting struct pointers only works for the first element" c + """ + #include + struct A { + int integer; + bool boolean; + }; + + struct B { + struct A struct_a; + }; + void cannotCastToBoolean() { + struct B struct_b; + struct_b.struct_a.boolean = true == true; // We currently don't support boolean literals + bool *pointer_to_boolean = (bool *)&struct_b; + } + """ +}