diff --git a/examples/runtime/ledgerExample.java b/examples/runtime/ledgerExample.java new file mode 100644 index 0000000000..d2e4cedcd3 --- /dev/null +++ b/examples/runtime/ledgerExample.java @@ -0,0 +1,98 @@ +package test; + +import java.lang.reflect.Array; +import java.util.concurrent.ConcurrentHashMap; + + +class Ledger { + + public static ConcurrentHashMap> __runtime__ = new ConcurrentHashMap>(); + public static ConcurrentHashMap> __array_locations = new ConcurrentHashMap>(); + + + public static void createHashMap() { + if (!__runtime__.containsKey(Thread.currentThread().getId())) { + __runtime__.put(Thread.currentThread().getId(), new ConcurrentHashMap()); + } + } + + public static Double getPermission(Object input) { + createHashMap(); + return __runtime__.get(Thread.currentThread().getId()).getOrDefault(input, 0.0); + } + + public static Double getPermission(Object input, int location) { + createHashMap(); + Object permLoc = __array_locations.get(input).get(location); + return getPermission(permLoc); + } + + public static void setPermission(Object input, Double value) { + assert (value >= 0 && value <= 1) : "value is not between bounds 0 and 1: " + value; + createHashMap(); + __runtime__.get(Thread.currentThread().getId()).put(input, value); + } + + public static void setPermission(Object input, int location, Double value) { + createHashMap(); + assert (input.getClass().isArray()); + Object permLoc = __array_locations.get(input).get(location); + setPermission(permLoc, value); + } + + public static void initiatePermission(Object input) { + createHashMap(); + setPermission(input, 1.0); + if (input.getClass().isArray()) { + initiatePermission(input, Array.getLength(input)); + } + } + + public static void initiatePermission(Object input, int size) { + createHashMap(); + setPermission(input, 1.0); + __array_locations.put(input, new ConcurrentHashMap<>()); + for (int i = 0; i < size; i++) { + Object[] permLoc = {input, i}; + __array_locations.get(input).put(i, permLoc); + setPermission(permLoc, 1.0); + } + + } +} + + +class Test extends Thread{ + int[] a; + int b; + + public Test(int[] a) { + this.a = a; + } + + /*@ + requires Perm(this.a, write); + */ + @Override + public void run() { + Ledger.setPermission(this.a, 1.0); + System.out.println("External thread: " + Ledger.getPermission(this.a)); + super.run(); + } +} + + +class Main { + + public static void main(String[] args) { + int[] a = new int[]{1, 2, 3, 4}; + Ledger.initiatePermission(a); + Test test = new Test(a); + Ledger.setPermission(test.a, Ledger.getPermission(test.a) - 1.0); + test.start(); + Ledger.initiatePermission(test, 1); + System.out.println(Ledger.getPermission(test.a)); + System.out.println(Ledger.getPermission(test, 0)); + } +} + diff --git a/examples/runtime/lockInvariant.java b/examples/runtime/lockInvariant.java new file mode 100644 index 0000000000..725f03e4fa --- /dev/null +++ b/examples/runtime/lockInvariant.java @@ -0,0 +1,16 @@ +//@ lock_invariant Perm(this.i, write); +class Source { + int i; + + public void test(){ + int x = this.i; + synchronized (this) { + this.i = 0; + } + } + + public void main() { + Source source = new Source(); + source.test(); + } +} \ No newline at end of file diff --git a/examples/runtime/loopInvariants.java b/examples/runtime/loopInvariants.java new file mode 100644 index 0000000000..49277e5824 --- /dev/null +++ b/examples/runtime/loopInvariants.java @@ -0,0 +1,29 @@ +class Program { + int[] a; + + public void setA(int[] a) { + this.a = a; + } + + public int indexOf(int b) { + //@ loop_invariant i <= a.length; + //@ loop_invariant (\forall* int j; 0 <= j && j < a.length; Perm(a[j], read)); + //@ loop_invariant (\forall int j; 0 <= j && j < a.length; a[j] % 3 == 0); + for(int i = 0; i < a.length; i++) { + if(a[i] == b) { + return i; + } + } + return -1; + } + + public void main() { + Program program = new Program(); + int[] tmp = new int[3]; + tmp[0] = 2; + tmp[1] = 4; + tmp[2] = 6; + program.setA(tmp); + program.indexOf(4); + } +} \ No newline at end of file diff --git a/examples/runtime/predicates.java b/examples/runtime/predicates.java new file mode 100644 index 0000000000..223adddad7 --- /dev/null +++ b/examples/runtime/predicates.java @@ -0,0 +1,39 @@ +public class Main { + + //@ requires c != null ** c.state(0); + //@ ensures c.state(2); + void foo(Counter c) { + c.increment(2); + } + + public void execute() { + Counter c = new Counter(); + //@ fold c.state(0); + Counter c2 = new Counter(); + //@ fold c2.state(0); + + foo(c); + foo(c2); + } + + public void main() { + Main m = new Main(); + m.execute(); + } +} + + +class Counter { + int count; + + //@ resource state(int val) = Perm(count, write) ** count == val; + + //@ requires state(count); + //@ ensures state(count); + void increment(int n) { + int z = count; + //@ unfold state(count); + count += n; + //@ fold state(count); + }; +} \ No newline at end of file diff --git a/examples/runtime/quantifiers.java b/examples/runtime/quantifiers.java new file mode 100644 index 0000000000..002231b731 --- /dev/null +++ b/examples/runtime/quantifiers.java @@ -0,0 +1,40 @@ +class Program { + int[] a; + int b; + + + /*@ + requires (\forall* int i; 0 <= i && i < a.length; Perm(a[i], write)); + */ + public void setA(int[] a) { + this.a = a; + } + + /*@ + requires a.length > 0; + requires (\forall* int x; 0 <= x && x < a.length; Perm(a[x], write)); + requires (\forall int x; 0 <= x && x < a.length; a[x] > 0); + requires (\forall int x; 0 <= x && x < a.length; (\forall int j; 0 <= j && j < x; a[j] >= a[x])); + ensures (\forall* int x; 0 <= x && x < a.length; Perm(a[x], write)); + ensures (\exists int x; 0 <= x && x < a.length; a[x] > 0); + */ + //ensures (\exists int x; 0 <= x && x < a.length; a[x] == b) ==> \result >= 0; + public int indexOf(int b) { + for (int i = 0; i < a.length; i++) { + if (a[i] == b) { + return i; + } + } + return -1; + } + + public void main() { + Program program = new Program(); + int[] tmp = new int[3]; + tmp[0] = 2; + tmp[1] = 4; + tmp[2] = 6; + program.setA(tmp); + program.indexOf(4); + } +} \ No newline at end of file diff --git a/examples/runtime/sinksource.java b/examples/runtime/sinksource.java new file mode 100644 index 0000000000..9824e04bd1 --- /dev/null +++ b/examples/runtime/sinksource.java @@ -0,0 +1,62 @@ +import java.util.*; + + +class Source extends Thread { + int i; + + /*@ + requires Perm(this.i, 1); + ensures Perm(this.i, 1); + */ + public void run() { + i = 42; + } + + public void join(){} + public void start(){} +} + +class Sink extends Thread { + Source source; + + public void setSource(Source source) { + this.source = source; + } + + /*@ + requires Perm(source, 1); + ensures Perm(source, 1); + ensures Perm(source.i, 1/2); + */ + public void run() { + + //@ source.postJoin(1\2); + source.join(); + source.i = 1; + } + + public void join(){} + public void start(){} +} + +class Main{ + + public void main() { + Source source = new Source(); + Sink sink = new Sink(); + sink.setSource(source); + + sink.source.i = 1; + source.start(); + sink.start(); + //@ source.postJoin(1\2); + source.join(); + //@ sink.postJoin(1); + sink.join(); + source.i = 1988; + } +} + +class Thread{ + +} \ No newline at end of file diff --git a/examples/runtime/sinksourcearray.java b/examples/runtime/sinksourcearray.java new file mode 100644 index 0000000000..be49660eab --- /dev/null +++ b/examples/runtime/sinksourcearray.java @@ -0,0 +1,67 @@ +class Source extends Thread { + int[] i; + + public void createI() { + this.i = new int[2]; + } + + /*@ + requires Perm(this.i, 1); + requires (\forall* int j; 0 <= j && j < i.length; Perm(i[j], write)); + ensures Perm(this.i, 1); + ensures (\forall* int j; 0 <= j && j < i.length; Perm(i[j], write)); + */ + public void run() { + i[0] = 42; + i[1] = 43; + } + + + public void join(){} + public void start(){} +} + +class Sink extends Thread { + Source source; + + public void setSource(Source source) { + this.source = source; + } + + /*@ + requires Perm(source, 1); + ensures Perm(source, 1); + ensures Perm(source.i, 1/2); + ensures (\forall* int j; 0 <= j && j < source.i.length ==> Perm(source.i[j], 1/2)); + */ + public void run() { + //@ source.postJoin(1\2); + source.join(); + source.i[0] = 1; + } + + public void join(){} + public void start(){} +} + +class Main{ + + public void main() { + Source source = new Source(); + Sink sink = new Sink(); + sink.setSource(source); + source.createI(); + + source.start(); + sink.start(); + //@ source.postJoin(1/2); + source.join(); + //@ sink.postJoin(1); + sink.join(); + source.i[0] = 1988; + } +} + +class Thread{ + +} \ No newline at end of file diff --git a/examples/runtime/sinksourcearrayobjects.java b/examples/runtime/sinksourcearrayobjects.java new file mode 100644 index 0000000000..def6a9bd4e --- /dev/null +++ b/examples/runtime/sinksourcearrayobjects.java @@ -0,0 +1,30 @@ +class DummyData { + int val; +} + +class Source { + DummyData[] i; + + public void createI() { + this.i = new DummyData[2]; + DummyData o = new DummyData(); + this.i[0] = o; + this.i[1] = o; + } + + /*@ + requires Perm(this.i, 1); + requires (\forall* int j; 0 <= j && j < i.length; Perm(i[j].val, write)); + ensures Perm(this.i, 1); + ensures (\forall* int j; 0 <= j && j < i.length; Perm(i[j].val, write)); + */ + public void test() { + + } + + public void main(){ + Source source = new Source(); + source.createI(); + source.test(); + } +} diff --git a/examples/runtime/test.java b/examples/runtime/test.java new file mode 100644 index 0000000000..cff9210659 --- /dev/null +++ b/examples/runtime/test.java @@ -0,0 +1,58 @@ +class Source extends Thread { + int i; + + /*@ + requires Perm(this.i, 1); + ensures Perm(this.i, 1); + */ + public void run() { + i = 42; + } + + public void join(){} + public void start(){} +} + +class Sink extends Thread { + Source source; + + public void setSource(Source source) { + this.source = source; + } + + /*@ + requires Perm(source, 1); + ensures Perm(source, 1); + ensures Perm(source.i, 1/2); + */ + public void run() { + + //@ source.postJoin(1\2); + source.join(); + source.i = 1; + } + + public void join(){} + public void start(){} +} + +class Main{ + + public void main() { + Source source = new Source(); + Sink sink = new Sink(); + sink.setSource(source); + + source.start(); + sink.start(); + //@ source.postJoin(1\2); + source.join(); + //@ sink.postJoin(1); + sink.join(); + source.i = 1988; + } +} + +class Thread{ + +} \ No newline at end of file diff --git a/examples/runtime/testquantifiers.java b/examples/runtime/testquantifiers.java new file mode 100644 index 0000000000..e3908decea --- /dev/null +++ b/examples/runtime/testquantifiers.java @@ -0,0 +1,36 @@ +class Source extends Thread { + int[] a; + + //@ resource state() = Perm(this.a, 1) **(\forall* int i; 0 < i && i < a.length; Perm(a[i], write)); + + + /*@ + requires this.state(); + */ + public void run() { + + } + + public void start() { + + } + + public void join() { + + } +} + +class Main { + + public void main() { + Source source = new Source(); + source.start(); + + //@ source.postJoin(1); + source.join(); + } +} + +class Thread{ + +} \ No newline at end of file diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 14c71119e7..16959b365c 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -70,6 +70,7 @@ import vct.col.ast.lang.pvl._ import vct.col.ast.lang.silver._ import vct.col.ast.lang.smt._ import vct.col.ast.lang.sycl._ +import vct.col.ast.lang.runtime._ import vct.col.ast.node._ import vct.col.ast.statement._ import vct.col.ast.statement.behavior.ExpressionContainerStatementImpl @@ -86,6 +87,8 @@ import vct.col.resolve.ctx._ import vct.col.resolve.lang.JavaAnnotationData import vct.col.structure.{family, scopes} +import scala.collection.mutable.ArrayBuffer + /** @inheritdoc */ sealed trait Node[G] extends NodeImpl[G] sealed trait NodeFamily[G] extends Node[G] with NodeFamilyImpl[G] @@ -238,7 +241,8 @@ final case class Branch[G](branches: Seq[(Expr[G], Statement[G])])(implicit val final case class IndetBranch[G](branches: Seq[Statement[G]])(implicit val o: Origin) extends CompositeStatement[G] with ControlContainerStatement[G] with IndetBranchImpl[G] final case class Switch[G](expr: Expr[G], body: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with ControlContainerStatement[G] with SwitchImpl[G] @scopes[SendDecl] final case class Loop[G](init: Statement[G], cond: Expr[G], update: Statement[G], contract: LoopContract[G], body: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with ControlContainerStatement[G] with LoopImpl[G] -@scopes[Variable] final case class RangedFor[G](iter: IterVariable[G], contract: LoopContract[G], body: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with Declarator[G] with ControlContainerStatement[G] with RangedForImpl[G] +@scopes[Variable] final case class EnhancedLoop[G](arg: Variable[G], iter: Expr[G], body: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with EnhancedLoopImpl[G] +final case class RangedFor[G](iter: IterVariable[G], contract: LoopContract[G], body: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with Declarator[G] with ControlContainerStatement[G] with RangedForImpl[G] final case class TryCatchFinally[G](body: Statement[G], after: Statement[G], catches: Seq[CatchClause[G]])(implicit val o: Origin) extends CompositeStatement[G] with ControlContainerStatement[G] with TryCatchFinallyImpl[G] final case class Synchronized[G](obj: Expr[G], body: Statement[G])(val blame: Blame[LockRegionFailure])(implicit val o: Origin) extends CompositeStatement[G] with ControlContainerStatement[G] with SynchronizedImpl[G] @scopes[ParInvariantDecl] final case class ParInvariant[G](decl: ParInvariantDecl[G], inv: Expr[G], content: Statement[G])(val blame: Blame[ParInvariantNotEstablished])(implicit val o: Origin) extends CompositeStatement[G] with ControlContainerStatement[G] with ParInvariantImpl[G] @@ -287,16 +291,23 @@ case class Boogie[G]()(implicit val o: Origin) extends ProverLanguage[G] with Bo extends ClassDeclaration[G] with AbstractFunction[G] with InstanceFunctionImpl[G] @scopes[LabelDecl] final class Constructor[G](val cls: Ref[G, Class[G]], val args: Seq[Variable[G]], val outArgs: Seq[Variable[G]], val typeArgs: Seq[Variable[G]], val body: Option[Statement[G]], val contract: ApplicableContract[G], val inline: Boolean = false)(val blame: Blame[CallableFailure])(implicit val o: Origin) extends ClassDeclaration[G] with AbstractMethod[G] with ConstructorImpl[G] @scopes[LabelDecl] final class InstanceMethod[G](val returnType: Type[G], - val args: Seq[Variable[G]], val outArgs: Seq[Variable[G]], val typeArgs: Seq[Variable[G]], + val args: Seq[Variable[G]], + val outArgs: Seq[Variable[G]], + val typeArgs: Seq[Variable[G]], val body: Option[Statement[G]], val contract: ApplicableContract[G], - val inline: Boolean = false, val pure: Boolean = false) + val inline: Boolean = false, + val pure: Boolean = false, + val static: Boolean = false, +// val public: Boolean = false, +// val overriding: Boolean = false + ) (val blame: Blame[CallableFailure])(implicit val o: Origin) extends ClassDeclaration[G] with AbstractMethod[G] with InstanceMethodImpl[G] @scopes[Variable] final class InstancePredicate[G](val args: Seq[Variable[G]], val body: Option[Expr[G]], val threadLocal: Boolean = false, val inline: Boolean = false)(implicit val o: Origin) extends ClassDeclaration[G] with AbstractPredicate[G] with InstancePredicateImpl[G] -final class InstanceField[G](val t: Type[G], val flags: Seq[FieldFlag[G]])(implicit val o: Origin) extends ClassDeclaration[G] with Field[G] with InstanceFieldImpl[G] +final class InstanceField[G](val t: Type[G], val flags: Seq[FieldFlag[G]], val value: Option[Expr[G]] = None)(implicit val o: Origin) extends ClassDeclaration[G] with Field[G] with InstanceFieldImpl[G] final class RunMethod[G](val body: Option[Statement[G]], val contract: ApplicableContract[G])(val blame: Blame[CallableFailure])(implicit val o: Origin) extends ClassDeclaration[G] with RunMethodImpl[G] final class InstanceOperatorFunction[G](val returnType: Type[G], val operator: Operator[G], val args: Seq[Variable[G]], val body: Option[Expr[G]], val contract: ApplicableContract[G], @@ -363,6 +374,7 @@ case class SplitAccountedPredicate[G](left: AccountedPredicate[G], right: Accoun @family sealed trait FieldFlag[G] extends NodeFamily[G] with FieldFlagImpl[G] final case class Final[G]()(implicit val o: Origin) extends FieldFlag[G] with FinalImpl[G] +final case class Static[G]()(implicit val o: Origin) extends FieldFlag[G] with StaticImpl[G] @family sealed trait Coercion[G] extends NodeFamily[G] with CoercionImpl[G] final case class CoerceIdentity[G](source: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceIdentityImpl[G] @@ -1395,4 +1407,90 @@ sealed trait SilverDeclaration[G] extends GlobalDeclaration[G] with SilverDeclar final class SilverField[G](val t: Type[G])(implicit val o: Origin) extends SilverDeclaration[G] with SilverFieldImpl[G] sealed trait SilverType[G] extends Type[G] with SilverTypeImpl[G] -case class SilverPartialTAxiomatic[G](ref: Ref[G, AxiomaticDataType[G]], partialTypeArgs: Seq[(Ref[G, Variable[G]], Type[G])])(implicit val o: Origin = DiagnosticOrigin) extends SilverType[G] with SilverPartialTAxiomaticImpl[G] \ No newline at end of file +case class SilverPartialTAxiomatic[G](ref: Ref[G, AxiomaticDataType[G]], partialTypeArgs: Seq[(Ref[G, Variable[G]], Type[G])])(implicit val o: Origin = DiagnosticOrigin) extends SilverType[G] with SilverPartialTAxiomaticImpl[G] + + +sealed trait CodeString[G] extends Node[G] with CodeStringImpl[G] { + val content: String +} + +final case class CodeStringGlobal[G](content: String)(implicit val o: Origin) extends GlobalDeclaration[G] with CodeString[G] with CodeStringGlobalImpl[G] +final case class CodeStringClass[G](content: String, ref: String)(implicit val o: Origin) extends ClassDeclaration[G] with CodeString[G] with CodeStringClassImpl[G] +final case class CodeStringStatement[G](content: String)(implicit val o: Origin) extends Statement[G] with CodeString[G] with CodeStringStatementImpl[G] + +final case class CodeStringQuantifier[G](quantifier: Expr[G], lowerBound: Expr[G], condition: Expr[G], body: Statement[G])(implicit val o: Origin) extends Statement[G] with CodeStringQuantifierImpl[G] +final case class CodeStringQuantifierCall[G](obj: Expr[G], quantifierId: String, ref: Ref[G, CodeStringQuantifierMethod[G]], args: Seq[Expr[G]])(val blame: Blame[InstanceInvocationFailure])(implicit val o: Origin) extends AnyMethodInvocation[G] with InstanceApply[G] with CodeStringQuantifierCallImpl[G] +final class CodeStringQuantifierMethod[G](val quantifierId: String, val args: Seq[Variable[G]], val body: Option[Statement[G]])(val blame: Blame[CallableFailure])(implicit val o: Origin) extends ClassDeclaration[G] with AbstractMethod[G] with CodeStringQuantifierMethodImpl[G] + +final class CodeStringPredicateConstructor[G](val args: Seq[Variable[G]], val body: Option[Statement[G]])(implicit val o: Origin) extends ClassDeclaration[G] with CodeStringPredicateConstructorImpl[G] + +final case class JavaLocalRuntime[G](ref: Ref[G, JavaParam[G]])(val blame: Blame[DerefInsufficientPermission])(implicit val o: Origin) extends JavaExpr[G] with JavaLocalRuntimeImpl[G] + +final case class CodeStringGetPredicate[G](args: Seq[Expr[G]], cls: Ref[G, Class[G]])(implicit val o: Origin) extends Statement[G] with CodeStringGetPredicateImpl[G] +final case class RuntimeNewPredicate[G](cls: Ref[G, Class[G]], args: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with RuntimeNewPredicateImpl[G] +final case class Equals[G](obj: Expr[G], target: Expr[G])(implicit val o: Origin) extends Expr[G] with EqualsImpl[G] + + +final case class GetPermission[G](objectLocation: Expr[G], id: Int, threadId: Expr[G])(implicit val o: Origin) extends Expr[G] with GetPermissionImpl[G] +final case class GetArrayPermission[G](objectLocation: Expr[G], id: Int, location: Expr[G], threadId: Expr[G])(implicit val o: Origin) extends Expr[G] with GetArrayPermissionImpl[G] +final case class PutPermission[G](objectLocation: Expr[G], id: Int, permission: Expr[G], threadId: Expr[G])(implicit val o: Origin) extends Expr[G] with PutPermissionImpl[G] +final case class PutArrayPermission[G](objectLocation: Expr[G], id: Int, location: Expr[G], permission: Expr[G], threadId: Expr[G])(implicit val o: Origin) extends Expr[G] with PutArrayPermissionImpl[G] +final case class RuntimePermission[G](permission: Expr[G])(implicit val o: Origin) extends Expr[G] with RuntimePermissionImpl[G] + + +final case class TRuntimeFraction[G]()(implicit val o: Origin = DiagnosticOrigin) extends NumericType[G] with TRuntimeFractionImpl[G] + +sealed trait RuntimeFractionExpression[G] extends Expr[G] + +sealed trait RuntimeFractionCreation[G] extends RuntimeFractionExpression[G] +final case class RuntimeFractionDiff[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends RuntimeFractionCreation[G] with RuntimeFractionDiffImpl[G] +final case class RuntimeFractionZero[G]()(implicit val o: Origin) extends RuntimeFractionCreation[G] with RuntimeFractionZeroImpl[G] +final case class RuntimeFractionOne[G]()(implicit val o: Origin) extends RuntimeFractionCreation[G] with RuntimeFractionOneImpl[G] + +sealed trait RuntimeFractionOperations[G] extends RuntimeFractionExpression[G] +final case class RuntimeFractionAdd[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends RuntimeFractionOperations[G] with RuntimeFractionAddImpl[G] +final case class RuntimeFractionSubstract[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends RuntimeFractionOperations[G] with RuntimeFractionSubstractImpl[G] +final case class RuntimeFractionMultiply[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends RuntimeFractionOperations[G] with RuntimeFractionMultiplyImpl[G] +final case class RuntimeFractionCompare[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends RuntimeFractionOperations[G] with RuntimeFractionCompareImpl[G] + +final case class RuntimePostJoin[G](obj: Expr[G], arg: Expr[G])(val blame: Blame[AssertFailed])(implicit val o: Origin) extends NormallyCompletingStatement[G] with RuntimePostJoinImpl[G] +final case class ThreadId[G](obj: Option[Expr[G]])(implicit val o: Origin) extends Expr[G] with ThreadIdImpl[G] + +final case class StaticClassRef[G](cls: Ref[G, Class[G]])(implicit val o: Origin) extends Expr[G] with StaticClassRefImpl[G] + +final case class RuntimeAssert[G](res: Expr[G], message: String)(val blame: Blame[AssertFailed])(implicit val o: Origin) extends NormallyCompletingStatement[G] with RuntimeAssertImpl[G] +final case class RuntimeAssertExpected[G](res: Expr[G], expected: Expr[G], received: Expr[G], message: String)(val blame: Blame[AssertFailed])(implicit val o: Origin) extends NormallyCompletingStatement[G] with RuntimeAssertExpectedImpl[G] + +final case class TLong[G]()(implicit val o: Origin = DiagnosticOrigin) extends NumericType[G] with TLongImpl[G] +final case class TLongObject[G]()(implicit val o: Origin = DiagnosticOrigin) extends NumericType[G] with TLongObjectImpl[G] +final case class TIntObject[G]()(implicit val o: Origin = DiagnosticOrigin) extends NumericType[G] with TIntObjectImpl[G] + +final case class RuntimeConcurrentHashMap[G](keyType: Type[G], valueType: Type[G])(implicit val o: Origin) extends DeclaredType[G] with RuntimeConcurrentHashMapImpl[G] +final case class RuntimeNewConcurrentHashMap[G](t: Type[G])(implicit val o: Origin) extends Expr[G] with RuntimeNewConcurrentHashMapImpl[G] +sealed trait RuntimeConcurrentHashMapFunctions[G] extends Expr[G] +final case class RuntimeConcurrentHashMapGet[G](hm: Expr[G], key: Expr[G])(implicit val o: Origin) extends RuntimeConcurrentHashMapFunctions[G] with RuntimeConcurrentHashMapGetImpl[G] +final case class RuntimeConcurrentHashMapGetOrDefault[G](hm: Expr[G], key: Expr[G], default: Expr[G])(implicit val o: Origin) extends RuntimeConcurrentHashMapFunctions[G] with RuntimeConcurrentHashMapGetOrDefaultImpl[G] +final case class RuntimeConcurrentHashMapPut[G](hm: Expr[G], key: Expr[G], value: Expr[G])(implicit val o: Origin) extends RuntimeConcurrentHashMapFunctions[G] with RuntimeConcurrentHashMapPutImpl[G] +final case class RuntimeConcurrentHashMapContainsKey[G](hm: Expr[G], key: Expr[G])(implicit val o: Origin) extends RuntimeConcurrentHashMapFunctions[G] with RuntimeConcurrentHashMapContainsKeyImpl[G] +final case class RuntimeConcurrentHashMapKeySet[G](hm: Expr[G])(implicit val o: Origin) extends RuntimeConcurrentHashMapFunctions[G] with RuntimeConcurrentHashMapKeySetImpl[G] + +final case class CopyOnWriteArrayList[G](listType: Type[G])(implicit val o: Origin) extends DeclaredType[G] with CopyOnWriteArrayListImpl[G] +final case class CopyOnWriteArrayListNew[G](t: Type[G])(implicit val o: Origin) extends Expr[G] with CopyOnWriteArrayListNewImpl[G] +final case class CopyOnWriteArrayListAdd[G](obj: Expr[G], arg: Expr[G])(implicit val o: Origin) extends Expr[G] with CopyOnWriteArrayListAddImpl[G] +final case class CopyOnWriteArrayListRemove[G](obj: Expr[G], arg: Expr[G])(implicit val o: Origin) extends Expr[G] with CopyOnWriteArrayListRemoveImpl[G] +final case class CopyOnWriteArrayListContains[G](obj: Expr[G], arg: Expr[G])(implicit val o: Origin) extends Expr[G] with CopyOnWriteArrayListContainsImpl[G] + + +final case class PredicateStore[G](storeType: Type[G])(implicit val o: Origin) extends ClassDeclaration[G] with PredicateStoreImpl[G] +final case class PredicateStoreGet[G](cls: Ref[G, Class[G]], threadId: Expr[G])(implicit val o: Origin) extends Expr[G] with PredicateStoreGetImpl[G] + +final case class ObjectIsArray[G](input: Expr[G])(implicit val o: Origin) extends Expr[G] with ObjectIsArrayImpl[G] +final case class ObjectGetLength[G](input: Expr[G])(implicit val o: Origin) extends Expr[G] with ObjectGetLengthImpl[G] +final case class CreateObjectArray[G](args: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with CreateObjectArrayImpl[G] + +final case class CoerceTArrayAnyClass[G]()(implicit val o: Origin) extends Coercion[G] with CoerceTArrayAnyClassImpl[G] + +final case class ArraysEquals[G](obj: Expr[G], target: Expr[G])(implicit val o: Origin) extends Expr[G] with ArraysEqualsImpl[G] +final case class ArraysHashCode[G](obj: Expr[G])(implicit val o: Origin) extends Expr[G] with ArraysHashCodeImpl[G] + +final case class GetClassCall[G](obj: Option[Expr[G]])(implicit val o: Origin) extends Expr[G] with GetClassCallImpl[G] \ No newline at end of file diff --git a/src/col/vct/col/ast/declaration/cls/InstanceFieldImpl.scala b/src/col/vct/col/ast/declaration/cls/InstanceFieldImpl.scala index c09a274a08..ebaf11d48d 100644 --- a/src/col/vct/col/ast/declaration/cls/InstanceFieldImpl.scala +++ b/src/col/vct/col/ast/declaration/cls/InstanceFieldImpl.scala @@ -1,12 +1,19 @@ package vct.col.ast.declaration.cls -import vct.col.ast.{Final, InstanceField} +import vct.col.ast.{Expr, Final, InstanceField} import vct.col.print._ import vct.col.ast.ops.InstanceFieldOps trait InstanceFieldImpl[G] extends InstanceFieldOps[G] { this: InstanceField[G] => def isFinal = flags.collectFirst { case _: Final[G] => () }.isDefined + def getValue(implicit ctx: Ctx): Doc = { + value match { + case Some(e: Expr[G]) => Text(" =") <+> e.show + case None => Empty + } + } + override def layout(implicit ctx: Ctx): Doc = - Doc.rspread(flags) <> t.show <+> ctx.name(this) <> ";" + Doc.rspread(flags) <> t.show <+> ctx.name(this) <> getValue <> ";" } \ No newline at end of file diff --git a/src/col/vct/col/ast/declaration/cls/InstanceMethodImpl.scala b/src/col/vct/col/ast/declaration/cls/InstanceMethodImpl.scala index 56bd2551b2..49cfd04d72 100644 --- a/src/col/vct/col/ast/declaration/cls/InstanceMethodImpl.scala +++ b/src/col/vct/col/ast/declaration/cls/InstanceMethodImpl.scala @@ -12,7 +12,8 @@ trait InstanceMethodImpl[G] extends ClassDeclarationImpl[G] with AbstractMethodI def layoutModifiers(implicit ctx: Ctx): Seq[Doc] = ListMap( pure -> "pure", inline -> "inline", - ).filter(_._1).values.map(Text).map(Doc.inlineSpec).toSeq + static -> "static" + ).filter(_._1).values.map(Text).toSeq private def layoutNameAndArgs(implicit ctx: Ctx): Doc = ctx.syntax match { case Ctx.Java => diff --git a/src/col/vct/col/ast/declaration/cls/InstancePredicateImpl.scala b/src/col/vct/col/ast/declaration/cls/InstancePredicateImpl.scala index 8452b3c796..432c31268c 100644 --- a/src/col/vct/col/ast/declaration/cls/InstancePredicateImpl.scala +++ b/src/col/vct/col/ast/declaration/cls/InstancePredicateImpl.scala @@ -13,8 +13,9 @@ trait InstancePredicateImpl[G] extends ClassDeclarationImpl[G] with AbstractPred threadLocal -> "thread_local", ).filter(_._1).values.map(Text).map(Doc.inlineSpec).toSeq - override def layout(implicit ctx: Ctx): Doc = Group( - Doc.rspread(layoutModifiers) <> "resource" <+> ctx.name(this) <> "(" <> Doc.args(args) <> ")" <> - body.map(Text(" =") <>> _ <> ";").getOrElse(Text(";")) - ) + override def layout(implicit ctx: Ctx): Doc = + Doc.spec(Group( + Doc.rspread(layoutModifiers) <> "resource" <+> ctx.name(this) <> "(" <> Doc.args(args) <> ")" <> + body.map(Text(" =") <>> _ <> ";").getOrElse(Text(";")) + )) } \ No newline at end of file diff --git a/src/col/vct/col/ast/declaration/global/ClassImpl.scala b/src/col/vct/col/ast/declaration/global/ClassImpl.scala index 33ae5dfaba..d1b267ee1c 100644 --- a/src/col/vct/col/ast/declaration/global/ClassImpl.scala +++ b/src/col/vct/col/ast/declaration/global/ClassImpl.scala @@ -2,10 +2,15 @@ package vct.col.ast.declaration.global import vct.col.ast.{Class, Declaration, TClass, TVar} import vct.col.ast.util.Declarator +import vct.col.origin.{JavaLibrary, PositionRange, ReadableOrigin, SourceName} import vct.col.print._ +import vct.col.ref.Ref import vct.col.util.AstBuildHelpers.tt import vct.result.VerificationError.Unreachable import vct.col.ast.ops.ClassOps +import vct.col.resolve.lang.Java.JRESource + +import scala.util.matching.Regex trait ClassImpl[G] extends Declarator[G] with ClassOps[G] { this: Class[G] => def transSupportArrowsHelper(seen: Set[TClass[G]]): Seq[(TClass[G], TClass[G])] = { @@ -24,15 +29,75 @@ trait ClassImpl[G] extends Declarator[G] with ClassOps[G] { this: Class[G] => def layoutLockInvariant(implicit ctx: Ctx): Doc = Text("lock_invariant") <+> intrinsicLockInvariant <> ";" <+/> Empty - override def layout(implicit ctx: Ctx): Doc = - (if(intrinsicLockInvariant == tt[G]) Empty else Doc.spec(Show.lazily(layoutLockInvariant(_)))) <> - Group( - Text("class") <+> ctx.name(this) <> - (if (typeArgs.nonEmpty) Text("<") <> Doc.args(typeArgs) <> ">" else Empty) <> - (if(supports.isEmpty) Empty else Text(" implements") <+> - Doc.args(supports.map(supp => ctx.name(supp.asClass.get.cls)).map(Text))) <+> - "{" - ) <>> - Doc.stack(decls) <+/> - "}" + private def searchInClassDeclaration(regex: Regex): Doc = { + val readableOrigin = this.o.getReadable + readableOrigin match { + case Some(ro: ReadableOrigin) => + val rangeContent = o.get[PositionRange] + val range = rangeContent.startLineIdx to rangeContent.endLineIdx + val res = range.collectFirst { + case index: Int if regex.findFirstMatchIn(ro.readable.readLines()(index)).nonEmpty => Text(regex.findFirstMatchIn(ro.readable.readLines()(index)).get.toString()) + } + res.getOrElse(Empty) + case None => Empty + } + } + + def classOrInterfaceDoc(): Doc = + searchInClassDeclaration(new Regex("(class|interface)")) + + def implementsDoc(): Doc = + searchInClassDeclaration(new Regex("implements(\\s+[A-Z][A-Za-z]*,?)*")) + + def extendsDoc(): Doc = + searchInClassDeclaration(new Regex("extends\\s+[A-Z][A-Za-z]*")) + + def implementsRef(): Option[Seq[Ref[G, Class[G]]]] = { + this.implementsDoc() match { + case Text(s) => + val names = s.replaceAll("implements\\s+", "").split(",\\s+") + Some(this.supports.collect { + case TClass(ref @ Ref(cls), _) if names.contains(cls.o.find[SourceName].map(_.name).getOrElse("~")) => ref + }) + case _ => None + } + } + + def extendsRef(): Option[Ref[G, Class[G]]] = { + this.extendsDoc() match { + case Text(s) => + val name = s.replaceAll("extends\\s+","") + this.supports.collectFirst { + case TClass(ref @ Ref(cls), _) if cls.o.find[SourceName].map(_.name).getOrElse("~") == name => ref + } + case _ => None + } + } + + def fromLibrary(): Boolean = + o.find[JavaLibrary.type].nonEmpty || o.find[JRESource.type].nonEmpty + + override def layout(implicit ctx: Ctx): Doc = { + val classOrInterface = classOrInterfaceDoc() match { + case Empty => Text("class") + case e => e + } + val extension = extendsDoc() + val implements = implementsDoc() + + if (fromLibrary()) { + Empty + } else { + (if(intrinsicLockInvariant == tt[G]) Empty else Doc.spec(Show.lazily(layoutLockInvariant(_)))) <> + Group( + Text("class") <+> ctx.name(this) <> + (if (typeArgs.nonEmpty) Text("<") <> Doc.args(typeArgs) <> ">" else Empty) <> + (if(supports.isEmpty) Empty else Text(" implements") <+> + Doc.args(supports.map(supp => ctx.name(supp.asClass.get.cls)).map(Text))) <+> + "{" + ) <>> + Doc.stack(decls) <+/> + "}" + } + } } \ No newline at end of file diff --git a/src/col/vct/col/ast/expr/heap/alloc/NewArrayImpl.scala b/src/col/vct/col/ast/expr/heap/alloc/NewArrayImpl.scala index 532cb8860d..69e86db022 100644 --- a/src/col/vct/col/ast/expr/heap/alloc/NewArrayImpl.scala +++ b/src/col/vct/col/ast/expr/heap/alloc/NewArrayImpl.scala @@ -10,5 +10,5 @@ trait NewArrayImpl[G] extends NewArrayOps[G] { this: NewArray[G] => override def precedence: Int = Precedence.POSTFIX override def layout(implicit ctx: Ctx): Doc = - Text("new") <+> element <> dims.map(dim => s"[$dim]").mkString <> "[]".repeat(moreDims) + Text("new") <+> element <> Doc.fold(dims.map(dim => Text("[") <> dim <> "]"))(_ <> _) <> "[]".repeat(moreDims) } \ No newline at end of file diff --git a/src/col/vct/col/ast/expr/type/CastImpl.scala b/src/col/vct/col/ast/expr/type/CastImpl.scala index 69d9cf5c5e..39732300a8 100644 --- a/src/col/vct/col/ast/expr/type/CastImpl.scala +++ b/src/col/vct/col/ast/expr/type/CastImpl.scala @@ -8,10 +8,11 @@ import vct.col.ast.ops.CastOps trait CastImpl[G] extends CastOps[G] { this: Cast[G] => override def t: Type[G] = typeValue.t match { case TType(t) => t - case _ => throw UnreachableAfterTypeCheck("The cast type is not a type", this) + case t => t +// case _ => throw UnreachableAfterTypeCheck("The cast type is not a type", this) } override def precedence: Int = Precedence.PREFIX override def layout(implicit ctx: Ctx): Doc = - Text("(") <> typeValue <> ")" <> assoc(value) + Text("(") <> typeValue <> ")" <+> assoc(value) } \ No newline at end of file diff --git a/src/col/vct/col/ast/family/coercion/CoerceTArrayAnyClassImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceTArrayAnyClassImpl.scala new file mode 100644 index 0000000000..ccaee644b7 --- /dev/null +++ b/src/col/vct/col/ast/family/coercion/CoerceTArrayAnyClassImpl.scala @@ -0,0 +1,8 @@ +package vct.col.ast.family.coercion + +import vct.col.ast.{CoerceTArrayAnyClass, TAnyClass} +import vct.col.ast.ops.CoerceTArrayAnyClassOps + +trait CoerceTArrayAnyClassImpl[G] extends CoerceTArrayAnyClassOps[G] { this: CoerceTArrayAnyClass[G] => + override def target: TAnyClass[G] = TAnyClass() +} diff --git a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala b/src/col/vct/col/ast/family/coercion/CoercionImpl.scala index 768278bfa0..208337f253 100644 --- a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoercionImpl.scala @@ -38,6 +38,7 @@ trait CoercionImpl[G] extends CoercionFamilyOps[G] { this: Coercion[G] => case CoerceNullClass(_, _) => true case CoerceNullJavaClass(_) => true case CoerceNullAnyClass() => true + case CoerceTArrayAnyClass() => true case CoerceNullPointer(_) => true case CoerceNullEnum(_) => true case CoerceFracZFrac() => true diff --git a/src/col/vct/col/ast/family/contract/ApplicableContractImpl.scala b/src/col/vct/col/ast/family/contract/ApplicableContractImpl.scala index 71c0f49fcc..f3ee9c88e8 100644 --- a/src/col/vct/col/ast/family/contract/ApplicableContractImpl.scala +++ b/src/col/vct/col/ast/family/contract/ApplicableContractImpl.scala @@ -55,4 +55,5 @@ trait ApplicableContractImpl[G] extends NodeFamilyImpl[G] with ApplicableContrac case Ctx.Silver => layoutSilver case _ => Doc.spec(Show.lazily(layoutSpec(_))) } + } \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/java/JavaImportImpl.scala b/src/col/vct/col/ast/lang/java/JavaImportImpl.scala index c81762943c..4da6ce5806 100644 --- a/src/col/vct/col/ast/lang/java/JavaImportImpl.scala +++ b/src/col/vct/col/ast/lang/java/JavaImportImpl.scala @@ -7,5 +7,5 @@ import vct.col.ast.ops.{JavaImportOps, JavaImportFamilyOps} trait JavaImportImpl[G] extends JavaImportOps[G] with JavaImportFamilyOps[G] { this: JavaImport[G] => override def layout(implicit ctx: Ctx): Doc = Text(if(isStatic) "import static" else "import") <+> - name <> (if(star) Text(".*") else Empty) + name <> (if(star) Text(".*") else Empty) <> ";" } \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/java/JavaNamespaceImpl.scala b/src/col/vct/col/ast/lang/java/JavaNamespaceImpl.scala index 6684378feb..84c568847a 100644 --- a/src/col/vct/col/ast/lang/java/JavaNamespaceImpl.scala +++ b/src/col/vct/col/ast/lang/java/JavaNamespaceImpl.scala @@ -14,7 +14,7 @@ trait JavaNamespaceImpl[G] extends JavaNamespaceOps[G] { this: JavaNamespace[G] override def layout(implicit ctx: Ctx): Doc = Doc.stack(Seq( - if(pkg.isEmpty) Empty else Text("package") <+> pkg.get, + if(pkg.isEmpty) Empty else Text("package") <+> pkg.get <> ";", Doc.stack(imports), Doc.stack(declarations), )) diff --git a/src/col/vct/col/ast/lang/runtime/ArraysEqualsImpl.scala b/src/col/vct/col/ast/lang/runtime/ArraysEqualsImpl.scala new file mode 100644 index 0000000000..9c1875fc18 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/ArraysEqualsImpl.scala @@ -0,0 +1,14 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.ArraysEqualsOps + +trait ArraysEqualsImpl[G] extends ArraysEqualsOps[G] { + this: ArraysEquals[G] => + override def precedence: Int = Precedence.ATOMIC + + override val t: Type[G] = TBool[G]() + + override def layout(implicit ctx: Ctx): Doc = Text("Arrays.equals(") <> obj <> "," <+> target.show <> ")" +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/ArraysHashCodeImpl.scala b/src/col/vct/col/ast/lang/runtime/ArraysHashCodeImpl.scala new file mode 100644 index 0000000000..bbacee83eb --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/ArraysHashCodeImpl.scala @@ -0,0 +1,14 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.ArraysHashCodeOps + +trait ArraysHashCodeImpl[G] extends ArraysHashCodeOps[G] { + this: ArraysHashCode[G] => + override def precedence: Int = Precedence.ATOMIC + + override val t: Type[G] = TInt[G]() + + override def layout(implicit ctx: Ctx): Doc = Text("Arrays.hashCode(") <> obj <> ")" +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/CodeStringGetPredicateImpl.scala b/src/col/vct/col/ast/lang/runtime/CodeStringGetPredicateImpl.scala new file mode 100644 index 0000000000..b28e2f6d44 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/CodeStringGetPredicateImpl.scala @@ -0,0 +1,21 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print.{Ctx, Doc, Group, Text} +import vct.col.ast.ops.CodeStringGetPredicateOps + +trait CodeStringGetPredicateImpl[G] extends CodeStringGetPredicateOps[G] { + this: CodeStringGetPredicate[G] => + + def getClassTypeLower(implicit ctx: Ctx): Text = Text(ctx.name(cls).toLowerCase) + + override def layout(implicit ctx: Ctx): Doc = + Group( + Group(Text(ctx.name(cls)) <+> Text("tmp = new") <+> ctx.name(cls) <> "(" <+> Doc.args(args) <+> ");") <+/> + Group( + Group(Text("for(") <> ctx.name(cls) <+> getClassTypeLower <+> ": predicateStore.get(Thread.currentThread().threadId()))") <+> + Text("{") <>> Group(Text("if(tmp.equals(") <> getClassTypeLower <> ")) return" <+> getClassTypeLower <> ";") <+/> "}" <+/> + Text("return null;") + ) + ) +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/CodeStringImpl.scala b/src/col/vct/col/ast/lang/runtime/CodeStringImpl.scala new file mode 100644 index 0000000000..a0cdd67979 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/CodeStringImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast.CodeString +import vct.col.print.{Ctx, Doc, Text} + +trait CodeStringImpl[G] { + this: CodeString[G] => + override def layout(implicit ctx: Ctx): Doc = Text(content) + +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/CodeStringPredicateConstructorImpl.scala b/src/col/vct/col/ast/lang/runtime/CodeStringPredicateConstructorImpl.scala new file mode 100644 index 0000000000..fa67537234 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/CodeStringPredicateConstructorImpl.scala @@ -0,0 +1,12 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print.{Ctx, Doc, Text} +import vct.col.ast.ops.CodeStringPredicateConstructorOps + +trait CodeStringPredicateConstructorImpl[G] extends CodeStringPredicateConstructorOps[G] { + this: CodeStringPredicateConstructor[G] => + + override def layout(implicit ctx: Ctx): Doc = Text("predicate") + +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/CodeStringQuantifierCallImpl.scala b/src/col/vct/col/ast/lang/runtime/CodeStringQuantifierCallImpl.scala new file mode 100644 index 0000000000..5e7fe65536 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/CodeStringQuantifierCallImpl.scala @@ -0,0 +1,19 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print.{Ctx, Doc, Group} +import vct.col.ref.Ref +import vct.col.ast.ops.CodeStringQuantifierCallOps + +trait CodeStringQuantifierCallImpl[G] extends CodeStringQuantifierCallOps[G] { + this: CodeStringQuantifierCall[G] => + override def givenMap: Seq[(Ref[G, Variable[G]], Expr[G])] = Seq.empty + override def yields: Seq[(Expr[G], Ref[G, Variable[G]])] = Seq.empty + override def typeArgs: Seq[Type[G]] = Seq.empty + override def outArgs: Seq[Expr[G]] = Seq.empty + override def typeEnv: Map[Variable[G], Type[G]] = Map.empty + + override def layout(implicit ctx: Ctx): Doc = + Group(Group(assoc(obj) <> "." <> ctx.name(ref) <> "(" <> Doc.args(args ++ outArgs) <> ")")) + +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/CodeStringQuantifierImpl.scala b/src/col/vct/col/ast/lang/runtime/CodeStringQuantifierImpl.scala new file mode 100644 index 0000000000..70e35ce829 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/CodeStringQuantifierImpl.scala @@ -0,0 +1,20 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast.{CodeStringQuantifier, Local} +import vct.col.print.{Ctx, Doc, Group, Text} +import vct.col.ast.ops.CodeStringQuantifierOps +trait CodeStringQuantifierImpl[G] extends CodeStringQuantifierOps[G] { + this: CodeStringQuantifier[G] => + + def getName(implicit ctx: Ctx): Doc = + quantifier match { + case Local(ref) => Text(ctx.name(ref)) + case _ => quantifier.show + } + + override def layout(implicit ctx: Ctx): Doc = + Group(Text("for(") <> getName <+> Text("=") <+> this.lowerBound.show <> Text(";") + <+> getName <+> Text("<") <+> this.condition.show <> Text(";") + <+> getName <> Text("++)") <+> body.layoutAsBlock) + +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/CodeStringQuantifierMethodImpl.scala b/src/col/vct/col/ast/lang/runtime/CodeStringQuantifierMethodImpl.scala new file mode 100644 index 0000000000..a9fe1fdcfb --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/CodeStringQuantifierMethodImpl.scala @@ -0,0 +1,28 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print.{Ctx, Doc, Group, Text} +import vct.col.ast.ops.CodeStringQuantifierMethodOps +import vct.col.util.AstBuildHelpers + +trait CodeStringQuantifierMethodImpl[G] extends CodeStringQuantifierMethodOps[G] { + this: CodeStringQuantifierMethod[G] => + + override def pure: Boolean = false + override def inline: Boolean = false + override def outArgs: Seq[Variable[G]] = Seq.empty + override def contract: ApplicableContract[G] = AstBuildHelpers.contract(this.o) + override def typeArgs: Seq[Variable[G]] = Seq.empty + + override def returnType: Type[G] = TBool[G]() + + + override def layout(implicit ctx: Ctx): Doc = + Doc.stack(Seq( + contract, + Group(Group(Text(s"public boolean __runtime_quantifier__${this.quantifierId}") <> + "(" <> Doc.args(args) <> ")") <> + body.map(Text(" ") <> _.layoutAsBlock).getOrElse(Text(";")), + ))) + +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/CopyOnWriteArrayListAddImpl.scala b/src/col/vct/col/ast/lang/runtime/CopyOnWriteArrayListAddImpl.scala new file mode 100644 index 0000000000..3d24428007 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/CopyOnWriteArrayListAddImpl.scala @@ -0,0 +1,15 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.CopyOnWriteArrayListAddOps + +trait CopyOnWriteArrayListAddImpl[G] extends CopyOnWriteArrayListAddOps[G] { + this: CopyOnWriteArrayListAdd[G] => + + override def t: Type[G] = TBool[G]() + + override def layout(implicit ctx: Ctx): Doc = + obj.show <> Text(".add(") <> arg.show <> Text(")") + +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/CopyOnWriteArrayListContainsImpl.scala b/src/col/vct/col/ast/lang/runtime/CopyOnWriteArrayListContainsImpl.scala new file mode 100644 index 0000000000..33ce76861f --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/CopyOnWriteArrayListContainsImpl.scala @@ -0,0 +1,15 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.CopyOnWriteArrayListContainsOps + +trait CopyOnWriteArrayListContainsImpl[G] extends CopyOnWriteArrayListContainsOps[G] { + this: CopyOnWriteArrayListContains[G] => + + override def t: Type[G] = TBool[G]() + + override def layout(implicit ctx: Ctx): Doc = + obj.show <> Text(".contains(") <> arg.show <> Text(")") + +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/CopyOnWriteArrayListImpl.scala b/src/col/vct/col/ast/lang/runtime/CopyOnWriteArrayListImpl.scala new file mode 100644 index 0000000000..4ec6f0c795 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/CopyOnWriteArrayListImpl.scala @@ -0,0 +1,12 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.CopyOnWriteArrayListOps + +trait CopyOnWriteArrayListImpl[G] extends CopyOnWriteArrayListOps[G] { + this: CopyOnWriteArrayList[G] => + + override def layout(implicit ctx: Ctx): Doc = Text("ArrayList<") <> listType.show <> ">" + +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/CopyOnWriteArrayListNewImpl.scala b/src/col/vct/col/ast/lang/runtime/CopyOnWriteArrayListNewImpl.scala new file mode 100644 index 0000000000..81652ad7d6 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/CopyOnWriteArrayListNewImpl.scala @@ -0,0 +1,12 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.CopyOnWriteArrayListNewOps + +trait CopyOnWriteArrayListNewImpl[G] extends CopyOnWriteArrayListNewOps[G] { + this: CopyOnWriteArrayListNew[G] => + + override def layout(implicit ctx: Ctx): Doc = Text("new") <+> t.show <> "()" + +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/CopyOnWriteArrayListRemoveImpl.scala b/src/col/vct/col/ast/lang/runtime/CopyOnWriteArrayListRemoveImpl.scala new file mode 100644 index 0000000000..4d7e856e44 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/CopyOnWriteArrayListRemoveImpl.scala @@ -0,0 +1,15 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.CopyOnWriteArrayListRemoveOps + +trait CopyOnWriteArrayListRemoveImpl[G] extends CopyOnWriteArrayListRemoveOps[G] { + this: CopyOnWriteArrayListRemove[G] => + + override def t: Type[G] = TBool[G]() + + override def layout(implicit ctx: Ctx): Doc = + obj.show <> Text(".remove(") <> arg.show <> Text(")") + +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/CreateObjectArrayImpl.scala b/src/col/vct/col/ast/lang/runtime/CreateObjectArrayImpl.scala new file mode 100644 index 0000000000..c2041f359f --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/CreateObjectArrayImpl.scala @@ -0,0 +1,15 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.CreateObjectArrayOps + +trait CreateObjectArrayImpl[G] extends CreateObjectArrayOps[G] { + this: CreateObjectArray[G] => + + override val t: Type[G] = TArray[G](TAnyClass[G]()) + override def precedence: Int = Precedence.ATOMIC + + + override def layout(implicit ctx: Ctx): Doc = Text("new Object[]{") <> Doc.args(args) <> "}" +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/EqualsImpl.scala b/src/col/vct/col/ast/lang/runtime/EqualsImpl.scala new file mode 100644 index 0000000000..2c33518e21 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/EqualsImpl.scala @@ -0,0 +1,14 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.EqualsOps + +trait EqualsImpl[G] extends EqualsOps[G] { + this: Equals[G] => + + override def t: Type[G] = TBool[G]() + + override def layout(implicit ctx: Ctx): Doc = + obj.show <> Text(".equals(") <> target.show <> Text(")") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/GetArrayPermissionImpl.scala b/src/col/vct/col/ast/lang/runtime/GetArrayPermissionImpl.scala new file mode 100644 index 0000000000..7609ed4319 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/GetArrayPermissionImpl.scala @@ -0,0 +1,17 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.GetArrayPermissionOps + +trait GetArrayPermissionImpl[G] extends GetArrayPermissionOps[G] { + this: GetArrayPermission[G] => + + override def precedence: Int = Precedence.ATOMIC + + override def t: Type[G] = TFraction[G]() + private def defaultFraction: RuntimeFractionZero[G] = RuntimeFractionZero[G]() + + override def layout(implicit ctx: Ctx): Doc = + Nest(objectLocation.show <> Text(s".__runtime__$id.get(") <> location <> Text(").getOrDefault(") <> threadId.show <> Text(",") <+> defaultFraction.show <> Text(")")) +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/GetClassCallImpl.scala b/src/col/vct/col/ast/lang/runtime/GetClassCallImpl.scala new file mode 100644 index 0000000000..e63f3cffea --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/GetClassCallImpl.scala @@ -0,0 +1,20 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.GetClassCallOps + +trait GetClassCallImpl[G] extends GetClassCallOps[G] { + this: GetClassCall[G] => + override def precedence: Int = Precedence.ATOMIC + + override val t: Type[G] = TAnyClass[G]() + + override def layout(implicit ctx: Ctx): Doc = { + if(obj.nonEmpty) { + obj.get.show <> ".getClass()" + } else{ + Text("getClass()") + } + } +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/GetPermissionImpl.scala b/src/col/vct/col/ast/lang/runtime/GetPermissionImpl.scala new file mode 100644 index 0000000000..562ddc1a5b --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/GetPermissionImpl.scala @@ -0,0 +1,17 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.GetPermissionOps + +trait GetPermissionImpl[G] extends GetPermissionOps[G] { + this: GetPermission[G] => + + override def t: Type[G] = TFraction[G]() + + private def defaultFraction: RuntimeFractionZero[G] = RuntimeFractionZero[G]() + + + override def layout(implicit ctx: Ctx): Doc = + Nest(objectLocation.show <> Text(s".__runtime__.get($id).getOrDefault(") <> threadId.show <> Text(",") <+> defaultFraction.show <> Text(")")) +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/JavaLocalRuntimeImpl.scala b/src/col/vct/col/ast/lang/runtime/JavaLocalRuntimeImpl.scala new file mode 100644 index 0000000000..7f03253c36 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/JavaLocalRuntimeImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print.{Ctx, Doc, Text} +import vct.col.ast.ops.JavaLocalRuntimeOps + +trait JavaLocalRuntimeImpl[G] extends JavaLocalRuntimeOps[G] { this: JavaLocalRuntime[G] => + override lazy val t: Type[G] = ref.decl.t + + override def layout(implicit ctx: Ctx): Doc = Text(ref.decl.name) +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/ObjectGetLengthImpl.scala b/src/col/vct/col/ast/lang/runtime/ObjectGetLengthImpl.scala new file mode 100644 index 0000000000..79bc5468b5 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/ObjectGetLengthImpl.scala @@ -0,0 +1,13 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.ObjectGetLengthOps + +trait ObjectGetLengthImpl[G] extends ObjectGetLengthOps[G] { + this: ObjectGetLength[G] => + + override val t: Type[G] = TInt[G]() + + override def layout(implicit ctx: Ctx): Doc = Text("Array.getLength(") <> input.show <> ")" +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/ObjectIsArrayImpl.scala b/src/col/vct/col/ast/lang/runtime/ObjectIsArrayImpl.scala new file mode 100644 index 0000000000..e89dfd1b62 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/ObjectIsArrayImpl.scala @@ -0,0 +1,13 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.ObjectIsArrayOps + +trait ObjectIsArrayImpl[G] extends ObjectIsArrayOps[G] { + this: ObjectIsArray[G] => + + override val t: Type[G] = TBool[G]() + + override def layout(implicit ctx: Ctx): Doc = input.show <> ".getClass().isArray()" +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/PredicateStoreGetImpl.scala b/src/col/vct/col/ast/lang/runtime/PredicateStoreGetImpl.scala new file mode 100644 index 0000000000..c0dc12edd7 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/PredicateStoreGetImpl.scala @@ -0,0 +1,15 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.PredicateStoreGetOps + +trait PredicateStoreGetImpl[G] extends PredicateStoreGetOps[G] { + this: PredicateStoreGet[G] => + + override def t: Type[G] = TArray[G](TClass[G](cls, Nil)) + + override def layout(implicit ctx: Ctx): Doc = + Text("predicateStore.get(") <> threadId.show <> Text(")") + +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/PredicateStoreImpl.scala b/src/col/vct/col/ast/lang/runtime/PredicateStoreImpl.scala new file mode 100644 index 0000000000..fb2fe9d2af --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/PredicateStoreImpl.scala @@ -0,0 +1,16 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print.{Ctx, Doc, Group, Text} +import vct.col.ast.ops.PredicateStoreOps + +trait PredicateStoreImpl[G] extends PredicateStoreOps[G] { + this: PredicateStore[G] => + + + + + override def layout(implicit ctx: Ctx): Doc = + Group(Text("private static ConcurrentHashMap storeType <> Text(">> predicateStore = new ConcurrentHashMap();")) + +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/PutArrayPermissionImpl.scala b/src/col/vct/col/ast/lang/runtime/PutArrayPermissionImpl.scala new file mode 100644 index 0000000000..fd2f7008fd --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/PutArrayPermissionImpl.scala @@ -0,0 +1,16 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.PutArrayPermissionOps + +trait PutArrayPermissionImpl[G] extends PutArrayPermissionOps[G] { + this: PutArrayPermission[G] => + + override def precedence: Int = Precedence.ATOMIC + + override def t: Type[G] = TFraction[G]() + + override def layout(implicit ctx: Ctx): Doc = + Nest(objectLocation.show <> Text(s".__runtime__$id.get(") <> location <> Text(").put(") <> threadId.show <> Text(", ") <> permission <> Text(")")) +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/PutPermissionImpl.scala b/src/col/vct/col/ast/lang/runtime/PutPermissionImpl.scala new file mode 100644 index 0000000000..cd7a23c908 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/PutPermissionImpl.scala @@ -0,0 +1,15 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.PutPermissionOps + +trait PutPermissionImpl[G] extends PutPermissionOps[G] { + this: PutPermission[G] => + + override def t: Type[G] = TFraction[G]() + + override def layout(implicit ctx: Ctx): Doc = + Nest(objectLocation.show <> Text(s".__runtime__.get($id)") <> Text(".put(") <> threadId.show <> Text(",") <> Nest(permission.show) <> Text(")")) + +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeAssertExpectedImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeAssertExpectedImpl.scala new file mode 100644 index 0000000000..88b1f34e0a --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeAssertExpectedImpl.scala @@ -0,0 +1,13 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeAssertExpectedOps + +trait RuntimeAssertExpectedImpl[G] extends RuntimeAssertExpectedOps[G] { + this: RuntimeAssertExpected[G] => + + + override def layout(implicit ctx: Ctx): Doc = + Text("assert(") <> res.show <> ") : \"" <> message <+> " expected: \" +" <+> expected.show <+> "+ \" but got: \" +" <+> received.show <> ";" +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeAssertImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeAssertImpl.scala new file mode 100644 index 0000000000..e77ff446d7 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeAssertImpl.scala @@ -0,0 +1,12 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeAssertOps + +trait RuntimeAssertImpl[G] extends RuntimeAssertOps[G] { + this: RuntimeAssert[G] => + + + override def layout(implicit ctx: Ctx): Doc = Group(Group(Text("assert (") <> res.show <> ")" ) <> Group(Text(": \"") <> message <> "\";")) +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapContainsKeyImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapContainsKeyImpl.scala new file mode 100644 index 0000000000..dfc7c459eb --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapContainsKeyImpl.scala @@ -0,0 +1,13 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeConcurrentHashMapContainsKeyOps + +trait RuntimeConcurrentHashMapContainsKeyImpl[G] extends RuntimeConcurrentHashMapContainsKeyOps[G] { + this: RuntimeConcurrentHashMapContainsKey[G] => + + override val t: Type[G] = TBool[G]() + + override def layout(implicit ctx: Ctx): Doc = hm.show <> ".containsKey(" <> key.show <> ")" +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapGetImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapGetImpl.scala new file mode 100644 index 0000000000..7b26efd57e --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapGetImpl.scala @@ -0,0 +1,13 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeConcurrentHashMapGetOps + +trait RuntimeConcurrentHashMapGetImpl[G] extends RuntimeConcurrentHashMapGetOps[G] { + this: RuntimeConcurrentHashMapGet[G] => + + override lazy val t: Type[G] = hm.t.asInstanceOf[RuntimeConcurrentHashMap[G]].valueType + + override def layout(implicit ctx: Ctx): Doc = hm.show <> ".get(" <> key.show <> ")" +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapGetOrDefaultImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapGetOrDefaultImpl.scala new file mode 100644 index 0000000000..bde04de80b --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapGetOrDefaultImpl.scala @@ -0,0 +1,13 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeConcurrentHashMapGetOrDefaultOps + +trait RuntimeConcurrentHashMapGetOrDefaultImpl[G] extends RuntimeConcurrentHashMapGetOrDefaultOps[G] { + this: RuntimeConcurrentHashMapGetOrDefault[G] => + + override lazy val t: Type[G] = hm.t.asInstanceOf[RuntimeConcurrentHashMap[G]].valueType + + override def layout(implicit ctx: Ctx): Doc = hm.show <> ".getOrDefault(" <> key.show <> "," <+> default.show <> ")" +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapImpl.scala new file mode 100644 index 0000000000..324f65caa5 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeConcurrentHashMapOps + +trait RuntimeConcurrentHashMapImpl[G] extends RuntimeConcurrentHashMapOps[G] { + this: RuntimeConcurrentHashMap[G] => + + override def layout(implicit ctx: Ctx): Doc = Text("Map<") <> keyType.show <> "," <+> valueType.show <> ">" +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapKeySetImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapKeySetImpl.scala new file mode 100644 index 0000000000..7874134cba --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapKeySetImpl.scala @@ -0,0 +1,13 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeConcurrentHashMapKeySetOps + +trait RuntimeConcurrentHashMapKeySetImpl[G] extends RuntimeConcurrentHashMapKeySetOps[G] { + this: RuntimeConcurrentHashMapKeySet[G] => + + override val t: Type[G] = TBool[G]() + + override def layout(implicit ctx: Ctx): Doc = hm.show <> ".keySet()" +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapPutImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapPutImpl.scala new file mode 100644 index 0000000000..ca2cc516a2 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeConcurrentHashMapPutImpl.scala @@ -0,0 +1,13 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeConcurrentHashMapPutOps + +trait RuntimeConcurrentHashMapPutImpl[G] extends RuntimeConcurrentHashMapPutOps[G] { + this: RuntimeConcurrentHashMapPut[G] => + + override val t: Type[G] = TVoid[G]() + + override def layout(implicit ctx: Ctx): Doc = hm.show <> ".put(" <> key.show <> "," <+> value.show <> ")" +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeFractionAddImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeFractionAddImpl.scala new file mode 100644 index 0000000000..eb16150479 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeFractionAddImpl.scala @@ -0,0 +1,15 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeFractionAddOps + +trait RuntimeFractionAddImpl[G] extends RuntimeFractionAddOps[G] { + this: RuntimeFractionAdd[G] => + + override def t: Type[G] = TRuntimeFraction[G]() + override def precedence: Int = Precedence.ATOMIC + + override def layout(implicit ctx: Ctx): Doc = + left.show <> Text(".add(") <> right <> Text(")") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeFractionCompareImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeFractionCompareImpl.scala new file mode 100644 index 0000000000..c09740d13e --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeFractionCompareImpl.scala @@ -0,0 +1,15 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeFractionCompareOps + +trait RuntimeFractionCompareImpl[G] extends RuntimeFractionCompareOps[G] { + this: RuntimeFractionCompare[G] => + + override def t: Type[G] = TInt[G]() + override def precedence: Int = Precedence.ATOMIC + + override def layout(implicit ctx: Ctx): Doc = + left.show <> Text(".compareTo(") <> right <> Text(")") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeFractionDiffImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeFractionDiffImpl.scala new file mode 100644 index 0000000000..15b9ed58c9 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeFractionDiffImpl.scala @@ -0,0 +1,15 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeFractionDiffOps + +trait RuntimeFractionDiffImpl[G] extends RuntimeFractionDiffOps[G] { + this: RuntimeFractionDiff[G] => + + override def t: Type[G] = TRuntimeFraction[G]() + override def precedence: Int = Precedence.ATOMIC + + override def layout(implicit ctx: Ctx): Doc = + Text("new Fraction(") <> left <> Text(",") <> right <> Text(")") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeFractionMultiplyImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeFractionMultiplyImpl.scala new file mode 100644 index 0000000000..7312832814 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeFractionMultiplyImpl.scala @@ -0,0 +1,15 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeFractionMultiplyOps + +trait RuntimeFractionMultiplyImpl[G] extends RuntimeFractionMultiplyOps[G] { + this: RuntimeFractionMultiply[G] => + + override def t: Type[G] = TRuntimeFraction[G]() + override def precedence: Int = Precedence.ATOMIC + + override def layout(implicit ctx: Ctx): Doc = + left.show <> Text(".multiply(") <> right <> Text(")") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeFractionOneImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeFractionOneImpl.scala new file mode 100644 index 0000000000..aaa3c551fc --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeFractionOneImpl.scala @@ -0,0 +1,15 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeFractionOneOps + +trait RuntimeFractionOneImpl[G] extends RuntimeFractionOneOps[G] { + this: RuntimeFractionOne[G] => + + override def t: Type[G] = TRuntimeFraction[G]() + override def precedence: Int = Precedence.ATOMIC + + override def layout(implicit ctx: Ctx): Doc = + Text("Fraction.ONE") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeFractionSubstractImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeFractionSubstractImpl.scala new file mode 100644 index 0000000000..845246cd2c --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeFractionSubstractImpl.scala @@ -0,0 +1,15 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeFractionSubstractOps + +trait RuntimeFractionSubstractImpl[G] extends RuntimeFractionSubstractOps[G] { + this: RuntimeFractionSubstract[G] => + + override def t: Type[G] = TRuntimeFraction[G]() + override def precedence: Int = Precedence.ATOMIC + + override def layout(implicit ctx: Ctx): Doc = + left.show <> Text(".subtract(") <> right <> Text(")") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeFractionZeroImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeFractionZeroImpl.scala new file mode 100644 index 0000000000..171831ac65 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeFractionZeroImpl.scala @@ -0,0 +1,15 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeFractionZeroOps + +trait RuntimeFractionZeroImpl[G] extends RuntimeFractionZeroOps[G] { + this: RuntimeFractionZero[G] => + + override def t: Type[G] = TRuntimeFraction[G]() + override def precedence: Int = Precedence.ATOMIC + + override def layout(implicit ctx: Ctx): Doc = + Text("Fraction.ZERO") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeNewConcurrentHashMapImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeNewConcurrentHashMapImpl.scala new file mode 100644 index 0000000000..7a87e98c08 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeNewConcurrentHashMapImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimeNewConcurrentHashMapOps + +trait RuntimeNewConcurrentHashMapImpl[G] extends RuntimeNewConcurrentHashMapOps[G] { + this: RuntimeNewConcurrentHashMap[G] => + + override def layout(implicit ctx: Ctx): Doc = Text("Collections.synchronizedMap(new WeakHashMap<>())") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimeNewPredicateImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimeNewPredicateImpl.scala new file mode 100644 index 0000000000..82bee5eabc --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimeNewPredicateImpl.scala @@ -0,0 +1,15 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print.{Ctx, Doc, Text} +import vct.col.ast.ops.RuntimeNewPredicateOps + +trait RuntimeNewPredicateImpl[G] extends RuntimeNewPredicateOps[G] { + this: RuntimeNewPredicate[G] => + + override def t: Type[G] = TClass(cls, Nil) + + override def layout(implicit ctx: Ctx): Doc = + Text("new") <+> ctx.name(cls) <> "(" <> Doc.args(this.args) <> ")" + +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimePermissionImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimePermissionImpl.scala new file mode 100644 index 0000000000..ba4e2353a2 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimePermissionImpl.scala @@ -0,0 +1,23 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print.{Empty, _} +import vct.col.ast.ops.RuntimePermissionOps + +trait RuntimePermissionImpl[G] extends RuntimePermissionOps[G] { + this: RuntimePermission[G] => + + override def t: Type[G] = TFraction[G]() + + def layoutPermission(implicit ctx: Ctx): Doc = { + permission match { + case _: WritePerm[G] => Text("1") + case _: ReadPerm[G] => Text("0") + case d : RatDiv[G] => Text("Fraction.getFraction(") <> d.left.show <> "," <+> d.right.show <> ")" + case _ => Empty + } + } + + override def layout(implicit ctx: Ctx): Doc = + Group(layoutPermission) +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/RuntimePostJoinImpl.scala b/src/col/vct/col/ast/lang/runtime/RuntimePostJoinImpl.scala new file mode 100644 index 0000000000..12ccc04c10 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/RuntimePostJoinImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.RuntimePostJoinOps + +trait RuntimePostJoinImpl[G] extends RuntimePostJoinOps[G] { + this: RuntimePostJoin[G] => + + override def layout(implicit ctx: Ctx): Doc = Doc.spec(obj.show <> ".postJoin(" <> arg.show <> ")") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/StaticClassRefImpl.scala b/src/col/vct/col/ast/lang/runtime/StaticClassRefImpl.scala new file mode 100644 index 0000000000..2e88b5103f --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/StaticClassRefImpl.scala @@ -0,0 +1,14 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.StaticClassRefOps + +trait StaticClassRefImpl[G] extends StaticClassRefOps[G] { + this: StaticClassRef[G] => + + + override def t: Type[G] = TClass(cls, Nil) + override def precedence: Int = Precedence.ATOMIC + override def layout(implicit ctx: Ctx): Doc = t.show +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/StaticImpl.scala b/src/col/vct/col/ast/lang/runtime/StaticImpl.scala new file mode 100644 index 0000000000..2705318dc2 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/StaticImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.StaticOps + +trait StaticImpl[G] extends StaticOps[G] { + this: Static[G] => + + override def layout(implicit ctx: Ctx): Doc = Text("static") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/TIntObjectImpl.scala b/src/col/vct/col/ast/lang/runtime/TIntObjectImpl.scala new file mode 100644 index 0000000000..91d10f1074 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/TIntObjectImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.TIntObjectOps + +trait TIntObjectImpl[G] extends TIntObjectOps[G] { + this: TIntObject[G] => + + override def layout(implicit ctx: Ctx): Doc = Text("Integer") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/TLongImpl.scala b/src/col/vct/col/ast/lang/runtime/TLongImpl.scala new file mode 100644 index 0000000000..031b2319cc --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/TLongImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.TLongOps + +trait TLongImpl[G] extends TLongOps[G] { + this: TLong[G] => + + override def layout(implicit ctx: Ctx): Doc = Text("long") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/TLongObjectImpl.scala b/src/col/vct/col/ast/lang/runtime/TLongObjectImpl.scala new file mode 100644 index 0000000000..262d72bda3 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/TLongObjectImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.TLongObjectOps + +trait TLongObjectImpl[G] extends TLongObjectOps[G] { + this: TLongObject[G] => + + override def layout(implicit ctx: Ctx): Doc = Text("Long") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/TRuntimeFractionImpl.scala b/src/col/vct/col/ast/lang/runtime/TRuntimeFractionImpl.scala new file mode 100644 index 0000000000..1d6ee99f21 --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/TRuntimeFractionImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.TRuntimeFractionOps + +trait TRuntimeFractionImpl[G] extends TRuntimeFractionOps[G] { + this: TRuntimeFraction[G] => + + override def layout(implicit ctx: Ctx): Doc = Text("Fraction") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/lang/runtime/ThreadIdImpl.scala b/src/col/vct/col/ast/lang/runtime/ThreadIdImpl.scala new file mode 100644 index 0000000000..5f4f656cce --- /dev/null +++ b/src/col/vct/col/ast/lang/runtime/ThreadIdImpl.scala @@ -0,0 +1,22 @@ +package vct.col.ast.lang.runtime + +import vct.col.ast._ +import vct.col.print._ +import vct.col.ast.ops.ThreadIdOps + +trait ThreadIdImpl[G] extends ThreadIdOps[G] { + this: ThreadId[G] => + + + override def t: Type[G] = TLong[G]() + + def objectLayout(implicit ctx: Ctx) : Doc = { + obj match { + case Some(value) => value.show <> Text(".getId()") + case None => Text("Thread.currentThread().getId()") + } + } + + + override def layout(implicit ctx: Ctx): Doc = objectLayout +} \ No newline at end of file diff --git a/src/col/vct/col/ast/statement/composite/EnhancedLoopImpl.scala b/src/col/vct/col/ast/statement/composite/EnhancedLoopImpl.scala new file mode 100644 index 0000000000..4273dd07b7 --- /dev/null +++ b/src/col/vct/col/ast/statement/composite/EnhancedLoopImpl.scala @@ -0,0 +1,21 @@ +package vct.col.ast.statement.composite + +import vct.col.ast._ +import vct.col.check.CheckContext +import vct.col.origin.Origin +import vct.col.print +import vct.col.print._ +import vct.col.ref.Ref +import vct.col.util.AstBuildHelpers._ +import vct.result.VerificationError.UserError +import vct.col.ast.ops.EnhancedLoopOps + +trait EnhancedLoopImpl[G] extends EnhancedLoopOps[G] { this: EnhancedLoop[G] => + + override def enterCheckContextScopes(context: CheckContext[G]): Seq[CheckContext.ScopeFrame[G]] = + context.withScope(Seq(arg), toScan = Seq(body)) + + override def layout(implicit ctx: Ctx): Doc = { + Group(Text("for") <+> "(" <> Nest(NonWsLine <> arg.show <+> ":" <+> iter.show) Text(")")) <+> body.layoutAsBlock + } +} \ No newline at end of file diff --git a/src/col/vct/col/ast/statement/terminal/AssertImpl.scala b/src/col/vct/col/ast/statement/terminal/AssertImpl.scala index c34211c664..ac24339b1e 100644 --- a/src/col/vct/col/ast/statement/terminal/AssertImpl.scala +++ b/src/col/vct/col/ast/statement/terminal/AssertImpl.scala @@ -11,8 +11,13 @@ trait AssertImpl[G] extends AssertOps[G] { this: Assert[G] => def layoutSilver(implicit ctx: Ctx): Doc = Text("assert") <+> res + def layoutJava(implicit ctx: Ctx): Doc = + Text("assert(") <> res <> ");" + + override def layout(implicit ctx: Ctx): Doc = ctx.syntax match { case Ctx.Silver => layoutSilver + case Ctx.Java => layoutJava case _ => Doc.inlineSpec(Show.lazily(layoutSpec(_))) } diff --git a/src/col/vct/col/ast/unsorted/CodeStringClassImpl.scala b/src/col/vct/col/ast/unsorted/CodeStringClassImpl.scala new file mode 100644 index 0000000000..7366d00896 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/CodeStringClassImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.unsorted + +import vct.col.ast.CodeStringClass +import vct.col.ast.ops.CodeStringClassOps +import vct.col.print._ + +trait CodeStringClassImpl[G] extends CodeStringClassOps[G] { this: CodeStringClass[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/unsorted/CodeStringGlobalImpl.scala b/src/col/vct/col/ast/unsorted/CodeStringGlobalImpl.scala new file mode 100644 index 0000000000..ef5eb05c49 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/CodeStringGlobalImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.unsorted + +import vct.col.ast.CodeStringGlobal +import vct.col.ast.ops.CodeStringGlobalOps +import vct.col.print._ + +trait CodeStringGlobalImpl[G] extends CodeStringGlobalOps[G] { this: CodeStringGlobal[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/unsorted/CodeStringStatementImpl.scala b/src/col/vct/col/ast/unsorted/CodeStringStatementImpl.scala new file mode 100644 index 0000000000..e791c47349 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/CodeStringStatementImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.unsorted + +import vct.col.ast.CodeStringStatement +import vct.col.ast.ops.CodeStringStatementOps +import vct.col.print._ + +trait CodeStringStatementImpl[G] extends CodeStringStatementOps[G] { this: CodeStringStatement[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/err/MistypedRef.scala b/src/col/vct/col/err/MistypedRef.scala index 337167ce8f..13dd8cbb9a 100644 --- a/src/col/vct/col/err/MistypedRef.scala +++ b/src/col/vct/col/err/MistypedRef.scala @@ -7,5 +7,5 @@ import scala.reflect.ClassTag case class MistypedRef(received: Declaration[_], expected: ClassTag[_]) extends ASTStateError { override def text: String = "A reference in the AST is referencing a declaration of the wrong kind.\n" + - s"A ${expected.runtimeClass.getSimpleName} was expected here, but we got a ${received.getClass.getSimpleName}" + s"A ${expected.runtimeClass.getSimpleName} was expected here, but we got a ${Option(received).map(_.getClass.getSimpleName).getOrElse("")}" } diff --git a/src/col/vct/col/origin/Origin.scala b/src/col/vct/col/origin/Origin.scala index 092ce536f4..bf2440108a 100644 --- a/src/col/vct/col/origin/Origin.scala +++ b/src/col/vct/col/origin/Origin.scala @@ -187,6 +187,10 @@ case class PositionRange(startLineIdx: Int, endLineIdx: Int, startEndColIdx: Opt } } +case class LedgerClassRuntime() extends OriginContent +case class DataObjectClassRuntime() extends OriginContent +object JavaLibrary extends OriginContent + /** * A sequence of OriginContents. This sequence can be mutated (add, remove, replace) for convenience. * @param originContents The known origin contents at the time of Origin creation. Can be empty for a new Origin. @@ -249,11 +253,23 @@ final case class Origin(originContents: Seq[OriginContent]) extends Blame[Verifi def debugName(name: String = "unknown"): String = find[SourceName].map(_.name).getOrElse(getPreferredNameOrElse(Seq(name)).camel) -// def addStartEndLines(startIdx: Int, endIdx: Int): Origin = -// withContent(StartEndLines(startIdx, endIdx)) -// -// def addOriginCols(cols: Option[(Int, Int)]): Origin = -// withContent(OriginCols(cols)) + def addLedgerClass(): Origin = { + Origin(originContents :+ LedgerClassRuntime()) + } + + def addDataObjectClass(): Origin = { + Origin(originContents :+ DataObjectClassRuntime()) + } + + def getReadable: Option[ReadableOrigin] = { + originContents.flatMap { + case ReadableOrigin(any1) => Seq(ReadableOrigin(any1)) + case _ => Nil + } match { + case Seq(ReadableOrigin(any1)) => Some(ReadableOrigin(any1)) + case _ => None + } + } def getPreferredName: Option[Name] = originContents.headOption.flatMap(_.name(tail).orElse(tail.getPreferredName)) @@ -280,6 +296,36 @@ final case class Origin(originContents: Seq[OriginContent]) extends Blame[Verifi def shortPositionText: String = shortPosition.getOrElse("[unknown position]") + def getFilename: Option[OriginFilename] = { + originContents.flatMap { + case OriginFilename(any) => Seq(OriginFilename(any)) + case _ => Nil + } match { + case Seq(OriginFilename(any)) => Some(OriginFilename(any)) + case _ => None + } + } + + def getLedgerClassRuntime: Option[LedgerClassRuntime] = { + originContents.flatMap { + case LedgerClassRuntime() => Seq(LedgerClassRuntime()) + case _ => Nil + } match { + case Seq(i@LedgerClassRuntime()) => Some(i) + case _ => None + } + } + + def getDataObjectClassRuntime: Option[DataObjectClassRuntime] = { + originContents.flatMap { + case DataObjectClassRuntime() => Seq(DataObjectClassRuntime()) + case _ => Nil + } match { + case Seq(i@DataObjectClassRuntime()) => Some(i) + case _ => None + } + } + override def blame(error: VerificationFailure): Unit = { Logger("vct").error(error.toString) } diff --git a/src/col/vct/col/print/Namer.scala b/src/col/vct/col/print/Namer.scala index 2071f6aa1a..30a9a7aade 100644 --- a/src/col/vct/col/print/Namer.scala +++ b/src/col/vct/col/print/Namer.scala @@ -44,6 +44,7 @@ case class Namer[G](syntax: Ctx.Syntax) { case _: Procedure[G] => () case _: InstanceFunction[G] => () case _: InstanceMethod[G] => () + case _: CodeStringQuantifierMethod[G] => () case _: Constructor[G] => () case _: JavaConstructor[G] => () case _: JavaMethod[G] => () @@ -63,6 +64,7 @@ case class Namer[G](syntax: Ctx.Syntax) { case _: Procedure[G] => () case _: InstanceFunction[G] => () case _: InstanceMethod[G] => () + case _: CodeStringQuantifierMethod[G] => () case _: Constructor[G] => () case _: JavaMethod[G] => () case _: JavaAnnotationMethod[G] => () @@ -107,6 +109,7 @@ case class Namer[G](syntax: Ctx.Syntax) { } while(keys.exists(key => names.contains((key, baseName, index)))) { + val similar_keys = keys.collect(key => names.get((key, baseName, index))) index += 1 } diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index f72204c330..0da8a92e4e 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -70,6 +70,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite */ def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])(implicit o: Origin): Expr[Post] = { coercion match { + case CoerceTArrayAnyClass() => e case CoerceIdentity(_) => e case CoercionSequence(cs) => cs.foldLeft(e) { case (e, c) => applyCoercion(e, c) } case CoerceNothingSomething(_) => e @@ -694,6 +695,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite And(bool(left), bool(right)) case any @ Any() => Any()(any.blame) + case ae@ArraysEquals(o,t) => e + case ae@ArraysHashCode(o) => e case a @ ArraySubscript(arr, index) => ArraySubscript(array(arr)._1, int(index))(a.blame) case BagAdd(xs, ys) => @@ -766,6 +769,10 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite val (coercedXs, TSeq(element)) = seq(xs) val sharedType = Types.leastCommonSuperType(x.t, element) Cons(coerce(x, sharedType), coerce(xs, TSeq(sharedType))) + case CopyOnWriteArrayListAdd(o, a) => e + case CopyOnWriteArrayListRemove(o, a) => e + case CopyOnWriteArrayListNew(t) => e + case CopyOnWriteArrayListContains(o, a) => e case cfa@CPPClassMethodOrFieldAccess(classInstance, methodOrFieldName) => CPPClassMethodOrFieldAccess(classInstance, methodOrFieldName)(cfa.blame) case defn@CPPLambdaDefinition(contract, declarator, body) => CPPLambdaDefinition(contract, declarator, body)(defn.blame) @@ -804,6 +811,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite Drop(seq(xs)._1, int(count)) case Empty(obj) => Empty(sized(obj)._1) + case Equals(obj, target) => Equals(obj, target) case EmptyProcess() => EmptyProcess() case use @ EnumUse(enum, const) => use case Eq(left, right) => @@ -831,8 +839,11 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite ForPermWithValue(binding, bool(body)) case inv @ FunctionInvocation(ref, args, typeArgs, givenMap, yields) => FunctionInvocation(ref, coerceArgs(args, ref.decl, inv.typeEnv, canCDemote=true), typeArgs, coerceGiven(givenMap, canCDemote=true), coerceYields(yields, inv))(inv.blame) + case g@GetClassCall(o) => e case get @ GetLeft(e) => GetLeft(either(e)._1)(get.blame) + case GetPermission(o, i, t) => e + case GetArrayPermission(o, i,l, t) => e case get @ GetRight(e) => GetRight(either(e)._1)(get.blame) case GlobalThreadId() => @@ -881,6 +892,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite case JavaLiteralArray(exprs) => JavaLiteralArray(exprs) case JavaLocal(name) => e + case JavaLocalRuntime(r) => e case JavaNewClass(args, typeArgs, name, givenMap, yields) => e case JavaNewDefaultArray(baseType, specifiedDims, moreDims) => e case JavaNewLiteralArray(baseType, dims, initializer) => e @@ -1039,6 +1051,9 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite Not(bool(arg)) case Null() => Null() + case ObjectIsArray(i) => e + case ObjectGetLength(i) => e + case CreateObjectArray(a) => e case old @ Old(expr, at) => Old(expr, at)(old.blame) case OptEmpty(opt) => @@ -1102,6 +1117,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite LlvmFunctionInvocation(ref, args, givenMap, yields)(inv.blame) case inv @ LlvmAmbiguousFunctionInvocation(name, args, givenMap, yields) => LlvmAmbiguousFunctionInvocation(name, args, givenMap, yields)(inv.blame) + case PredicateStoreGet(c, t) => e case ProcessApply(process, args) => ProcessApply(process, coerceArgs(args, process.decl)) case ProcessChoice(left, right) => @@ -1116,6 +1132,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite Product(bindings, bool(condition), int(main)) case ProverFunctionInvocation(ref, args) => ProverFunctionInvocation(ref, coerceArgs(args, ref.decl)) + case PutPermission(o, i, p,t) => e + case PutArrayPermission(o, i, l, p,t) => e case PVLDeref(obj, field) => e case PVLInvocation(obj, method, args, typeArgs, givenArgs, yields) => e case PVLLocal(name) => e @@ -1142,6 +1160,21 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite ResourceValue(res(r)) case Result(ref) => Result(ref) + case RuntimeNewPredicate(c, a) => e + case RuntimePermission(p) => e + case RuntimeFractionDiff(l, r) => e + case RuntimeFractionZero() => e + case RuntimeFractionOne() => e + case RuntimeConcurrentHashMapGet(h, k) => e + case RuntimeConcurrentHashMapContainsKey(h, k) => e + case RuntimeConcurrentHashMapGetOrDefault(h, k, v) => e + case RuntimeConcurrentHashMapKeySet(h) => e + case RuntimeConcurrentHashMapPut(h, k, v) => e + case RuntimeNewConcurrentHashMap(t) => e + case RuntimeFractionAdd(l, r) => e + case RuntimeFractionSubstract(l, r) => e + case RuntimeFractionMultiply(l, r) => e + case RuntimeFractionCompare(l, r) => e case s @ Scale(scale, r) => Scale(rat(scale), res(r))(s.blame) case ScaleByParBlock(ref, r) => @@ -1326,6 +1359,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite Star(res(left), res(right)) case starall @ Starall(bindings, triggers, body) => Starall(bindings, triggers, res(body))(starall.blame) + case StaticClassRef(cls) => e case SubBag(left, right) => val (coercedLeft, leftBag) = bag(left) val (coercedRight, rightBag) = bag(right) @@ -1352,6 +1386,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite Sum(bindings, bool(condition), int(main)) case SuperType(left, right) => SuperType(left, right) + case StaticClassRef(r) => e case Tail(xs) => Tail(seq(xs)._1) case Take(xs, count) => @@ -1364,6 +1399,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite ThisSeqProg(ref) case ThisObject(ref) => ThisObject(ref) + case ThreadId(o) => e case TupGet(tup, index) => TupGet(tuple(tup)._1, index) case TypeOf(expr) => @@ -1460,6 +1496,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite case localIncoming: BipLocalIncomingData[Pre] => localIncoming case glue: JavaBipGlue[Pre] => glue case LlvmLocal(name) => e + case CodeStringQuantifierCall(_,_,_,_) => e } } @@ -1522,6 +1559,9 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite case Recv(ref) => Recv(ref) case r @ Refute(assn) => Refute(res(assn))(r.blame) case Return(result) => Return(result) // TODO coerce return, make AmbiguousReturn? + case r@RuntimeAssert(res, m) => RuntimeAssert(res, m)(r.blame) + case r@RuntimeAssertExpected(res, ex, received, m) => RuntimeAssertExpected(res, ex, received, m)(r.blame) + case r@RuntimePostJoin(obj, args) => RuntimePostJoin(obj, args)(r.blame) case Scope(locals, body) => Scope(locals, body) case send @ Send(decl, offset, resource) => Send(decl, offset, res(resource))(send.blame) case ass @ SilverFieldAssign(obj, field, value) => SilverFieldAssign(ref(obj), field, coerce(value, field.decl.t))(ass.blame) @@ -1563,6 +1603,11 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite case branch@PVLBranch(branches) => PVLBranch(branches.map { case (cond, effect) => (bool(cond), effect) })(branch.blame) case loop@UnresolvedSeqLoop(cond, contract, body) => UnresolvedSeqLoop(bool(cond), contract, body)(loop.blame) case loop@PVLLoop(init, cond, update, contract, body) => PVLLoop(init, bool(cond), update, contract, body)(loop.blame) + case c @ PVLCommunicate(s, r) => PVLCommunicate(s, r)(c.blame) + case CodeStringStatement(c) => CodeStringStatement(c) + case CodeStringQuantifier(q, l, u, body) => CodeStringQuantifier(q, l, u, body) + case CodeStringGetPredicate(a, c) => CodeStringGetPredicate(a, c) + case EnhancedLoop(a, i, b) => EnhancedLoop(a, i, b) } } @@ -1713,8 +1758,12 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite case glob: LlvmGlobal[Pre] => glob case endpoint: PVLEndpoint[Pre] => endpoint case seqProg: PVLSeqProg[Pre] => seqProg + case codestring: CodeString[Pre] => decl + case codeStringQuantifier: CodeStringQuantifierMethod[Pre] => decl + case predicateStore: PredicateStore[Pre] => decl + case _ => decl case seqRun: PVLSeqRun[Pre] => seqRun - } + } } def coerce(region: ParRegion[Pre]): ParRegion[Pre] = { @@ -1813,6 +1862,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite implicit val o: Origin = node.o node match { case value: Final[_] => value + case s: Static[_] => s } } diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index dc9bf84f0d..1a6bd1e924 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -189,6 +189,7 @@ case object CoercionUtils { case None => return None } + case (a@TArray(_), TAnyClass()) => CoerceTArrayAnyClass() // Something with TVar? diff --git a/src/col/vct/col/util/AstBuildHelpers.scala b/src/col/vct/col/util/AstBuildHelpers.scala index 887362651f..20e16912c3 100644 --- a/src/col/vct/col/util/AstBuildHelpers.scala +++ b/src/col/vct/col/util/AstBuildHelpers.scala @@ -60,13 +60,14 @@ object AstBuildHelpers { def %(right: Expr[G])(implicit origin: Origin, blame: Blame[DivByZero]): Mod[G] = Mod(left, right)(blame) def ===(right: Expr[G])(implicit origin: Origin): Eq[G] = Eq(left, right) + def ====(right: Expr[G])(implicit origin: Origin) : Equals[G] = Equals(left, right) def !==(right: Expr[G])(implicit origin: Origin): Neq[G] = Neq(left, right) def <(right: Expr[G])(implicit origin: Origin): Less[G] = Less(left, right) def >(right: Expr[G])(implicit origin: Origin): Greater[G] = Greater(left, right) def <=(right: Expr[G])(implicit origin: Origin): LessEq[G] = LessEq(left, right) def >=(right: Expr[G])(implicit origin: Origin): GreaterEq[G] = GreaterEq(left, right) - def unary_!(implicit origin: Origin): Not[G] = Not(left) + def unary_!(implicit origin: Origin = left.o): Not[G] = Not(left) def &&(right: Expr[G])(implicit origin: Origin): And[G] = And(left, right) def ||(right: Expr[G])(implicit origin: Origin): Or[G] = Or(left, right) def &*(right: Expr[G])(implicit origin: Origin): Star[G] = Star(left, right) @@ -76,6 +77,12 @@ object AstBuildHelpers { def ~>(field: SilverField[G])(implicit blame: Blame[InsufficientPermission], origin: Origin): SilverDeref[G] = SilverDeref[G](left, field.ref)(blame) def @@(index: Expr[G])(implicit blame: Blame[SeqBoundFailure], origin: Origin): SeqSubscript[G] = SeqSubscript(left, index)(blame) + + + def r_+(right: Expr[G])(implicit origin: Origin): RuntimeFractionAdd[G] = RuntimeFractionAdd(left, right) + def r_-(right: Expr[G])(implicit origin: Origin): RuntimeFractionSubstract[G] = RuntimeFractionSubstract(left, right) + def r_*(right: Expr[G])(implicit origin: Origin): RuntimeFractionMultiply[G] = RuntimeFractionMultiply(left, right) + def r_<=>(right: Expr[G])(implicit origin: Origin): RuntimeFractionCompare[G] = RuntimeFractionCompare(left, right) } implicit class VarBuildHelpers[G](left: Variable[G]) { @@ -155,6 +162,8 @@ object AstBuildHelpers { method.rewrite(returnType = returnType, operator = rewriter.dispatch(method.operator), args = args, body = body, contract = contract, inline = Some(inline), pure = Some(pure), blame = blame) case cons: Constructor[Pre] => cons.rewrite(args = args, outArgs = outArgs, typeArgs = typeArgs, body = body, contract = contract, inline = Some(inline), blame = blame) + case method: CodeStringQuantifierMethod[Pre] => + method.rewrite(quantifierId = method.quantifierId, args = args, body = body) } } @@ -243,6 +252,8 @@ object AstBuildHelpers { inv.rewrite(args = args, outArgs = outArgs, typeArgs = typeArgs, givenMap = givenMap, yields = yields) case inv: ConstructorInvocation[Pre] => inv.rewrite(args = args, outArgs = outArgs, typeArgs = typeArgs, givenMap = givenMap, yields = yields) + case codeCall:CodeStringQuantifierCall[Pre] => + codeCall.rewrite(args = args) } } @@ -506,4 +517,6 @@ object AstBuildHelpers { def foldAnd[G](exprs: Seq[Expr[G]])(implicit o: Origin): Expr[G] = exprs.reduceOption(And(_, _)).getOrElse(tt) + + def EMPTY[G](implicit origin: Origin):Block[G] = Block[G](Nil) } diff --git a/src/col/vct/col/util/Scopes.scala b/src/col/vct/col/util/Scopes.scala index fb06620546..7d46444e64 100644 --- a/src/col/vct/col/util/Scopes.scala +++ b/src/col/vct/col/util/Scopes.scala @@ -105,4 +105,9 @@ case class Scopes[Pre, Post, PreDecl <: Declaration[Pre], PostDecl <: Declaratio def dispatch[PreRefDecl <: PreDecl, PostRefDecl <: PostDecl](ref: Ref[Pre, PreRefDecl])(implicit tag: ClassTag[PostRefDecl]): Ref[Post, PostRefDecl] = freeze.succ(ref.decl) + + + def freezeBuffer: Seq[PostDecl] = { + collectionBuffer.top.toSeq + } } diff --git a/src/hre/hre/util/ScopedStack.scala b/src/hre/hre/util/ScopedStack.scala index 2a96e7b48a..706b62b211 100644 --- a/src/hre/hre/util/ScopedStack.scala +++ b/src/hre/hre/util/ScopedStack.scala @@ -1,7 +1,7 @@ package hre.util import scala.collection.mutable -import scala.collection.mutable.ArrayBuffer +import scala.collection.mutable.{ArrayBuffer, HashMap} case object ScopedStack { implicit class ScopedArrayBufferStack[T](stack: ScopedStack[ArrayBuffer[T]]) { @@ -11,6 +11,22 @@ case object ScopedStack { (buf.toSeq, res) } } + + implicit class ScopedSetStack[T](stack: ScopedStack[mutable.Set[T]]) { + def collect[R](f: => R): (mutable.Set[T], R) = { + val buf = mutable.Set[T]() + val res = stack.having(buf)(f) + (buf, res) + } + } + + implicit class ScopedHashMapStack[K, V](stack: ScopedStack[HashMap[K,V]]){ + def collect[R](f: => R): (HashMap[K,V], R) = { + val map = HashMap[K,V]() + val res = stack.having(map)(f) + (map, res) + } + } } case class ScopedStack[T]() { diff --git a/src/hre/vct/result/VerificationError.scala b/src/hre/vct/result/VerificationError.scala index 8811276f66..f817af27cc 100644 --- a/src/hre/vct/result/VerificationError.scala +++ b/src/hre/vct/result/VerificationError.scala @@ -47,7 +47,7 @@ object VerificationError { initCause(cause) override def text: String = - messageContext("VerCors crashed near this position. Cause follows:") + messageContext("VerCors crashed near this position. Cause follows:" + cause.getStackTrace.mkString("\n")) } trait Context { diff --git a/src/main/vct/importer/JavaLibraryLoader.scala b/src/main/vct/importer/JavaLibraryLoader.scala index 40b5e9a98e..e784e4fd71 100644 --- a/src/main/vct/importer/JavaLibraryLoader.scala +++ b/src/main/vct/importer/JavaLibraryLoader.scala @@ -2,7 +2,7 @@ package vct.importer import hre.io.RWFile import vct.col.ast.JavaNamespace -import vct.col.origin.{Origin, ReadableOrigin} +import vct.col.origin.{JavaLibrary, Origin, ReadableOrigin} import vct.col.resolve.ExternalJavaLoader import vct.parsers.debug.DebugOptions import vct.parsers.transform.BlameProvider @@ -16,7 +16,7 @@ import java.nio.file.Path case class JavaLibraryLoader(blameProvider: BlameProvider, debugOptions: DebugOptions) extends ExternalJavaLoader { override def load[G](base: Path, name: Seq[String]): Option[JavaNamespace[G]] = try { val f = RWFile(base.resolve((name.init :+ name.last + ".java").mkString(FILE_SEPARATOR))) - parser.ColJavaParser(debugOptions, blameProvider).parse[G](f).decls match { + parser.ColJavaParser(debugOptions, blameProvider).parse[G](f, Origin(Seq(JavaLibrary))).decls match { case Seq(ns: JavaNamespace[G]) => Some(ns) case _ => None } diff --git a/src/main/vct/main/Main.scala b/src/main/vct/main/Main.scala index 048258bfa2..8e3a6f390c 100644 --- a/src/main/vct/main/Main.scala +++ b/src/main/vct/main/Main.scala @@ -8,8 +8,8 @@ import hre.progress.{Layout, Progress} import org.slf4j.LoggerFactory import scopt.OParser import vct.col.ast.Node +import vct.main.modes.{RuntimeVerification, CFG, VeSUV, Verify, VeyMont} import vct.debug.CrashReport -import vct.main.modes.{CFG, VeSUV, Verify, VeyMont} import vct.main.stages.Transformation import vct.options.types.{Mode, Verbosity} import vct.options.Options @@ -123,6 +123,9 @@ case object Main extends LazyLogging { case Mode.CFG => logger.info("Starting control flow graph transformation") CFG.runOptions(options) + case Mode.RuntimeVerification => + logger.info("Starting runtime verification") + RuntimeVerification.runOptions(options) } } finally { Progress.finish() diff --git a/src/main/vct/main/modes/RuntimeVerification.scala b/src/main/vct/main/modes/RuntimeVerification.scala new file mode 100644 index 0000000000..0fdcc38aa9 --- /dev/null +++ b/src/main/vct/main/modes/RuntimeVerification.scala @@ -0,0 +1,26 @@ +package vct.main.modes + +import com.typesafe.scalalogging.LazyLogging +import vct.col.origin.BlameCollector +import vct.main.stages.Stages +import vct.options.Options +import vct.options.types.PathOrStd +import vct.parsers.transform.ConstantBlameProvider + +object RuntimeVerification extends LazyLogging { + + def verifyWithOptions(options: Options, inputs: Seq[PathOrStd]) = { + val collector = BlameCollector() + val stages = Stages.runtimeVerificationWithOptions(options, ConstantBlameProvider(collector)) + stages.run(inputs) match { + case Left(value) => logger.error(value.text) + case Right(()) => logger.info("Runtime terminated successfully.") + } + } + + def runOptions(options: Options): Int = { + verifyWithOptions(options, options.inputs) + 0 + } + +} diff --git a/src/main/vct/main/stages/CodeGeneration.scala b/src/main/vct/main/stages/CodeGeneration.scala index 50938eed54..ce9b703893 100644 --- a/src/main/vct/main/stages/CodeGeneration.scala +++ b/src/main/vct/main/stages/CodeGeneration.scala @@ -9,6 +9,7 @@ import vct.importer.Util import vct.main.stages.Transformation.writeOutFunctions import vct.options.Options import vct.options.types.{Backend, PathOrStd} +import vct.rewrite.runtime.GenerateJava import vct.rewrite.veymont.ParalleliseEndpoints object CodeGeneration { @@ -29,6 +30,12 @@ object CodeGeneration { channelClass = Util.loadJavaClass(options.veymontChannel, options.getParserDebugOptions), ) } + + def runtimeGenerationOfOptions(options: Options): RuntimeGeneration = + RuntimeGeneration( + onBeforePassKey = writeOutFunctions(options.outputBeforePass), + onAfterPassKey = writeOutFunctions(options.outputAfterPass) + ) } class CodeGeneration(val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)], @@ -65,3 +72,9 @@ case class VeyMontGeneration(override val onBeforePassKey: Seq[(String, Verifica extends CodeGeneration(onBeforePassKey, onAfterPassKey, Seq( ParalleliseEndpoints.withArg(channelClass), )) + +case class RuntimeGeneration(override val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil, + override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil) + extends CodeGeneration(onBeforePassKey, onAfterPassKey, Seq( + GenerateJava + )) diff --git a/src/main/vct/main/stages/Output.scala b/src/main/vct/main/stages/Output.scala index ca808b0149..5f81a0fbb4 100644 --- a/src/main/vct/main/stages/Output.scala +++ b/src/main/vct/main/stages/Output.scala @@ -11,6 +11,10 @@ import vct.parsers.ParseResult import java.nio.file.{Files, Path} case object Output { + def runtimeOfOptions(options: Options) = { + Output(options.runtimeOutput, Ctx.Java) + } + def vesuvOfOptions(options: Options): Stages[ParseResult[_ <: Generation], Unit] = FunctionStage((pr: ParseResult[_ <: Generation]) => Program(pr.decls)(DiagnosticOrigin)(DiagnosticOrigin)) .thenRun(Output(options.vesuvOutput, Ctx.PVL)) @@ -30,7 +34,7 @@ case class Output(out: Path, syntax: Ctx.Syntax) extends Stage[Node[_ <: Generat val namer = Namer[G](syntax) namer.name(in) val names = namer.finish - val ctx = Ctx(syntax = syntax, names = names.asInstanceOf[Map[Declaration[_], String]]) + val ctx = Ctx(syntax = syntax, width=250, names = names.asInstanceOf[Map[Declaration[_], String]]) // If possible (if a directory is given as output), print all classes to separate files if (in.isInstanceOf[Program[G]] && Files.isDirectory(out)) { diff --git a/src/main/vct/main/stages/Stages.scala b/src/main/vct/main/stages/Stages.scala index 658452a390..b89301e72f 100644 --- a/src/main/vct/main/stages/Stages.scala +++ b/src/main/vct/main/stages/Stages.scala @@ -1,10 +1,10 @@ package vct.main.stages import hre.progress.Progress -import vct.col.ast.{Program, Verification, BipTransition} +import vct.col.ast.{BipTransition, Program, Verification} import vct.col.rewrite.Generation import vct.options.Options -import vct.parsers.transform.BlameProvider +import vct.parsers.transform.{BlameProvider, ConstantBlameProvider} import vct.result.VerificationError import hre.io.Readable import hre.stages.Stages @@ -15,6 +15,7 @@ import viper.api.backend.silicon.Silicon import scala.collection.mutable case object Stages { + def silicon(blameProvider: BlameProvider, bipResults: BIP.VerificationResults): Stages[Seq[Readable], Unit] = { Parsing(blameProvider) .thenRun(Resolution(blameProvider, vct.parsers.debug.DebugOptions.NONE)) @@ -83,4 +84,13 @@ case object Stages { .thenRun(Resolution.ofOptions(options, blameProvider)) .thenRun(PrintCFG.ofOptions(options)) } + + def runtimeVerificationWithOptions(options: Options, blameProvider: BlameProvider): Stages[Seq[Readable], Unit] = { + Parsing.ofOptions(options, blameProvider) + .thenRun(Resolution.ofOptions(options, blameProvider)) + .thenRun(Transformation.runtimeTransformationOfOptions(options)) + .thenRun(CodeGeneration.runtimeGenerationOfOptions(options)) + .thenRun(Output.runtimeOfOptions(options)) + } + } \ No newline at end of file diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index 504969dd50..e10bb99321 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/src/main/vct/main/stages/Transformation.scala @@ -26,9 +26,11 @@ import vct.result.VerificationError.SystemError import vct.rewrite.adt.ImportSetCompat import vct.rewrite.{EncodeRange, EncodeResourceValues, ExplicitResourceValues, HeapVariableToRef, MonomorphizeClass, SmtlibToProverTypes} import vct.rewrite.lang.ReplaceSYCLTypes +import vct.rewrite.runtime._ import vct.rewrite.veymont.{DeduplicateSeqGuards, EncodeSeqBranchUnanimity, EncodeSeqProg, EncodeUnpointedGuard, GenerateSeqProgPermissions, SplitSeqGuards} object Transformation { + case class TransformationCheckError(pass: RewriterBuilder, errors: Seq[(Program[_], CheckError)]) extends SystemError { override def text: String = s"The ${pass.key} rewrite caused the AST to no longer typecheck:\n" + errors.map { @@ -81,6 +83,13 @@ object Transformation { onAfterPassKey = writeOutFunctions(options.outputAfterPass), ) } + + def runtimeTransformationOfOptions(options: Options): Transformation = + RuntimeTransformation( + onBeforePassKey = writeOutFunctions(options.outputBeforePass), + onAfterPassKey = writeOutFunctions(options.outputAfterPass), + ) + } /** @@ -90,9 +99,9 @@ object Transformation { * pass chain. * * @param onBeforePassKey Execute a side effect just before a rewrite pass is executed. - * @param onAfterPassKey Execute a side effect just after a rewrite pass is executed. The consistency check is done - * before the side effect is performed. - * @param passes The list of rewrite passes to execute. + * @param onAfterPassKey Execute a side effect just after a rewrite pass is executed. The consistency check is done + * before the side effect is performed. + * @param passes The list of rewrite passes to execute. */ class Transformation ( @@ -101,6 +110,7 @@ class Transformation val passes: Seq[RewriterBuilder] ) extends Stage[Verification[_ <: Generation], Verification[_ <: Generation]] with LazyLogging { override def friendlyName: String = "Transformation" + override def progressWeight: Int = 10 override def run(input: Verification[_ <: Generation]): Verification[_ <: Generation] = { @@ -160,15 +170,15 @@ class Transformation /** * Defines the rewrite chain appropriate for the Viper backends: Silicon and Carbon. * - * @param adtImporter Decides how to import the definition of the built-in axiomatically-defined datatypes. - * @param onBeforePassKey Execute a side effect just before a rewrite pass is executed. - * @param onAfterPassKey Execute a side effect just after a rewrite pass is executed. The consistency check is done - * before the side effect is performed. + * @param adtImporter Decides how to import the definition of the built-in axiomatically-defined datatypes. + * @param onBeforePassKey Execute a side effect just before a rewrite pass is executed. + * @param onAfterPassKey Execute a side effect just after a rewrite pass is executed. The consistency check is done + * before the side effect is performed. * @param simplifyBeforeRelations The list of passes to execute at the appropriate point for simplification, just before * quantified integer relations are simplified. - * @param simplifyAfterRelations The list of passes to execute at the appropriate point for simplification, just after - * quantified integer relations are simplified. - * @param checkSat Check that non-trivial contracts are satisfiable. + * @param simplifyAfterRelations The list of passes to execute at the appropriate point for simplification, just after + * quantified integer relations are simplified. + * @param checkSat Check that non-trivial contracts are satisfiable. */ case class SilverTransformation ( @@ -183,145 +193,141 @@ case class SilverTransformation splitVerificationByProcedure: Boolean = false, veymontGeneratePermissions: Boolean = false, ) extends Transformation(onBeforePassKey, onAfterPassKey, Seq( - // Replace leftover SYCL types - ReplaceSYCLTypes, - CFloatIntCoercion, - - ComputeBipGlue, - InstantiateBipSynchronizations, - EncodeBipPermissions, - EncodeBip.withArg(bipResults), - - // Remove the java.lang.Object -> java.lang.Object inheritance loop - NoSupportSelfLoop, - - // Delete stuff that may be declared unsupported at a later stage - FilterSpecIgnore, - - // Normalize AST - TruncDivMod, - Disambiguate, // Resolve overloaded operators (+, subscript, etc.) - DisambiguateLocation, // Resolve location type - EncodeRangedFor, - - // VeyMont sequential program encoding - SplitSeqGuards, - EncodeUnpointedGuard, - DeduplicateSeqGuards, - GenerateSeqProgPermissions.withArg(veymontGeneratePermissions), - EncodeSeqBranchUnanimity, - EncodeSeqProg, - - EncodeString, // Encode spec string as seq - EncodeChar, - - CollectLocalDeclarations, // all decls in Scope - DesugarPermissionOperators, // no PointsTo, \pointer, etc. - ReadToValue, // resolve wildcard into fractional permission - TrivialAddrOf, - DesugarCoalescingOperators, // no ?. - PinCollectionTypes, // no anonymous sequences, sets, etc. - QuantifySubscriptAny, // no arr[*] - IterationContractToParBlock, - PropagateContextEverywhere, // inline context_everywhere into loop invariants - EncodeArrayValues, // maybe don't target shift lemmas on generated function for \values - GivenYieldsToArgs, - - CheckProcessAlgebra, - EncodeCurrentThread, - EncodeIntrinsicLock, - EncodeForkJoin, - InlineApplicables, - PureMethodsToFunctions, - RefuteToInvertedAssert, - ExplicitResourceValues, - EncodeResourceValues, - - // Encode parallel blocks - EncodeSendRecv, - ParBlockEncoder, - - // Extract explicitly extracted code sections, which ban continue/break/return/goto outside them. - SpecifyImplicitLabels, - EncodeExtract, - - // Encode exceptional behaviour (no more continue/break/return/try/throw) - SwitchToGoto, - ContinueToBreak, - EncodeBreakReturn, - - ) ++ simplifyBeforeRelations ++ Seq( - SimplifyQuantifiedRelations, - SimplifyNestedQuantifiers, - TupledQuantifiers, - ) ++ simplifyAfterRelations ++ Seq( - UntupledQuantifiers, - - // Encode proof helpers - EncodeProofHelpers.withArg(inferHeapContextIntoFrame), - ImportSetCompat.withArg(adtImporter), - - // Make final fields constant functions. Explicitly before ResolveExpressionSideEffects, because that pass will - // 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, - - // Resolve side effects including method invocations, for encodetrythrowsignals. - ResolveExpressionSideChecks, - ResolveExpressionSideEffects, - EncodeTryThrowSignals, - - ResolveScale, - MonomorphizeClass, - // No more classes - ClassToRef, - HeapVariableToRef, - - CheckContractSatisfiability.withArg(checkSat), - - DesugarCollectionOperators, - EncodeNdIndex, - - ExtractInlineQuantifierPatterns, - // Translate internal types to domains - FloatToRat, - SmtlibToProverTypes, - EnumToDomain, - ImportArray.withArg(adtImporter), - ImportPointer.withArg(adtImporter), - ImportMapCompat.withArg(adtImporter), - ImportEither.withArg(adtImporter), - ImportTuple.withArg(adtImporter), - ImportOption.withArg(adtImporter), - ImportFrac.withArg(adtImporter), - ImportNothing.withArg(adtImporter), - ImportVoid.withArg(adtImporter), - ImportNull.withArg(adtImporter), - ImportAny.withArg(adtImporter), - ImportViperOrder.withArg(adtImporter), - EncodeRange.withArg(adtImporter), - - // All locations with a value should now be SilverField - EncodeForPermWithValue, - - ExtractInlineQuantifierPatterns, - RewriteTriggerADTFunctions, - MonomorphizeContractApplicables, - - // Silver compat (basically no new nodes) - FinalizeArguments, - ExplicitADTTypeArgs, - ForLoopToWhileLoop, - BranchToIfElse, - EvaluationTargetDummy, - - // Final translation to rigid silver nodes - SilverIntRatCoercion, - // PB TODO: PinSilverNodes has now become a collection of Silver oddities, it should be more structured / split out. - PinSilverNodes, - - Explode.withArg(splitVerificationByProcedure), - )) + // Replace leftover SYCL types + ReplaceSYCLTypes, + CFloatIntCoercion, + + ComputeBipGlue, + InstantiateBipSynchronizations, + EncodeBipPermissions, + EncodeBip.withArg(bipResults), + + // Remove the java.lang.Object -> java.lang.Object inheritance loop + NoSupportSelfLoop, + + // Delete stuff that may be declared unsupported at a later stage + FilterSpecIgnore, + + // Normalize AST + TruncDivMod, + Disambiguate, // Resolve overloaded operators (+, subscript, etc.) + DisambiguateLocation, // Resolve location type + EncodeRangedFor, + + // VeyMont sequential program encoding + SplitSeqGuards, + EncodeUnpointedGuard, + DeduplicateSeqGuards, + GenerateSeqProgPermissions.withArg(veymontGeneratePermissions), + EncodeSeqBranchUnanimity, + EncodeSeqProg, + + EncodeString, // Encode spec string as seq + EncodeChar, + + CollectLocalDeclarations, // all decls in Scope + DesugarPermissionOperators, // no PointsTo, \pointer, etc. + ReadToValue, // resolve wildcard into fractional permission + TrivialAddrOf, + DesugarCoalescingOperators, // no ?. + PinCollectionTypes, // no anonymous sequences, sets, etc. + QuantifySubscriptAny, // no arr[*] + IterationContractToParBlock, + PropagateContextEverywhere, // inline context_everywhere into loop invariants + EncodeArrayValues, // maybe don't target shift lemmas on generated function for \values + GivenYieldsToArgs, + + CheckProcessAlgebra, + EncodeCurrentThread, + EncodeIntrinsicLock, + EncodeForkJoin, + InlineApplicables, + PureMethodsToFunctions, + RefuteToInvertedAssert, + ExplicitResourceValues, + EncodeResourceValues, + + // Encode parallel blocks + EncodeSendRecv, + ParBlockEncoder, + + // Extract explicitly extracted code sections, which ban continue/break/return/goto outside them. + SpecifyImplicitLabels, + EncodeExtract, + + // Encode exceptional behaviour (no more continue/break/return/try/throw) + SwitchToGoto, + ContinueToBreak, + EncodeBreakReturn, + +) ++ simplifyBeforeRelations ++ Seq( + SimplifyQuantifiedRelations, + SimplifyNestedQuantifiers, + TupledQuantifiers, +) ++ simplifyAfterRelations ++ Seq( + UntupledQuantifiers, + + // Encode proof helpers + EncodeProofHelpers.withArg(inferHeapContextIntoFrame), + ImportSetCompat.withArg(adtImporter), + + // Make final fields constant functions. Explicitly before ResolveExpressionSideEffects, because that pass will + // 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, + + // Resolve side effects including method invocations, for encodetrythrowsignals. + ResolveExpressionSideChecks,ResolveExpressionSideEffects, + EncodeTryThrowSignals, + + ResolveScale, + MonomorphizeClass,// No more classes + ClassToRef, + HeapVariableToRef, + + CheckContractSatisfiability.withArg(checkSat), + + DesugarCollectionOperators, + EncodeNdIndex, + + ExtractInlineQuantifierPatterns, + // Translate internal types to domains + FloatToRat, + SmtlibToProverTypes,EnumToDomain, + ImportArray.withArg(adtImporter), + ImportPointer.withArg(adtImporter), + ImportMapCompat.withArg(adtImporter), + ImportEither.withArg(adtImporter), + ImportTuple.withArg(adtImporter), + ImportOption.withArg(adtImporter), + ImportFrac.withArg(adtImporter), + ImportNothing.withArg(adtImporter), + ImportVoid.withArg(adtImporter), + ImportNull.withArg(adtImporter), + ImportAny.withArg(adtImporter), + ImportViperOrder.withArg(adtImporter),EncodeRange.withArg(adtImporter), + + // All locations with a value should now be SilverField + EncodeForPermWithValue, + + ExtractInlineQuantifierPatterns, + RewriteTriggerADTFunctions, + MonomorphizeContractApplicables, + + // Silver compat (basically no new nodes) + FinalizeArguments, + ExplicitADTTypeArgs, + ForLoopToWhileLoop, + BranchToIfElse, + EvaluationTargetDummy, + + // Final translation to rigid silver nodes + SilverIntRatCoercion, + // PB TODO: PinSilverNodes has now become a collection of Silver oddities, it should be more structured / split out. + PinSilverNodes, + + Explode.withArg(splitVerificationByProcedure), +)) case class VeyMontTransformation(override val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil, override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil) @@ -332,4 +338,20 @@ case class VeyMontTransformation(override val onBeforePassKey: Seq[(String, Veri )) - +case class RuntimeTransformation(override val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil, + override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil) + extends Transformation(onBeforePassKey, onAfterPassKey, Seq( + CreateLedger, + RemoveSelfLoops, + RefactorGeneratedCode, +// CreateFieldPermissions, + AddPermissionsOnCreate, +// CreatePredicates, //Create predicate templates for all specified predicates -> since you only need to check the predicate condition if the predicate is folded In the pre and post conditions then we need to do the check if the thread holds a predicate + CheckPermissionsBlocksMethod, //Basic permission check + CreatePrePostConditions, //Basic permission check for pre and post conditions by making use of the RewriteContractExpr + CreatePredicateFoldUnfold, + CreateLocking, //Create predicate instance for the Lock and use the constructor and synchronize keyword to check it + CreateLoopInvariants, //Create pre and post inside loop for all the specified conditions (maybe we can reuse code from the previous assertion checks) by making use of the RewriteContractExpr + ForkJoinPermissionTransfer, //Creates the permission transfer when a fork method occurs (when a start method is called) +// GenerateJava //Generates valid java code so that it can be executed properly + )) \ No newline at end of file diff --git a/src/main/vct/options/Options.scala b/src/main/vct/options/Options.scala index a6c914157f..4708231ea7 100644 --- a/src/main/vct/options/Options.scala +++ b/src/main/vct/options/Options.scala @@ -263,6 +263,19 @@ case object Options { .action((p, c) => c.copy(devVeymontAllowAssign = true)) .text("Do not error when plain assignment is used in seq_programs"), + note(""), + note("Runtime Verification Mode"), + opt[Unit]("runtime") + .action((_, c) => c.copy(mode = Mode.RuntimeVerification)) + .text("Use runtime verification to test the program") + .children( + opt[Path]("runtime-output").valueName("") + .action((path, c) => c.copy(runtimeOutput = path)), + opt[Int]("runtime-timeout").valueName("") + .action((timeout, c) => c.copy(runtimeTimeout = timeout)) + ), + + note(""), note("VeyMont Mode"), opt[Unit]("veymont") @@ -400,6 +413,10 @@ case class Options devViperProverLogFile: Option[Path] = None, + //Runtime verification options + runtimeOutput: Path = null, + runtimeTimeout: Int = 60, + // VeyMont options veymontOutput: Path = null, // required veymontChannel: PathOrStd = PathOrStd.Path(getVeymontChannel), diff --git a/src/main/vct/options/types/Mode.scala b/src/main/vct/options/types/Mode.scala index 5405e70dc0..a7728b9538 100644 --- a/src/main/vct/options/types/Mode.scala +++ b/src/main/vct/options/types/Mode.scala @@ -8,5 +8,6 @@ case object Mode { case object Verify extends Mode case object VeyMont extends Mode case object VeSUV extends Mode + case object RuntimeVerification extends Mode case object CFG extends Mode } diff --git a/src/parsers/antlr4/SpecLexer.g4 b/src/parsers/antlr4/SpecLexer.g4 index dbe017a447..f0c21b40da 100644 --- a/src/parsers/antlr4/SpecLexer.g4 +++ b/src/parsers/antlr4/SpecLexer.g4 @@ -127,6 +127,7 @@ VAL_LEFT: 'Left'; VAL_RIGHT: 'Right'; VAL_VALUE: 'Value'; +POSTJOIN: 'postJoin'; UNFOLDING: '\\unfolding'; UNFOLDING_JAVA: '\\Unfolding'; IN: '\\in'; diff --git a/src/parsers/antlr4/SpecParser.g4 b/src/parsers/antlr4/SpecParser.g4 index 1e4bab6783..7f46606245 100644 --- a/src/parsers/antlr4/SpecParser.g4 +++ b/src/parsers/antlr4/SpecParser.g4 @@ -70,6 +70,7 @@ valStatement | 'open' langExpr ';' # valOpen | 'close' langExpr ';' # valClose | 'assert' langExpr ';' # valAssert + | langExpr '.' 'postJoin' '(' langExpr ')' ';' # valPostJoin | 'assume' langExpr ';' # valAssume | 'inhale' langExpr ';' # valInhale | 'exhale' langExpr ';' # valExhale diff --git a/src/parsers/vct/parsers/transform/JavaToCol.scala b/src/parsers/vct/parsers/transform/JavaToCol.scala index 342f3b1b65..88956c0ef4 100644 --- a/src/parsers/vct/parsers/transform/JavaToCol.scala +++ b/src/parsers/vct/parsers/transform/JavaToCol.scala @@ -1131,6 +1131,7 @@ case class JavaToCol[G](override val baseOrigin: Origin, case ValOpen(_, _, _) => ??(stat) case ValClose(_, _, _) => ??(stat) case ValAssert(_, assn, _) => Assert(convert(assn))(blame(stat)) + case ValPostJoin(obj, _, _, _, arg, _, _) => RuntimePostJoin(convert(obj), convert(arg))(blame(stat)) case ValAssume(_, assn, _) => Assume(convert(assn)) case ValInhale(_, resource, _) => Inhale(convert(resource)) case ValExhale(_, resource, _) => Exhale(convert(resource))(blame(stat)) diff --git a/src/parsers/vct/parsers/transform/systemctocol/engine/ClassTransformer.java b/src/parsers/vct/parsers/transform/systemctocol/engine/ClassTransformer.java index b23134a1df..72babab3fc 100644 --- a/src/parsers/vct/parsers/transform/systemctocol/engine/ClassTransformer.java +++ b/src/parsers/vct/parsers/transform/systemctocol/engine/ClassTransformer.java @@ -50,7 +50,7 @@ public Class create_process_class(ProcessClass process) { // 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 TClass<>(main_cls_ref, Seqs.empty(), OriGen.create()), col_system.NO_FLAGS, Option.empty(), 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(), @@ -91,7 +91,7 @@ public Class create_state_class(StateClass state_class) { // 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 TClass<>(main_cls_ref, Seqs.empty(), OriGen.create()), col_system.NO_FLAGS, Option.empty(), 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(), diff --git a/src/parsers/vct/parsers/transform/systemctocol/engine/ExpressionTransformer.java b/src/parsers/vct/parsers/transform/systemctocol/engine/ExpressionTransformer.java index 5bec2e09fb..56e4519269 100644 --- a/src/parsers/vct/parsers/transform/systemctocol/engine/ExpressionTransformer.java +++ b/src/parsers/vct/parsers/transform/systemctocol/engine/ExpressionTransformer.java @@ -1127,7 +1127,7 @@ private Ref> create_random_function(Type return_type) { new UnitAccountedPredicate<>(col_system.TRUE, OriGen.create()), col_system.TRUE, col_system.NO_SIGNALS, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), new GeneratedBlame<>(), OriGen.create()); InstanceMethod randomizer = new InstanceMethod<>(return_type, col_system.NO_VARS, col_system.NO_VARS, col_system.NO_VARS, - Option.empty(), contract, false, true, new GeneratedBlame<>(), OriGen.create(name)); + Option.empty(), contract, false, true, false, new GeneratedBlame<>(), OriGen.create(name)); newly_generated_methods.add(randomizer); // Return reference to the new method diff --git a/src/parsers/vct/parsers/transform/systemctocol/engine/FunctionTransformer.java b/src/parsers/vct/parsers/transform/systemctocol/engine/FunctionTransformer.java index 00fbd88e07..4ccfad3081 100644 --- a/src/parsers/vct/parsers/transform/systemctocol/engine/FunctionTransformer.java +++ b/src/parsers/vct/parsers/transform/systemctocol/engine/FunctionTransformer.java @@ -91,7 +91,7 @@ public InstanceMethod transform_method(SCFunction function, ProcessClass proc // Create method InstanceMethod new_method = new InstanceMethod<>(return_type, parameters, col_system.NO_VARS, col_system.NO_VARS, - Option.apply(body), contract, false, pure, new GeneratedBlame<>(), OriGen.create(function.getName())); + Option.apply(body), contract, false, pure, false, new GeneratedBlame<>(), OriGen.create(function.getName())); // Register method in COL system context and return col_system.add_instance_method(function, sc_inst, process, new_method); diff --git a/src/parsers/vct/parsers/transform/systemctocol/engine/KnownTypeTransformer.java b/src/parsers/vct/parsers/transform/systemctocol/engine/KnownTypeTransformer.java index 3165bba55d..20554051ee 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 TClass<>(ref_to_cls, Seqs.empty(), OriGen.create()), col_system.NO_FLAGS, Option.empty(), OriGen.create(name.toLowerCase()))); } @@ -119,10 +119,10 @@ 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 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")); + InstanceField m = new InstanceField<>(new TClass<>(main_cls_ref, Seqs.empty(), OriGen.create()), col_system.NO_FLAGS, Option.empty(), OriGen.create("m")); + InstanceField buf = new InstanceField<>(new TSeq<>(t, OriGen.create()), col_system.NO_FLAGS, Option.empty(), OriGen.create("buffer")); + InstanceField nr_read = new InstanceField<>(col_system.T_INT, col_system.NO_FLAGS, Option.empty(), OriGen.create("num_read")); + InstanceField written = new InstanceField<>(new TSeq<>(t, OriGen.create()), col_system.NO_FLAGS, Option.empty(), OriGen.create("written")); col_system.add_primitive_instance_field(sc_inst, Constants.FIFO_BUFFER, buf); col_system.add_primitive_instance_field(sc_inst, Constants.FIFO_NUM_READ, nr_read); col_system.add_primitive_instance_field(sc_inst, Constants.FIFO_WRITTEN, written); @@ -336,7 +336,7 @@ private InstanceMethod create_fifo_read_method(Type t, InstanceField m, // Finishing the method ApplicableContract contract = new ApplicableContract<>(precondition, postcondition, col_system.TRUE, col_system.NO_SIGNALS, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), new GeneratedBlame<>(), OriGen.create()); - return new InstanceMethod<>(t, col_system.NO_VARS, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), contract, false, false, + return new InstanceMethod<>(t, col_system.NO_VARS, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), contract, false, false, false, new GeneratedBlame<>(), OriGen.create("fifo_read")); } @@ -407,7 +407,7 @@ private InstanceMethod create_fifo_write_method(Type t, InstanceField m // Finishing the method ApplicableContract contract = new ApplicableContract<>(precondition, postcondition, col_system.TRUE, col_system.NO_SIGNALS, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), new GeneratedBlame<>(), OriGen.create()); - return new InstanceMethod<>(col_system.T_VOID, params, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), contract, false, false, + return new InstanceMethod<>(col_system.T_VOID, params, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), contract, false, false,false, new GeneratedBlame<>(), OriGen.create("fifo_write")); } @@ -511,7 +511,7 @@ private InstanceMethod create_fifo_update_method(InstanceField m, Instance ApplicableContract contract = new ApplicableContract<>(precondition, postcondition, col_system.TRUE, col_system.NO_SIGNALS, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), new GeneratedBlame<>(), OriGen.create()); return new InstanceMethod<>(col_system.T_VOID, col_system.NO_VARS, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), - contract, false, false, new GeneratedBlame<>(), OriGen.create("fifo_update")); + contract, false, false,false, new GeneratedBlame<>(), OriGen.create("fifo_update")); } /** @@ -524,9 +524,9 @@ 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 val = new InstanceField<>(t, col_system.NO_FLAGS, OriGen.create("val")); - InstanceField _val = new InstanceField<>(t, col_system.NO_FLAGS, OriGen.create("_val")); + InstanceField m = new InstanceField<>(new TClass<>(main_cls_ref, Seqs.empty(), OriGen.create()), col_system.NO_FLAGS, Option.empty(), OriGen.create("m")); + InstanceField val = new InstanceField<>(t, col_system.NO_FLAGS, Option.empty(), OriGen.create("val")); + InstanceField _val = new InstanceField<>(t, col_system.NO_FLAGS, Option.empty(), OriGen.create("_val")); // Permission invariant for the Main class InstancePredicate inv = create_signal_permission_invariant(m, val, _val); @@ -669,7 +669,7 @@ private InstanceMethod create_signal_read_method(Type t, InstanceField // Finishing the method ApplicableContract contract = new ApplicableContract<>(precondition, postcondition, col_system.TRUE, col_system.NO_SIGNALS, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), new GeneratedBlame<>(), OriGen.create()); - return new InstanceMethod<>(t, col_system.NO_VARS, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), contract, false, false, + return new InstanceMethod<>(t, col_system.NO_VARS, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), contract, false, false,false, new GeneratedBlame<>(), OriGen.create("signal_read")); } @@ -727,7 +727,7 @@ private InstanceMethod create_signal_write_method(Type t, InstanceField ApplicableContract contract = new ApplicableContract<>(precondition, postcondition, col_system.TRUE, col_system.NO_SIGNALS, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), new GeneratedBlame<>(), OriGen.create()); return new InstanceMethod<>(col_system.T_VOID, params, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), contract, - false, false, new GeneratedBlame<>(), OriGen.create("signal_write")); + false, false,false, new GeneratedBlame<>(), OriGen.create("signal_write")); } /** @@ -800,7 +800,7 @@ private InstanceMethod create_signal_update_method(InstanceField m, Instan ApplicableContract contract = new ApplicableContract<>(precondition, postcondition, col_system.TRUE, col_system.NO_SIGNALS, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), new GeneratedBlame<>(), OriGen.create()); return new InstanceMethod<>(col_system.T_VOID, col_system.NO_VARS, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), - contract, false, false, new GeneratedBlame<>(), OriGen.create("signal_update")); + contract, false, false,false, new GeneratedBlame<>(), OriGen.create("signal_update")); } /** diff --git a/src/parsers/vct/parsers/transform/systemctocol/engine/MainTransformer.java b/src/parsers/vct/parsers/transform/systemctocol/engine/MainTransformer.java index a17b920286..d7e903cb6a 100644 --- a/src/parsers/vct/parsers/transform/systemctocol/engine/MainTransformer.java +++ b/src/parsers/vct/parsers/transform/systemctocol/engine/MainTransformer.java @@ -192,7 +192,7 @@ private void create_instances() { Type t = new TClass<>(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))); + InstanceField inst = new InstanceField<>(t, col_system.NO_FLAGS, Option.empty(), OriGen.create(create_instance_name(process_class))); col_system.add_instance_mapping(process_class, inst); processes.add(inst); class_by_field.put(inst, process_class); @@ -207,7 +207,7 @@ private void create_instances() { Type t = new TClass<>(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))); + InstanceField inst = new InstanceField<>(t, col_system.NO_FLAGS, Option.empty(), OriGen.create(create_instance_name(state_class))); col_system.add_instance_mapping(state_class, inst); state_classes.add(inst); class_by_field.put(inst, state_class); @@ -806,7 +806,7 @@ private InstanceMethod create_find_minimum_advance() { // Generate contract and method and return ApplicableContract contract = col_system.to_applicable_contract(col_system.TRUE, col_system.fold_star(ensures)); return new InstanceMethod<>(col_system.T_INT, params, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), contract, - false, true, new GeneratedBlame<>(), OriGen.create("find_minimum_advance")); + false, true,false, new GeneratedBlame<>(), OriGen.create("find_minimum_advance")); } /** @@ -973,7 +973,7 @@ private Expr create_helper_context() { */ private InstanceMethod create_abstract_method(ApplicableContract contract, String method_name) { return new InstanceMethod<>(col_system.T_VOID, col_system.NO_VARS, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), - contract, false, false, new GeneratedBlame<>(), OriGen.create(method_name)); + contract, false, false,false, new GeneratedBlame<>(), OriGen.create(method_name)); } /** @@ -986,7 +986,7 @@ private void create_scheduler() { Expr context = create_scheduler_contract(); ApplicableContract contract = col_system.to_applicable_contract(context, context); scheduler = new InstanceMethod<>(col_system.T_VOID, col_system.NO_VARS, col_system.NO_VARS, col_system.NO_VARS, - Option.apply(body), contract, false, false, new GeneratedBlame<>(), OriGen.create("main")); + Option.apply(body), contract, false, false,false, new GeneratedBlame<>(), OriGen.create("main")); } /** diff --git a/src/parsers/vct/parsers/transform/systemctocol/engine/Transformer.java b/src/parsers/vct/parsers/transform/systemctocol/engine/Transformer.java index 1c4d9a4c75..5e97171bf6 100644 --- a/src/parsers/vct/parsers/transform/systemctocol/engine/Transformer.java +++ b/src/parsers/vct/parsers/transform/systemctocol/engine/Transformer.java @@ -8,6 +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 scala.Option; import vct.col.ast.Class; import vct.col.ast.InstanceField; import vct.parsers.transform.systemctocol.exceptions.SystemCFormatException; @@ -253,9 +254,9 @@ private void scan_enums() { * Main class itself. */ private void create_minimal_main() { - col_system.set_process_state(new InstanceField<>(col_system.T_SEQ_INT, col_system.NO_FLAGS, OriGen.create("process_state"))); - col_system.set_event_state(new InstanceField<>(col_system.T_SEQ_INT, col_system.NO_FLAGS, OriGen.create("event_state"))); - col_system.set_primitive_channel_update(new InstanceField<>(col_system.T_SEQ_BOOL, col_system.NO_FLAGS, OriGen.create("primitive_channel_update"))); + col_system.set_process_state(new InstanceField<>(col_system.T_SEQ_INT, col_system.NO_FLAGS, Option.empty(), OriGen.create("process_state"))); + col_system.set_event_state(new InstanceField<>(col_system.T_SEQ_INT, col_system.NO_FLAGS, Option.empty(), OriGen.create("event_state"))); + col_system.set_primitive_channel_update(new InstanceField<>(col_system.T_SEQ_BOOL, col_system.NO_FLAGS, Option.empty(), OriGen.create("primitive_channel_update"))); } /** @@ -267,7 +268,7 @@ private void translate_system_parameters() { // System parameters are declared as global const int fields TODO: Discuss this encoding if (global_variable.isConst() && col_system.parse_type(global_variable.getType()).equals(col_system.T_INT)) { String var_name = "PARAM_" + global_variable.getName().toUpperCase(); - InstanceField parameter_field = new InstanceField<>(col_system.T_INT, col_system.NO_FLAGS, OriGen.create(var_name)); + InstanceField parameter_field = new InstanceField<>(col_system.T_INT, col_system.NO_FLAGS, Option.empty(), OriGen.create(var_name)); col_system.add_parameter(global_variable, parameter_field); } } @@ -276,7 +277,7 @@ private void translate_system_parameters() { for (SCClassInstance sc_inst : sc_system.getInstances()) { // Check if any instance is a FIFO queue, add the parameter if (sc_inst.getType().equals(Constants.CLASS_FIFO_INT) || sc_inst.getType().equals(Constants.CLASS_FIFO_BOOL)) { - InstanceField buffer_size = new InstanceField<>(col_system.T_INT, col_system.NO_FLAGS, OriGen.create("BUFFER_SIZE")); + InstanceField buffer_size = new InstanceField<>(col_system.T_INT, col_system.NO_FLAGS, Option.empty(), OriGen.create("BUFFER_SIZE")); col_system.set_fifo_size_parameter(buffer_size); break; } diff --git a/src/parsers/vct/parsers/transform/systemctocol/engine/VariableTransformer.java b/src/parsers/vct/parsers/transform/systemctocol/engine/VariableTransformer.java index 52ac710be6..94250c7990 100644 --- a/src/parsers/vct/parsers/transform/systemctocol/engine/VariableTransformer.java +++ b/src/parsers/vct/parsers/transform/systemctocol/engine/VariableTransformer.java @@ -3,6 +3,7 @@ import de.tub.pes.syscir.sc_model.SCVariable; import de.tub.pes.syscir.sc_model.variables.SCArray; import de.tub.pes.syscir.sc_model.variables.SCClassInstance; +import scala.Option; import vct.col.ast.InstanceField; import vct.col.ast.TArray; import vct.col.ast.Type; @@ -61,7 +62,7 @@ public InstanceField transform_variable_to_instance_field(SCVariable sc_var, if (result == null) { // If no such field exists, create a new one Origin o = OriGen.create((fun_name.isEmpty()) ? sc_var.getName() : sc_var.getName() + "_" + fun_name); - result = new InstanceField<>(get_type(sc_var), col_system.NO_FLAGS, o); + result = new InstanceField<>(get_type(sc_var), col_system.NO_FLAGS, Option.empty(), o); col_system.add_instance_field_mapping(sc_inst, sc_var, result); } diff --git a/src/rewrite/vct/rewrite/runtime/AddPermissionsOnCreate.scala b/src/rewrite/vct/rewrite/runtime/AddPermissionsOnCreate.scala new file mode 100644 index 0000000000..e79755cd55 --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/AddPermissionsOnCreate.scala @@ -0,0 +1,116 @@ +package vct.rewrite.runtime + +import hre.util.ScopedStack +import vct.col.ast.RewriteHelpers._ +import vct.col.ast.{PrimitiveType, _} +import vct.col.util.AstBuildHelpers._ +import vct.col.origin.{DiagnosticOrigin, Origin} +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} +import vct.rewrite.runtime.util.LedgerHelper.{LedgerMethodBuilderHelper, LedgerRewriter} +import vct.rewrite.runtime.util.Util.isExtendingThread +import vct.rewrite.runtime.util.permissionTransfer.PermissionData +import vct.rewrite.runtime.util.{RewriteContractExpr, TransferPermissionRewriter} + +object AddPermissionsOnCreate extends RewriterBuilder { + override def key: String = "addPermissionsOnCreate" + + override def desc: String = "Creates the permissions inside the constructor for each InstanceField of the object" +} + + +case class AddPermissionsOnCreate[Pre <: Generation]() extends Rewriter[Pre] { + + val currentClass: ScopedStack[Class[Pre]] = new ScopedStack() + + implicit var program: Program[Pre] = _ + + implicit var ledger: LedgerMethodBuilderHelper[Post] = _ + + + /** + * Dispatch of the program for debugging and using the program everywhere to look up specific instancefields + * + * @param program Program node + * @return The rewritten program + */ + override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] = { + this.program = program + lazy val newDecl: Seq[GlobalDeclaration[Post]] = globalDeclarations.collect { + val (ledgerHelper, _, otherDeclarations) = LedgerRewriter[Pre](this).rewriteLedger(program) + ledger = ledgerHelper + otherDeclarations.foreach(dispatch) + + }._1 + val test = program.rewrite(declarations = newDecl) + test + } + + /** + * Dispatches declarations + * The java constructor is dispatched and so that permissions are initialized for each instance field + * the class is dispatched to keep track of the current class + * @param decl + */ + override def dispatch(decl: Declaration[Pre]): Unit = { + decl match { + case jc: JavaConstructor[Pre] => dispatchJC(jc) + case cls: Class[Pre] => currentClass.having(cls) { + super.dispatch(cls) + } + case _ => super.dispatch(decl) + } + } + + /** + * Dispatches the java constructor so that it initializes the permissions for each instance field + * if the thread extends the thread class also a join token is set + * @param jc + * @return + */ + private def dispatchJC(jc: JavaConstructor[Pre]): JavaConstructor[Post] = { + implicit val origin: Origin = jc.o + val instanceFields = currentClass.top.declarations.collect { case i: InstanceField[Pre] => i } + val size = instanceFields.size + val obj = ThisObject[Post](this.anySucc(currentClass.top)) + val initInstanceFieldsExpr: MethodInvocation[Post] = if (size == 0) ledger.miInitiatePermission(obj).get else ledger.miInitiatePermission(obj, const(size)).get + val initInstanceFieldsPerm = Eval[Post](initInstanceFieldsExpr) + val newBody = Block[Post](Seq(dispatch(jc.body), initInstanceFieldsPerm, createJoinTokenCall)) + classDeclarations.succeed(jc, jc.rewrite(body = newBody)) + } + + /** + * Creates a join token for the thread if the class extends the thread class + * @return + */ + def createJoinTokenCall : Block[Post] = { + implicit val origin: Origin = DiagnosticOrigin + if (!isExtendingThread(currentClass.top)) { + return Block(Nil) + } + val mi = ledger.miSetJoinToken(ThisObject[Post](this.anySucc(currentClass.top)), RuntimeFractionOne[Post]()).get + Block[Post](Seq(Eval[Post](mi))) + } + + /** + * When a new array is created the permissions are initialized for the array + * @param stat + * @return + */ + override def dispatch(stat: Statement[Pre]): Statement[Rewritten[Pre]] = { + stat match { + case a@Assign(location, na@NewArray(_, dims, _, _)) => + val dispatchedAssign = super.dispatch(a) + val initPermissionArray = Eval[Post](ledger.miInitiatePermission(dispatch(location), dispatch(dims.head)).get)(DiagnosticOrigin) + Block[Post](Seq(dispatchedAssign, initPermissionArray))(DiagnosticOrigin) + case a@Eval(PreAssignExpression(location, na@NewArray(_, dims, _, _))) => + val dispatchedAssign = super.dispatch(a) + val initPermissionArray = Eval[Post](ledger.miInitiatePermission(dispatch(location), dispatch(dims.head)).get)(DiagnosticOrigin) + Block[Post](Seq(dispatchedAssign, initPermissionArray))(DiagnosticOrigin) + case a@Eval(PostAssignExpression(location, na@NewArray(_, dims, _, _))) => + val dispatchedAssign = super.dispatch(a) + val initPermissionArray = Eval[Post](ledger.miInitiatePermission(dispatch(location), dispatch(dims.head)).get)(DiagnosticOrigin) + Block[Post](Seq(dispatchedAssign, initPermissionArray))(DiagnosticOrigin) + case _ => super.dispatch(stat) + } + } +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/runtime/CheckPermissionsBlocksMethod.scala b/src/rewrite/vct/rewrite/runtime/CheckPermissionsBlocksMethod.scala new file mode 100644 index 0000000000..d2c557b6f1 --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/CheckPermissionsBlocksMethod.scala @@ -0,0 +1,249 @@ +package vct.rewrite.runtime + +import hre.util.ScopedStack +import vct.col.ast.RewriteHelpers._ +import vct.col.ast._ +import vct.col.origin.{Origin, PositionRange} +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} +import vct.col.util.AstBuildHelpers._ +import vct.result.VerificationError.Unreachable +import vct.rewrite.runtime.util.permissionTransfer.PermissionData +import vct.rewrite.runtime.util.LedgerHelper._ + +import scala.collection.mutable + +object CheckPermissionsBlocksMethod extends RewriterBuilder { + override def key: String = "CheckPermissionsBlocksMethod" + + override def desc: String = "Creates internal method blocks. In these blocks permissions will be checked" +} + + +case class CheckPermissionsBlocksMethod[Pre <: Generation]() extends Rewriter[Pre] { + + + val isTarget: ScopedStack[Boolean] = ScopedStack() + private val dereferences: ScopedStack[mutable.HashMap[Expr[Pre], Boolean]] = ScopedStack() + var heapChange: Boolean = false + + implicit var program: Program[Pre] = _ + implicit var ledger: LedgerMethodBuilderHelper[Post] = _ + + + /** + * Basic part of rewriting the program to retrieve ledger helper and rewrite the other declarations + * @param program + * @return + */ + override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] = { + this.program = program + lazy val newDecl: Seq[GlobalDeclaration[Post]] = globalDeclarations.collect { + val (ledgerHelper, _, otherDeclarations) = LedgerRewriter[Pre](this).rewriteLedger(program) + ledger = ledgerHelper + isTarget.having(false) { + otherDeclarations.foreach(dispatch) + } + }._1 + program.rewrite(declarations = newDecl) + } + + + /** + * If the statement is an assignment keep track of the target and if it is not a primitive type set the heapChange to true + * If there is scope with a block in it , change the block structure of the block + * if it is an unfold/fold create a new dereferences map so that there are no permission checks in the contract + * @param stat + * @return + */ + override def dispatch(stat: Statement[Pre]): Statement[Rewritten[Pre]] = { + stat match { + case a: Assign[Pre] => a.rewrite(target = isTarget.having(true) { + if(!a.target.t.isInstanceOf[PrimitiveType[Pre]]){ + heapChange = true + } + dispatch(a.target) + }) + case s@Scope(_, b@Block(_)) => s.rewrite(body = determineNewBlockStructure(b)) + case _: Unfold[Pre] | _: Fold[Pre] => dereferences.collect(super.dispatch(stat))._2 + case _ => super.dispatch(stat) + } + } + + /** + * When a dereference is found check if it is a target and if it is not already in the dereferences map + * when there is a change in the heap set the value of heapChange to true + * @param e + * @return + */ + override def dispatch(e: Expr[Pre]): Expr[Rewritten[Pre]] = { + e match { + case mi: MethodInvocation[Pre] if mi.o.getLedgerClassRuntime.nonEmpty => { + heapChange = true + dereferences.collect(super.dispatch(mi))._2 + } + case inv@(_: MethodInvocation[Pre] | _: ProcedureInvocation[Pre]) => heapChange = true; super.dispatch(inv) + case preExpr: PreAssignExpression[Pre] => preExpr.rewrite(isTarget.having(true) { + if(preExpr.target.t.isInstanceOf[PrimitiveType[Pre]]){ + heapChange = true + } + dispatch(preExpr.target) + }) + case postExpr: PostAssignExpression[Pre] => postExpr.rewrite(isTarget.having(true) { + if(postExpr.target.t.isInstanceOf[PrimitiveType[Pre]]){ + heapChange = true + } + dispatch(postExpr.target) + }) + case d@(_: Deref[Pre] | _: AmbiguousSubscript[Pre]) => { + val newD = isTarget.having(false){ super.dispatch(d) } + if (dereferences.isEmpty) return newD + if (isTarget.top) { + dereferences.top += (d -> true) + } else if (!dereferences.top.contains(d)) { + dereferences.top += (d -> false) + } + newD + } + case _ => super.dispatch(e) + } + } + + /** + * Create new statements for the permission checks using the found dereferences + * @param l + * @param write + * @return + */ + private def generatePermissionChecksStatements(l: Expr[Pre], write: Boolean): Statement[Post] = { + implicit val origin: Origin = l.o + + val location: Expr[Post] = l match { + case d: Deref[Pre] => { + val newDataObject: MethodInvocation[Post] = ledger.pmbh.miCreate( + CreateObjectArray[Post]( + Seq(dispatch(d.obj), + dispatch(const[Pre](findNumberInstanceField(program, d.ref.decl).get))) + )).get + ledger.miGetPermission(newDataObject).get + } + case AmbiguousSubscript(coll, index) => { + val newDataObject: MethodInvocation[Post] = ledger.pmbh.miCreate( + CreateObjectArray[Post](Seq(dispatch(coll), dispatch(index)))).get + ledger.miGetPermission(newDataObject).get + } + case _ => throw Unreachable(s"This location type is not supported yet: ${l}") + } + val rangeContent = l.o.find[PositionRange] + val readableContent = l.o.getReadable + + val linenum = rangeContent.map(_.startLineIdx).getOrElse(-1) + val lineDetails: String = (rangeContent, readableContent) match { + case Some(range) -> Some(readable) => readable.readable.readLines()(range.startLineIdx-1).trim + case _ => "unknown line" + } + val check = if (write) (location r_<=> RuntimeFractionOne[Post]()) === const(0) else (location r_<=> RuntimeFractionZero[Post]()) === const(1) + val message = if (write) s"Permission should have been write but was not: ${l.toString}, line: ${linenum}\\n${lineDetails}" else s"Permission should have been read but there was no permission: ${l.toString}, line: ${linenum}\\n ${lineDetails}" + RuntimeAssert[Post](check, message)(null) + } + + /** + * Dispatch the loop and create new block structure for the loops body + * @param loop + * @return + */ + private def dispatchLoop(loop: Loop[Pre]): Loop[Post] = { + lazy val newBody = dereferences.collect(determineNewBlockStructure(loop.body.asInstanceOf[Block[Pre]]))._2 + val contract = dereferences.collect(dispatch(loop.contract))._2 //Any dereference in the contract should not be checked by the permission checker so putting it in its own scope + loop.rewrite(init = dispatch(loop.init), cond = dispatch(loop.cond), update = dispatch(loop.update), body = newBody, contract = contract) + } + + /** + * Dispatch the synchronized block and create new block structure for the synchronized blocks body + * @param s + * @return + */ + private def dispatchSynchronized(s: Synchronized[Pre]): Synchronized[Post] = { + lazy val newBody = dereferences.collect(determineNewBlockStructure(s.body.asInstanceOf[Block[Pre]]))._2 + s.rewrite(body = newBody) + } + + /** + * Dispatch the branch and create new block structure for the branches body + * @param branch + * @return + */ + private def dispatchBranch(branch: Branch[Pre]): Branch[Post] = { + val gatheredConditions = branch.branches.map(b => dispatch(b._1)) + val gatheredBlocks = branch.branches + .map(b => b._2) + .map { + case block: Block[Pre] => dereferences.collect(determineNewBlockStructure(block))._2 + case b => super.dispatch(b) + } + Branch[Post](gatheredConditions.zip(gatheredBlocks))(branch.o) + } + + /** + * retrieves the top dereferences from the dereferences stack and clears the buffer + * @return + */ + private def retrieveDereferences: Seq[Statement[Post]] = { + val newAssertions: Seq[Statement[Post]] = dereferences.top.map(pair => generatePermissionChecksStatements(pair._1, pair._2)).toSeq + dereferences.top.clear() + newAssertions + } + + /** + * normal method to fold the statements of a block + * @param b + * @param blockFold + * @param statement + * @param origin + * @return + */ + private def defaultStatementNewMethodStructure(b: Block[Pre], blockFold: (Seq[Block[Post]], Block[Post]), statement: Statement[Pre])(implicit origin: Origin): (Seq[Block[Post]], Block[Post]) = { + val newStatement = dispatch(statement) + if (heapChange) { + heapChange = false + (blockFold._1 :+ Block[Post](retrieveDereferences ++ blockFold._2.statements) :+ Block[Post](Seq(newStatement)), Block[Post](Nil)) + } else { + (blockFold._1, Block[Post](blockFold._2.statements :+ newStatement)) + } + } + + /** + * Wrapper method to also fold the statements of other block types, like loops, branches and synchronized blocks + * @param preBlock + * @param blockFold + * @param statement + * @param dispatchFunc + * @param origin + * @tparam T + * @return + */ + private def dispatchStatementWrapper[T[Pre] <: Statement[Pre]](preBlock: Block[Pre], blockFold: (Seq[Block[Post]], Block[Post]), statement: T[Pre], dispatchFunc: T[Pre] => T[Post])(implicit origin: Origin): (Seq[Block[Post]], Block[Post]) = { + val newStat = dispatchFunc(statement) + (blockFold._1 :+ Block[Post](retrieveDereferences ++ blockFold._2.statements :+ newStat), Block[Post](Nil)) + } + + /** + * Method that transforms a block to a new block structure and uses the defaultStatementNewMethodStructure to fold the statements + * If it is not a default statement it will use the dispatchStatementWrapper to fold the statements + * @param b + * @return + */ + private def determineNewBlockStructure(b: Block[Pre]): Block[Post] = { + implicit val origin: Origin = b.o + dereferences.collect { + val newBlocks = b.statements.foldLeft((Seq.empty[Block[Post]], Block[Post](Nil))) { + case (blockFold, branch: Branch[Pre]) => dispatchStatementWrapper(b, blockFold, branch, dispatchBranch) + case (blockFold, loop: Loop[Pre]) => dispatchStatementWrapper(b, blockFold, loop, dispatchLoop) + case (blockFold, sync: Synchronized[Pre]) => dispatchStatementWrapper(b, blockFold, sync, dispatchSynchronized) + case (blockFold, statement) => defaultStatementNewMethodStructure(b, blockFold, statement) + } + heapChange = false + val finalBlock: Block[Post] = Block[Post](retrieveDereferences ++ newBlocks._2.statements) + Block[Post](newBlocks._1 :+ finalBlock) + }._2 + } +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/runtime/CreateLedger.scala b/src/rewrite/vct/rewrite/runtime/CreateLedger.scala new file mode 100644 index 0000000000..d00ace05bf --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/CreateLedger.scala @@ -0,0 +1,385 @@ +package vct.rewrite.runtime + +import vct.col.ast.RewriteHelpers._ +import vct.col.ast._ +import vct.col.origin.{DiagnosticOrigin, Origin} +import vct.col.ref.LazyRef +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} +import vct.col.util.AstBuildHelpers._ +import vct.rewrite.runtime.util.LedgerHelper.{LedgerMethodBuilderHelper, DataMethodBuilderHelper} + +object CreateLedger extends RewriterBuilder { + override def key: String = "createLedger" + + override def desc: String = "Create Ledger to store permissions in" + +} + + +case class CreateLedger[Pre <: Generation]() extends Rewriter[Pre] { + + var newLedgerClass: Class[Post] = _ + + def getLedgerNewClass: Class[Post] = newLedgerClass + + var newDataClass: Class[Post] = _ + + def getDataNewClass: Class[Post] = newDataClass + + override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] = { + lazy val declarations = globalDeclarations.dispatch(program.declarations) + lazy val predicateClass = globalDeclarations.collectScoped(createPredicateObject)._1 + lazy val ledgerClass = globalDeclarations.collectScoped(createLedger)._1 + val test = program.rewrite(declarations = predicateClass ++ ledgerClass ++ declarations) + test + } + + /* + class PredicateObject{ + ... + } + */ + def createPredicateObject: Class[Post] = { + implicit val classOrigin: Origin = Origin(Nil).where(name = "DataObject").addDataObjectClass() + val newDeclarations = classDeclarations.collect { + val creatorMethods: Seq[DataMethodBuilderHelper[Post] => Unit] = Seq(createPredicateDataInstanceField, createSetData, createPredicateObject, createPredicateEquals, createPredicateHashCode) + creatorMethods.map(m => m(DataMethodBuilderHelper[Post](new LazyRef[Post, Class[Post]](getDataNewClass), classDeclarations.freezeBuffer))) + }._1 + newDataClass = new Class[Post](Nil, newDeclarations, Seq.empty, tt) + globalDeclarations.declare(newDataClass) + } + + def createPredicateDataInstanceField(mbh: DataMethodBuilderHelper[Post]): Unit = { + val newInstanceField: InstanceField[Post] = new InstanceField[Post]( + TArray(TAnyClass()), + Nil + )(DiagnosticOrigin.where(name = "data").addDataObjectClass()) + classDeclarations.declare(newInstanceField) + } + + def createSetData(mbh: DataMethodBuilderHelper[Post]): Unit = { + implicit val o: Origin = DiagnosticOrigin.addDataObjectClass() + val input = new Variable[Post](TArray[Post](TAnyClass[Post]()))(o.where(name = "data")) + val assign = Assign[Post](Deref[Post](ThisObject[Post](mbh.refCls), mbh.dataField.get.ref)(null), input.get)(null) + val body = Scope[Post](Nil, Block[Post](Seq(assign))) + classDeclarations.declare(mbh.createMethod(TVoid(), Seq(input), Some(body), "setData", false)) + } + + def createPredicateObject(mbh: DataMethodBuilderHelper[Post]): Unit = { + implicit val o: Origin = DiagnosticOrigin.addDataObjectClass() + val input = new Variable[Post](TArray[Post](TAnyClass[Post]()))(o.where(name = "data")) + val newObject = new Variable[Post](TClass[Post](mbh.refCls, Nil))(o.where(name = "object")) + val assign = Assign[Post](newObject.get, NewObject(mbh.refCls))(null) + val miSetData = Eval[Post](mbh.miSetData(newObject.get, input.get).get) + val returnObject = Return[Post](newObject.get) + val body = Scope[Post](Seq(newObject), Block[Post](Seq(assign, miSetData, returnObject))) + classDeclarations.declare(mbh.createMethod(TClass[Post](mbh.refCls, Nil), Seq(input), Some(body), "create")) + } + + def createPredicateEquals(mbh: DataMethodBuilderHelper[Post]): Unit = { + implicit val o: Origin = DiagnosticOrigin.addDataObjectClass() + val input = new Variable[Post](TAnyClass[Post]())(o.where(name = "obj")) + val otherObject = new Variable[Post](TClass[Post](mbh.refCls, Nil))(o.where(name = "otherObject")) + val checkOne = Branch[Post](Seq((ThisObject[Post](mbh.refCls) === input.get, Return[Post](tt)))) + val checkTwo = Branch[Post](Seq((input.get === Null[Post]() || (GetClassCall[Post](None) !== GetClassCall[Post](Some(input.get))), Return[Post](ff)))) + val cast = Assign[Post](otherObject.get, Cast[Post](input.get, StaticClassRef[Post](mbh.refCls)))(null) + + val ownDeref = Deref[Post](ThisObject[Post](mbh.refCls), mbh.dataField.get.ref)(null) + val otherDeref = Deref[Post](otherObject.get, mbh.dataField.get.ref)(null) + val returnStat = Return[Post](ArraysEquals[Post](ownDeref, otherDeref)) + val body = Scope[Post](Seq(otherObject), Block[Post](Seq(checkOne, checkTwo, cast, returnStat))) + classDeclarations.declare(mbh.createMethod(TBool[Post](), Seq(input), Some(body), "equals", false)) + } + + def createPredicateHashCode(mbh: DataMethodBuilderHelper[Post]): Unit = { + implicit val o: Origin = DiagnosticOrigin.addDataObjectClass() + val ownDeref = Deref[Post](ThisObject[Post](mbh.refCls), mbh.dataField.get.ref)(null) + val returnStat = Return[Post](ArraysHashCode[Post](ownDeref)) + val body = Scope[Post](Nil, Block[Post](Seq(returnStat))) + classDeclarations.declare(mbh.createMethod(TInt[Post](), Nil, Some(body), "hashCode", false)) + } + + /* + class Ledger { + ... + } + */ + def createLedger: Class[Post] = { + implicit val classOrigin: Origin = Origin(Seq.empty).addLedgerClass().where(name = "LedgerRuntime") + val newDeclarations: Seq[ClassDeclaration[Post]] = classDeclarations.collect { + val creatorMethods: Seq[LedgerMethodBuilderHelper[Post] => Unit] = Seq(createObjectLedger, createJoinTokensLedger, createPredicateLedger, createHashMapMethod, createGetPermission, createGetJoinToken, createSetJoinToken, createSetPermission, createInitiatePermissionWithSize, createInitiatePermission, createHasPredicateCheck,createFoldPredicate ,createUnfoldPredicate, createCheckForInjectivity) + creatorMethods.map(m => m(LedgerMethodBuilderHelper[Post](new LazyRef[Post, Class[Post]](getLedgerNewClass), classDeclarations.freezeBuffer, DataMethodBuilderHelper[Post](new LazyRef[Post, Class[Post]](getDataNewClass), getDataNewClass.decls)))) + }._1 + newLedgerClass = new Class[Post](Nil, newDeclarations, Seq.empty, tt) + globalDeclarations.declare(newLedgerClass) + } + + /* + public static ConcurrentHashMap> __runtime__ = new ConcurrentHashMap>(); + */ + def createObjectLedger(mbh: LedgerMethodBuilderHelper[Post]): Unit = { + val fieldFlags: Seq[FieldFlag[Post]] = Seq(Static[Post]()(DiagnosticOrigin)) + val newInstanceField: InstanceField[Post] = new InstanceField[Post]( + mbh.ledgerProperties.outerHM, + fieldFlags, + Some(mbh.ledgerProperties.newOuterMap) + )(DiagnosticOrigin.where(name = "__runtime__")) + classDeclarations.declare(newInstanceField) + } + + /* + public static ConcurrentHashMap __join_tokens__ = new ConcurrentHashMap(); + */ + def createJoinTokensLedger(mbh: LedgerMethodBuilderHelper[Post]): Unit = { + val fieldFlags: Seq[FieldFlag[Post]] = Seq(Static[Post]()(DiagnosticOrigin)) + val newInstanceField: InstanceField[Post] = new InstanceField[Post]( + mbh.ledgerJoinTokensProperites.outerHM, + fieldFlags, + Some(mbh.ledgerJoinTokensProperites.newOuterMap) + )(DiagnosticOrigin.where(name = "__join_tokens__")) + classDeclarations.declare(newInstanceField) + } + + /* + public static ConcurrentHashMap> __predicate_store__ = new ConcurrentHashMap>(); + */ + def createPredicateLedger(mbh: LedgerMethodBuilderHelper[Post]): Unit = { + val fieldFlags: Seq[FieldFlag[Post]] = Seq(Static[Post]()(DiagnosticOrigin)) + val newInstanceField: InstanceField[Post] = new InstanceField[Post]( + mbh.ledgerPredicateStore.outerHM, + fieldFlags, + Some(mbh.ledgerPredicateStore.newOuterMap) + )(DiagnosticOrigin.where(name = "__predicate_store__")) + classDeclarations.declare(newInstanceField) + } + + /* + public static void createHashMap() { + if (!__runtime__.containsKey(Thread.currentThread().getId())) { + __runtime__.put(Thread.currentThread().getId(), new ConcurrentHashMap()); + } + + if(!__predicate_store__.containsKey(Thread.currentThread().get())){ + __predicate_store__.put(Thread.currentThread().get(), new CopyOnWriteArrayList()); + } + } + */ + def createHashMapMethod(mbh: LedgerMethodBuilderHelper[Post]): Unit = { + implicit val o: Origin = DiagnosticOrigin + val containsKey: Expr[Post] = mbh.ledgerProperties.containsKey(mbh.threadId) + val putNewMap: Expr[Post] = mbh.ledgerProperties.put(mbh.threadId, mbh.ledgerProperties.newInner) + val keyBranch: Branch[Post] = Branch[Post](Seq((!containsKey, Eval[Post](putNewMap)))) + + val predContainsKey: Expr[Post] = mbh.ledgerPredicateStore.containsKey(mbh.threadId) + val predPutNewMap: Expr[Post] = mbh.ledgerPredicateStore.put(mbh.threadId, mbh.ledgerPredicateStore.newInner) + val predKeyBranch: Branch[Post] = Branch[Post](Seq((!predContainsKey, Eval[Post](predPutNewMap)))) + + val newBlock: Block[Post] = Block[Post](Seq(keyBranch, predKeyBranch)) + val body = Scope[Post](Seq.empty, newBlock) + classDeclarations.declare(mbh.createMethod(TVoid(), Nil, Some(body), "createHashMap")) + } + + /* + public static Double getPermission(Object input) { + createHashMap(); + return __runtime__.get(Thread.currentThread().getId()).getOrDefault(input, 0.0); + } + */ + def createGetPermission(mbh: LedgerMethodBuilderHelper[Post]): Unit = { + implicit val o: Origin = DiagnosticOrigin + val chm: Eval[Post] = Eval[Post](mbh.miCreateHashMaps.get) + val input = new Variable[Post](TAnyClass[Post]())(o.where(name = "input")) + val returnStat = Return[Post](mbh.ledgerProperties.getOrDefault(mbh.ledgerProperties.get(mbh.threadId), input.get, RuntimeFractionZero[Post]())) + val newBlock: Block[Post] = Block[Post](Seq(chm, returnStat)) + val body = Scope[Post](Nil, newBlock) + classDeclarations.declare(mbh.createMethod(TRuntimeFraction[Post](), Seq(input), Some(body), "getPermission")) + } + + /* + public static Fraction getPermission(Object input) { + __runtime__.get(Thread.currentThread().getId()).put(input, value); + } + */ + def createGetJoinToken(mbh: LedgerMethodBuilderHelper[Post]): Unit = { + implicit val o: Origin = DiagnosticOrigin + val input = new Variable[Post](TAnyClass[Post]())(o.where(name = "input")) + val returnStat = Return[Post](mbh.ledgerJoinTokensProperites.get(input.get)) + val newBlock: Block[Post] = Block[Post](Seq(returnStat)) + val body = Scope[Post](Nil, newBlock) + classDeclarations.declare(mbh.createMethod(TRuntimeFraction[Post](), Seq(input), Some(body), "getJoinToken")) + } + + + /* + public static void setPermission(Object input, Fraction value) { + assert (value >= 0 && value <= 1) : "value is not between bounds 0 and 1: " + value; + __runtime__.get(Thread.currentThread().getId()).put(input, value); + } + */ + def createSetJoinToken(mbh: LedgerMethodBuilderHelper[Post]): Unit = { + implicit val o: Origin = DiagnosticOrigin + val inputParam: Variable[Post] = new Variable[Post](TAnyClass[Post]())(o.where(name = "input")) + val valueParam: Variable[Post] = new Variable[Post](TRuntimeFraction[Post]())(o.where(name = "value")) + val newAssert: RuntimeAssert[Post] = RuntimeAssert[Post]((valueParam.get r_<=> RuntimeFractionZero[Post]()) !== const(-1), "Join token cannot be below 0")(null) + val putPermission: Eval[Post] = Eval[Post](mbh.ledgerJoinTokensProperites.put(inputParam.get, valueParam.get)) + val newBlock: Block[Post] = Block[Post](Seq(newAssert, putPermission)) + val body = Scope[Post](Nil, newBlock) + classDeclarations.declare(mbh.createMethod(TVoid(), Seq(inputParam, valueParam), Some(body), "setJoinToken")) + } + + /* + public static void setPermission(Object input, Double value) { + assert (value >= 0 && value <= 1) : "value is not between bounds 0 and 1: " + value; + createHashMap(); + __runtime__.get(Thread.currentThread().getId()).put(input, value); + } + */ + def createSetPermission(mbh: LedgerMethodBuilderHelper[Post]): Unit = { + implicit val o: Origin = DiagnosticOrigin + val inputParam: Variable[Post] = new Variable[Post](TAnyClass[Post]())(o.where(name = "input")) + val valueParam: Variable[Post] = new Variable[Post](TRuntimeFraction[Post]())(o.where(name = "value")) + val newAssertLowerBound: RuntimeAssert[Post] = RuntimeAssert[Post]((valueParam.get r_<=> RuntimeFractionZero[Post]()) !== const(-1), "Permission cannot be below 0")(null) + val newAssertUpperBound: RuntimeAssert[Post] = RuntimeAssert[Post]((valueParam.get r_<=> RuntimeFractionOne[Post]()) !== const(1), "Permisison cannot exceed 1")(null) + + // val newAssert: RuntimeAssert[Post] = RuntimeAssert[Post](valueParam.get >= RuntimeFractionZero[Post]() && valueParam.get <= RuntimeFractionOne[Post](), "\"value is not between bounds 0 and 1\"")(null) + val chm: Eval[Post] = Eval[Post](mbh.miCreateHashMaps.get) + val putPermission: Eval[Post] = Eval[Post](mbh.ledgerProperties.put(mbh.ledgerProperties.get(mbh.threadId), inputParam.get, valueParam.get)) + val newBlock: Block[Post] = Block[Post](Seq(newAssertLowerBound, newAssertUpperBound, chm, putPermission)) + val body = Scope[Post](Nil, newBlock) + classDeclarations.declare(mbh.createMethod(TVoid(), Seq(inputParam, valueParam), Some(body), "setPermission")) + } + + /* + public static void initiatePermission(Object input, int size) { + createHashMap(); + setPermission(input, 1.0); + __array_locations.put(input, new ConcurrentHashMap<>()); + for (int i = 0; i < size; i++) { + Object[] permLoc = {input, i}; + __array_locations.get(input).put(i, permLoc); + setPermission(permLoc, 1.0); + } + } + */ + def createInitiatePermissionWithSize(mbh: LedgerMethodBuilderHelper[Post]): Unit = { + implicit val o: Origin = DiagnosticOrigin + val inputParam: Variable[Post] = new Variable[Post](TAnyClass[Post]())(o.where(name = "input")) + val sizeParam: Variable[Post] = new Variable[Post](TInt[Post]())(o.where(name = "size")) + val setPermissionOuter = Eval[Post](mbh.miSetPermission(inputParam.get, RuntimeFractionOne[Post]()).get) + + //Loop statements: + val i: Variable[Post] = new Variable[Post](TInt[Post]())(o.where(name = "i")) + val newDataObject: MethodInvocation[Post] = mbh.pmbh.miCreate( + CreateObjectArray[Post](Seq(inputParam.get, i.get))).get + + val setPermission = Eval[Post](mbh.miSetPermission(newDataObject, RuntimeFractionOne[Post]()).get) + val newLoop = Loop[Post]( + Assign[Post](i.get, const(0))(null), + i.get < sizeParam.get, + Assign[Post](i.get, i.get + const(1))(null), + LoopInvariant[Post](tt, None)(null), + Block[Post](Seq(setPermission)) + ) + val newBlock: Block[Post] = Block[Post](Seq(setPermissionOuter, newLoop)) + val body = Scope[Post](Seq(i), newBlock) + classDeclarations.declare(mbh.createMethod(TVoid(), Seq(inputParam, sizeParam), Some(body), "initiatePermission")) + } + + /* + public static void initiatePermission(Object input) { + createHashMap(); + setPermission(input, 1.0); + if (input.getClass().isArray()) { + initiatePermission(input, Array.getLength(input)); + } + } + */ + def createInitiatePermission(mbh: LedgerMethodBuilderHelper[Post]): Unit = { + implicit val o: Origin = DiagnosticOrigin + val inputParam: Variable[Post] = new Variable[Post](TAnyClass[Post]())(o.where(name = "input")) + val miInitiate = Eval[Post](mbh.miInitiatePermission(inputParam.get, const(0)).get) + val body = Scope[Post](Nil, Block[Post](Seq(miInitiate))) + classDeclarations.declare(mbh.createMethod(TVoid(), Seq(inputParam), Some(body), "initiatePermission")) + } + + + /* + static void hasPredicateCheck(Object[] input) { + assert(LedgerRuntime.__predicate_store__.get(Thread.currentThread().getId()).contains(PredicateObject.create(input))); + } + */ + + def createHasPredicateCheck(mbh: LedgerMethodBuilderHelper[Post]): Unit = { + implicit val o: Origin = DiagnosticOrigin + val inputParam: Variable[Post] = new Variable[Post](TArray(TAnyClass[Post]()))(o.where(name = "input")) + val newAssert: RuntimeAssert[Post] = RuntimeAssert[Post]( + CopyOnWriteArrayListContains[Post](mbh.ledgerPredicateStore.get(mbh.threadId), mbh.pmbh.miCreate(inputParam.get).get), "Thread does not own the predicate")(null) + val newBlock: Block[Post] = Block[Post](Seq(newAssert)) + val body = Scope[Post](Nil, newBlock) + classDeclarations.declare(mbh.createMethod(TVoid(), Seq(inputParam), Some(body), "hasPredicateCheck")) + } + + /* + static void foldPredicate(Object[] input) { + LedgerRuntime.createHashMap(); + LedgerRuntime.__predicate_store__.get(Thread.currentThread().getId()).add(PredicateObject.create(input)); + } + */ + def createFoldPredicate(mbh: LedgerMethodBuilderHelper[Post]): Unit = { + implicit val o: Origin = DiagnosticOrigin + val inputParam: Variable[Post] = new Variable[Post](TArray(TAnyClass[Post]()))(o.where(name = "input")) + val chm: Eval[Post] = Eval[Post](mbh.miCreateHashMaps.get) + val addPred = Eval[Post](CopyOnWriteArrayListAdd[Post]( + mbh.ledgerPredicateStore.get(mbh.threadId), + mbh.pmbh.miCreate(inputParam.get).get + )) + val newBlock: Block[Post] = Block[Post](Seq(chm, addPred)) + val body = Scope[Post](Nil, newBlock) + classDeclarations.declare(mbh.createMethod(TVoid(), Seq(inputParam), Some(body), "foldPredicate")) + } + + /* + static void unFoldPredicate(Object[] input) { + LedgerRuntime.createHashMap(); + LedgerRuntime.hasPredicateCheck(input); + LedgerRuntime.__predicate_store__.get(Thread.currentThread().getId()).remove(PredicateObject.create(input)); + } + */ + def createUnfoldPredicate(mbh: LedgerMethodBuilderHelper[Post]): Unit = { + implicit val o: Origin = DiagnosticOrigin + val inputParam: Variable[Post] = new Variable[Post](TArray(TAnyClass[Post]()))(o.where(name = "input")) + val chm: Eval[Post] = Eval[Post](mbh.miCreateHashMaps.get) + val checkCall: Eval[Post] = Eval[Post](mbh.miHasPredicateCheck(inputParam.get).get) + val removePred = Eval[Post](CopyOnWriteArrayListRemove[Post]( + mbh.ledgerPredicateStore.get(mbh.threadId), + mbh.pmbh.miCreate(inputParam.get).get + )) + val newBlock: Block[Post] = Block[Post](Seq(chm, checkCall, removePred)) + val body = Scope[Post](Nil, newBlock) + classDeclarations.declare(mbh.createMethod(TVoid(), Seq(inputParam), Some(body), "unfoldPredicate")) + } + + + def createCheckForInjectivity(mbh: LedgerMethodBuilderHelper[Post]): Unit = { + implicit val o: Origin = DiagnosticOrigin + val map: Variable[Post] = mbh.createNewInjectivityMap + val key: Variable[Post] = new Variable[Post](TAnyClass[Post]())(o.where(name = "key")) + val valueLeft: Expr[Post] = mbh.injectivityMap.get(map.get, key.get) + val valueRight: Expr[Post] = mbh.miGetPermission(key.get).get + val assertCheck: RuntimeAssert[Post] = RuntimeAssert[Post]( + (valueLeft r_<=> valueRight) !== const(1), + "Permission cannot exceed 1 due to injectivity")(null) + + val newLoop: EnhancedLoop[Post] = EnhancedLoop[Post]( + key, + mbh.injectivityMap.keySet(map.get), + Block[Post](Seq(assertCheck)) + ) + val newBlock: Block[Post] = Block[Post](Seq(newLoop)) + val body = Scope[Post](Nil, newBlock) + classDeclarations.declare(mbh.createMethod(TVoid(), Seq(map), Some(body), "checkForInjectivity")) + + } + + +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/runtime/CreateLocking.scala b/src/rewrite/vct/rewrite/runtime/CreateLocking.scala new file mode 100644 index 0000000000..c255b82a7e --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/CreateLocking.scala @@ -0,0 +1,110 @@ +package vct.rewrite.runtime + +import hre.util.ScopedStack +import vct.col.ast.RewriteHelpers._ +import vct.col.ast._ +import vct.col.origin.Origin +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} +import vct.col.util.AstBuildHelpers.tt +import vct.rewrite.runtime.util.LedgerHelper.{LedgerMethodBuilderHelper, LedgerRewriter} +import vct.rewrite.runtime.util.Util.findClosestInjectivityMap +import vct.rewrite.runtime.util.{RewriteContractExpr, TransferPermissionRewriter} +import vct.rewrite.runtime.util.permissionTransfer.PermissionData + +object CreateLocking extends RewriterBuilder { + override def key: String = "createLocking" + + override def desc: String = "Creates locking for the constructor and synchronized key word" +} + + +case class CreateLocking[Pre <: Generation]() extends Rewriter[Pre] { + + val currentClass: ScopedStack[Class[Pre]] = new ScopedStack() + + implicit var program: Program[Pre] = _ + implicit var ledger: LedgerMethodBuilderHelper[Post] = _ + + /** + * Dispatch of the program for debugging and using the program everywhere to look up specific instancefields + * + * @param program Program node + * @return The rewritten program + */ + override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] = { + this.program = program + lazy val newDecl: Seq[GlobalDeclaration[Post]] = globalDeclarations.collect { + val (ledgerHelper, _, otherDeclarations) = LedgerRewriter[Pre](this).rewriteLedger(program) + ledger = ledgerHelper + otherDeclarations.foreach(dispatch) + }._1 + program.rewrite(declarations = newDecl) + } + + /** + * Transform the constructor to remove the permissions of the lock invariant + * @param decl + */ + override def dispatch(decl: Declaration[Pre]): Unit = { + decl match { + case jc: JavaConstructor[Pre] => dispatchJC(jc) + case cls: Class[Pre] => currentClass.having(cls) {super.dispatch(cls)} + case _ => super.dispatch(decl) + } + } + + /** + * Change the constructor to remove the permissions of the lock invariant + * @param jc + */ + private def dispatchJC(jc: JavaConstructor[Pre]) : Unit = { + implicit val origin: Origin = jc.o + val pd: PermissionData[Pre] = PermissionData[Pre]().setOuter(this).setCls(currentClass.top).setLedger(ledger) + val removePermissions: Block[Post] = TransferPermissionRewriter[Pre](pd).removePermissions(currentClass.top.intrinsicLockInvariant) + val newBody = Block[Post](Seq(dispatch(jc.body), removePermissions)) + classDeclarations.succeed(jc, jc.rewrite(body = newBody)) + } + + /** + * Dispatch the synchronized statement to add and remove the permissions of the lock invariant inside the synchronized statement + * @param stat + * @return + */ + override def dispatch(stat: Statement[Pre]): Statement[Post] = { + stat match { + case s: Synchronized[Pre] => dispatchSynchronized(s) + case _ => super.dispatch(stat) + } + } + + /** + * Transforms the synchronized block to transfer the permissions of the lock invariant + * At the end of the block the permissions are removed and the lock invariant is checked + * @param s + * @return + */ + private def dispatchSynchronized(s: Synchronized[Pre]): Synchronized[Post] = { + implicit val origin: Origin = s.o + val injectivityMap = findClosestInjectivityMap(variables.freeze) + val lockInvariant: Expr[Pre] = s.obj.t.asInstanceOf[TClass[Pre]].cls.decl.intrinsicLockInvariant + val pd: PermissionData[Pre] = PermissionData[Pre]().setOuter(this).setCls(currentClass.top).setLedger(ledger).setInjectivityMap(injectivityMap).setOffset(dispatch(s.obj)) + val transferrer = TransferPermissionRewriter[Pre](pd) + val addPermissions: Block[Post] = transferrer.addPermissions(lockInvariant) + val check: Statement[Post] = RewriteContractExpr[Pre](pd).createAssertions(lockInvariant) + val removePermissions: Block[Post] = transferrer.removePermissions(lockInvariant) + val newBody = Block[Post](Seq(addPermissions, dispatch(s.body), check, removePermissions)) + s.rewrite(body = newBody) + } + + /** + * Dispatch committed expression to be changed to true + * @param lc + * @return + */ + override def dispatch(e: Expr[Pre]): Expr[Rewritten[Pre]] = { + e match { + case c: Committed[Pre] => tt[Post] + case _ => super.dispatch(e) + } + } +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/runtime/CreateLoopInvariants.scala b/src/rewrite/vct/rewrite/runtime/CreateLoopInvariants.scala new file mode 100644 index 0000000000..83ae42e36f --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/CreateLoopInvariants.scala @@ -0,0 +1,94 @@ +package vct.rewrite.runtime + +import hre.util.ScopedStack +import vct.col.ast.RewriteHelpers._ +import vct.col.ast._ +import vct.col.origin.Origin +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} +import vct.col.util.AstBuildHelpers.tt +import vct.rewrite.runtime.util.LedgerHelper._ +import vct.rewrite.runtime.util.RewriteContractExpr +import vct.rewrite.runtime.util.Util.findClosestInjectivityMap +import vct.rewrite.runtime.util.permissionTransfer.PermissionData + +object CreateLoopInvariants extends RewriterBuilder { + override def key: String = "createLoopInvariants" + + override def desc: String = "Create loop invariant statements" +} + + +case class CreateLoopInvariants[Pre <: Generation]() extends Rewriter[Pre] { + + + implicit var program: Program[Pre] = _ + implicit var ledger: LedgerMethodBuilderHelper[Post] = _ + val currentClass: ScopedStack[Class[Pre]] = new ScopedStack() + val loopContract: ScopedStack[() => Statement[Post]] = new ScopedStack() + + + + override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] = { + this.program = program + lazy val newDecl: Seq[GlobalDeclaration[Post]] = globalDeclarations.collect { + val (ledgerHelper, _, otherDeclarations) = LedgerRewriter[Pre](this).rewriteLedger(program) + ledger = ledgerHelper + otherDeclarations.foreach(dispatch) + }._1 + program.rewrite(declarations = newDecl) + } + + /** + * Dispatches the class declaration to keep track of the current class during the transformation + * @param decl + */ + override def dispatch(decl: Declaration[Pre]): Unit = { + decl match { + case cls: Class[Pre] => currentClass.having(cls) { + super.dispatch(cls) + } + case _ => super.dispatch(decl) + } + } + + /** + * dispatched the loop contract to create the loop invariant + * @param lc + * @return + */ + def dispatchLoopContract(lc: LoopContract[Pre]): Statement[Post] = { + val injectivityMap = findClosestInjectivityMap(variables.freeze) + val pd: PermissionData[Pre] = PermissionData().setOuter(this).setCls(currentClass.top).setLedger(ledger).setInjectivityMap(injectivityMap) + RewriteContractExpr[Pre](pd).createAssertions(lc.asInstanceOf[LoopInvariant[Pre]].invariant) + } + + /** + * Dispatches the loop to create the loop invariant + * by storing the function of the loop contract in the stack, other methods can make use of the same function with the correct + * paramaters + * @param l + * @return + */ + def dispatchLoop(l: Loop[Pre]): Statement[Post] = { + implicit val o: Origin = l.o + loopContract.having(() => dispatchLoopContract(l.contract)) { + val newBody = Block[Post](Seq(loopContract.top(), dispatch(l.body), loopContract.top())) + l.rewrite(body = newBody, contract = LoopInvariant[Post](tt[Post], None)(null)) + } + } + + /** + * Dispatches the statement, if the loop iteration will stop also check the loop contract again + * @param stat + * @return + */ + override def dispatch(stat: Statement[Pre]): Statement[Rewritten[Pre]] = { + stat match { + case l: Loop[Pre] => dispatchLoop(l) +// case r@(_:Return[Pre] | _:Continue[Pre] | _:Break[Pre] ) if loopContract.nonEmpty => Block[Post](Seq(loopContract.top(), super.dispatch(stat)))(r.o) + case r@(_:Continue[Pre]) if loopContract.nonEmpty => Block[Post](Seq(loopContract.top(), super.dispatch(stat)))(r.o) + case _ => super.dispatch(stat) + } + } + +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/runtime/CreatePrePostConditions.scala b/src/rewrite/vct/rewrite/runtime/CreatePrePostConditions.scala new file mode 100644 index 0000000000..bce6d5544f --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/CreatePrePostConditions.scala @@ -0,0 +1,134 @@ +package vct.rewrite.runtime + +import hre.util.ScopedStack +import vct.col.ast.RewriteHelpers._ +import vct.col.ast._ +import vct.col.origin.Origin +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} +import vct.rewrite.runtime.util.LedgerHelper._ +import vct.rewrite.runtime.util.RewriteContractExpr +import vct.rewrite.runtime.util.permissionTransfer.PermissionData + +import scala.collection.mutable +import scala.collection.mutable.ArrayBuffer + + +object CreatePrePostConditions extends RewriterBuilder { + override def key: String = "CreatePrePostConditions" + + override def desc: String = "Create permissions for the pre and post conditions of the methods" +} + + +case class CreatePrePostConditions[Pre <: Generation]() extends Rewriter[Pre] { + + + val givenStatementBuffer: mutable.Buffer[Statement[Rewritten[Pre]]] = new ArrayBuffer() + val currentClass: ScopedStack[Class[Pre]] = new ScopedStack() + val currentContract: ScopedStack[AccountedPredicate[Pre]] = new ScopedStack() + val postConditions: ScopedStack[() => Statement[Post]] = new ScopedStack() + + + val injectivityMap: ScopedStack[Variable[Post]] = new ScopedStack(); + + implicit var program: Program[Pre] = null + implicit var ledger: LedgerMethodBuilderHelper[Post] = _ + + + override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] = { + this.program = program + lazy val newDecl: Seq[GlobalDeclaration[Post]] = globalDeclarations.collect { + val (ledgerHelper, _, otherDeclarations) = LedgerRewriter[Pre](this).rewriteLedger(program) + ledger = ledgerHelper + otherDeclarations.foreach(dispatch) + }._1 + program.rewrite(declarations = newDecl) + } + + override def dispatch(decl: Declaration[Pre]): Unit = { + decl match { + case im: InstanceMethod[Pre] => dispatchInstanceMethod(im) + case cls: Class[Pre] => currentClass.having(cls) { + globalDeclarations.succeed(cls, cls.rewrite()) + } + case _ => super.dispatch(decl) + } + } + + /** + * Dispatches the instance method and creates a new injectivity map for the method + * @param im + */ + def dispatchInstanceMethod(im: InstanceMethod[Pre]): Unit = { + im.body match { + case Some(sc: Scope[Pre]) => sc.body match { + case block: Block[Pre] => { + injectivityMap.having(ledger.createNewInjectivityMap){ + val (newVariables, newBody) = variables.collectScoped{ + sc.locals.foreach(dispatch) + variables.declare(injectivityMap.top) + dispatchMethodBlock(block, im) + } + classDeclarations.succeed(im, im.rewrite(body = Some(sc.rewrite(locals = newVariables, body = newBody)))) + } + } + case _ => ??? + } + case _ => super.dispatch(im) + } + } + + /** + * Collects the pre and postcondtions + * It store te postConditions in a function so that it can be called later and thus the postconditions can be generated later on as well + * @param block + * @param im + * @return + */ + def dispatchMethodBlock(block: Block[Pre], im: InstanceMethod[Pre]): Block[Post] = { + implicit val origin: Origin = block.o + val preConditionStatements: Statement[Post] = dispatchApplicableContractToAssert(im.contract.requires) + postConditions.having(() => dispatchApplicableContractToAssert(im.contract.ensures)){ + val originalStatements: Seq[Statement[Post]] = block.statements.map(dispatch) + val lastStatement: Option[Statement[Pre]] = block.statements.lastOption + lastStatement match { + case Some(_: Return[Pre]) => Block[Post](preConditionStatements +: originalStatements) + case _ => Block[Post](preConditionStatements +: originalStatements :+ postConditions.top())(block.o) + } + } + } + + /** + * Changes a contract to assert statements + * @param ap + * @return + */ + private def dispatchApplicableContractToAssert(ap: AccountedPredicate[Pre]): Statement[Post] = { + ap match { + case uni: UnitAccountedPredicate[Pre] => { + currentContract.having(ap) { + val pd = PermissionData().setOuter(this).setCls(currentClass.top).setLedger(ledger).setInjectivityMap(injectivityMap.top) + val stat = new RewriteContractExpr[Pre](pd)(program).createAssertions(uni.pred) + dispatch(ap) + stat + } + } + case _ => ??? + } + } + + /** + * When a return statement is found, the postconditions are added to the block + * @param stat + * @return + */ + override def dispatch(stat: Statement[Pre]): Statement[Rewritten[Pre]] = { + val dispatched = super.dispatch(stat) + stat match { + case _:Return[Pre] if postConditions.nonEmpty => Block[Post](Seq(postConditions.top(), dispatched))(stat.o) + case _ => dispatched + } + } + +} + diff --git a/src/rewrite/vct/rewrite/runtime/CreatePredicateFoldUnfold.scala b/src/rewrite/vct/rewrite/runtime/CreatePredicateFoldUnfold.scala new file mode 100644 index 0000000000..b1b0f079f6 --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/CreatePredicateFoldUnfold.scala @@ -0,0 +1,111 @@ +package vct.rewrite.runtime + +import hre.util.ScopedStack +import vct.col.ast.RewriteHelpers._ +import vct.col.ast.{Block, _} +import vct.col.origin.Origin +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} +import vct.col.util.AstBuildHelpers._ +import vct.rewrite.runtime.util.LedgerHelper.{LedgerMethodBuilderHelper, LedgerRewriter} +import vct.rewrite.runtime.util.Util.findClosestInjectivityMap +import vct.rewrite.runtime.util.{RewriteContractExpr, TransferPermissionRewriter} +import vct.rewrite.runtime.util.permissionTransfer.PermissionData + + +object CreatePredicateFoldUnfold extends RewriterBuilder { + override def key: String = "createPredicatesFoldUnfold" + override def desc: String = "When a fold or unfold predicate is found replace it with a method call to the correct instancePredicate class" +} + +case class CreatePredicateFoldUnfold[Pre <: Generation]() extends Rewriter[Pre] { + + implicit var program: Program[Pre] = _ + implicit var ledger: LedgerMethodBuilderHelper[Post] = _ + private val currentClass: ScopedStack[Class[Pre]] = new ScopedStack() + + + override def dispatch(decl: Declaration[Pre]): Unit = { + decl match { + case cls: Class[Pre] => currentClass.having(cls) { + super.dispatch(cls) + } + case _ => super.dispatch(decl) + } + } + + override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] = { + this.program = program + lazy val newDecl: Seq[GlobalDeclaration[Post]] = globalDeclarations.collect { + val (ledgerHelper, _, otherDeclarations) = LedgerRewriter[Pre](this).rewriteLedger(program) + ledger = ledgerHelper + otherDeclarations.foreach(dispatch) + }._1 + val test = program.rewrite(declarations = newDecl) + test + } + + /** + * Dispatches the statement and if it is a fold or unfold predicate it will call the correct method to rewrite it + * @param stat + * @return + */ + override def dispatch(stat: Statement[Pre]): Statement[Rewritten[Pre]] = { + implicit val origin: Origin = stat.o + stat match { + case Unfold(ipa@InstancePredicateApply(_, _, _, _)) => Block[Post](Seq(super.dispatch(stat), dispatchUnfold(ipa))) + case Fold(ipa@InstancePredicateApply(_, _, _, _)) => Block[Post](Seq(super.dispatch(stat), dispatchFold(ipa))) + case _ => super.dispatch(stat) + } + } + + /** + * When it is a fold method it will first check if the predicate condition is met by the thread + * After that it will remove the permissions and call the method fold of the ledger + * @param ipa + * @param origin + * @return + */ + def dispatchFold(ipa: InstancePredicateApply[Pre])(implicit origin: Origin): Statement[Rewritten[Pre]] = { + val injectivityMap = findClosestInjectivityMap(variables.freeze) + val permissionExpr = ipa.ref.decl.body + variables.collectScoped { + val newVars = variables.dispatch(ipa.ref.decl.args) + val newVarsAssignments: Seq[Statement[Post]] = newVars + .zip(ipa.args) + .map{case (v: Variable[Post], e: Expr[Pre]) => Assign[Post](v.get, dispatch(e))(null)} + val nvAssignmentsBlock = Block[Post](newVarsAssignments) + + val pd = PermissionData[Pre]().setOuter(this).setCls(currentClass.top).setLedger(ledger).setInjectivityMap(injectivityMap).setOffset(dispatch(ipa.obj)) + val predCheck: Statement[Post] = if (permissionExpr.isEmpty) Block[Post](Nil) else RewriteContractExpr(pd).createAssertions(permissionExpr.get) + val removeStatements = if (permissionExpr.isEmpty) Block[Post](Nil) else TransferPermissionRewriter(pd).removePermissions(permissionExpr.get) + + val allArgs: Seq[Expr[Pre]] = ipa.args :+ ipa.obj :+ StringValue(ipa.ref.decl.o.getPreferredNameOrElse().camel) + val dispatchedArgs: Seq[Expr[Post]] = allArgs.map(dispatch) + val newObject = CreateObjectArray[Post](dispatchedArgs) + val mi: Eval[Post] = Eval[Post](ledger.miFoldPredicate(newObject).get) + Scope[Post](newVars, Block[Post](Seq(nvAssignmentsBlock, predCheck, removeStatements, mi))) + }._2 + } + + /** + * When it is a unfold method it will first check if the predicate is hold by the thread in the ledger + * After that it will add the permissions and call the method unfold of the ledger + * @param ipa + * @param origin + * @return + */ + def dispatchUnfold(ipa: InstancePredicateApply[Pre])(implicit origin: Origin): Statement[Rewritten[Pre]] = { + val permissionExpr = ipa.ref.decl.body + val pdAdd: PermissionData[Pre] = PermissionData[Pre]().setOuter(this).setCls(currentClass.top) + .setLedger(ledger).setOffset(dispatch(ipa.obj)) + val addStatements = if(permissionExpr.isEmpty) Block[Post](Nil) else TransferPermissionRewriter(pdAdd).addPermissions(permissionExpr.get) + + + val allArgs: Seq[Expr[Pre]] = ipa.args :+ ipa.obj :+ StringValue(ipa.ref.decl.o.getPreferredNameOrElse().camel) + val dispatchedArgs: Seq[Expr[Post]] = allArgs.map(dispatch) + val newObject = CreateObjectArray[Post](dispatchedArgs) + val mi: Eval[Post] = Eval[Post](ledger.miUnfoldPredicate(newObject).get) + Block[Post](Seq(mi, addStatements)) + } + +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/runtime/ForkJoinPermissionTransfer.scala b/src/rewrite/vct/rewrite/runtime/ForkJoinPermissionTransfer.scala new file mode 100644 index 0000000000..a1264d3448 --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/ForkJoinPermissionTransfer.scala @@ -0,0 +1,145 @@ +package vct.rewrite.runtime + +import hre.util.ScopedStack +import vct.col.ast.RewriteHelpers._ +import vct.col.ast._ +import vct.col.origin.Origin +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} +import vct.col.util.AstBuildHelpers._ +import vct.result.VerificationError.Unreachable +import vct.rewrite.runtime.util.LedgerHelper._ +import vct.rewrite.runtime.util.TransferPermissionRewriter +import vct.rewrite.runtime.util.Util._ +import vct.rewrite.runtime.util.permissionTransfer.PermissionData + +import scala.collection.mutable +import scala.language.postfixOps + + +object ForkJoinPermissionTransfer extends RewriterBuilder { + override def key: String = "forkJoinPermissionTransfer" + + override def desc: String = "Detects fork/join/run methods and creates a permission transfer for the forked thread" +} + +case class ForkJoinPermissionTransfer[Pre <: Generation]() extends Rewriter[Pre] { + + implicit var program: Program[Pre] = _ + implicit var ledger: LedgerMethodBuilderHelper[Post] = _ + + private val currentClass: ScopedStack[Class[Pre]] = new ScopedStack() + private val postJoinTokens: ScopedStack[mutable.ArrayBuffer[RuntimePostJoin[Post]]] = new ScopedStack() + + override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] = { + this.program = program + lazy val newDecl: Seq[GlobalDeclaration[Post]] = globalDeclarations.collect { + val (ledgerHelper, _, otherDeclarations) = LedgerRewriter[Pre](this).rewriteLedger(program) + ledger = ledgerHelper + otherDeclarations.foreach(dispatch) + }._1 + program.rewrite(declarations = newDecl) + } + + override def dispatch(decl: Declaration[Pre]): Unit = { + decl match { + case cls: Class[Pre] => currentClass.having(cls) { + super.dispatch(cls) + } + case i: InstanceMethod[Pre] => dispatchInstanceMethod(i) + case _ => super.dispatch(decl) + } + } + + /** + * Dispatches the instance method to the method with transferring permission statements + * @param i + * @param o + */ + private def dispatchInstanceMethod(i: InstanceMethod[Pre])(implicit o: Origin = i.o): Unit = { + postJoinTokens.collect { + variables.collectScoped { + val (preStatements, postStatements): (Block[Post], Block[Post]) = collectTransferPermissionStatementsFromRunMethod(i) + val scope = collectMethodBody(i) + val scopeBlock = collectBlockScope(scope) + val newScope = scope.rewrite(body = Block[Post](Seq(preStatements, dispatch(scopeBlock), postStatements))) + classDeclarations.succeed(i, i.rewrite(body = Some(newScope))) + } + } + } + + /** + * Collects the transfer permission statements from the run method + * where the pre and post conditions will be used to add and remove permissions from the thread + * @param i + * @param o + * @return + */ + private def collectTransferPermissionStatementsFromRunMethod(i: InstanceMethod[Pre]): (Block[Post], Block[Post]) = { + implicit val o: Origin = i.o + if (!isExtendingThread(currentClass.top) || !isMethod(i, "run")) return (EMPTY, EMPTY) + val pd: PermissionData[Pre] = PermissionData[Pre]().setOuter(this).setCls(currentClass.top).setLedger(ledger) + val trans = TransferPermissionRewriter(pd) + val (prePredicate, postPredicate) = (unfoldPredicate(i.contract.requires).head, unfoldPredicate(i.contract.ensures).head) + (trans.addPermissions(prePredicate), trans.removePermissions(postPredicate)) + } + + /** + * When a post join token is found, store the token in the buffer + * When an join or start methodinvocation is found dispatch the method invocation to the also transfer permissions + * @param stat + * @return + */ + override def dispatch(stat: Statement[Pre]): Statement[Rewritten[Pre]] = { + stat match { + case rpj: RuntimePostJoin[Pre] if postJoinTokens.nonEmpty => { + val newRpj = super.dispatch(rpj) + postJoinTokens.top.addOne(newRpj.asInstanceOf[RuntimePostJoin[Post]]) + newRpj + } + case e@Eval(mi: MethodInvocation[Pre]) if isThreadMethod(mi, "join") => dispatchJoinInvocation(e, mi) + case e@Eval(mi: MethodInvocation[Pre]) if isThreadMethod(mi, "start") => dispatchStartInvocation(e, mi) + case _ => super.dispatch(stat) + } + } + + /** + * Dispatches the join method invocation to the method with adding permission statements for the joined thread + * Using the join token as a factor to remove the permissions from the thread + * @param e + * @param mi + * @param o + * @return + */ + private def dispatchJoinInvocation(e: Eval[Pre], mi: MethodInvocation[Pre])(implicit o: Origin = e.o): Statement[Rewritten[Pre]] = { + val runMethod: InstanceMethod[Pre] = getRunMethod(mi) + val predicate: Expr[Pre] = unfoldPredicate(runMethod.contract.ensures).head + val dispatchedStatement: Eval[Post] = super.dispatch(e).asInstanceOf[Eval[Post]] + val dispatchedOffset: Expr[Post] = dispatchedStatement.expr.asInstanceOf[MethodInvocation[Post]].obj + val pst = postJoinTokens.top + val postfactor: Expr[Post] = postJoinTokens.top + .find(rpj => rpj.obj == dispatchedOffset) + .get.arg + + val factor = permissionToRuntimeValue(postfactor) + val removePostJoinToken: Eval[Post] = Eval[Post](ledger.miSetJoinToken(dispatchedOffset, ledger.miGetJoinToken(dispatchedOffset).get r_- factor).get) + val pdAdd: PermissionData[Pre] = PermissionData[Pre]().setOuter(this).setCls(currentClass.top).setLedger(ledger).setOffset(dispatch(mi.obj)).setFactor(factor) + val newAddStatements = TransferPermissionRewriter(pdAdd).addPermissions(predicate) + Block[Post](Seq(dispatchedStatement, removePostJoinToken, newAddStatements)) + } + + /** + * Dispatches the start method invocation to the method with removing permission statements of the starting thread + * @param e + * @param mi + * @param o + * @return + */ + private def dispatchStartInvocation(e: Eval[Pre], mi: MethodInvocation[Pre])(implicit o: Origin = e.o): Statement[Rewritten[Pre]] = { + val runMethod: InstanceMethod[Pre] = getRunMethod(mi) + val predicate: Expr[Pre] = unfoldPredicate(runMethod.contract.requires).head + val dispatchedStatement: Eval[Post] = super.dispatch(e).asInstanceOf[Eval[Post]] + val pdRemove: PermissionData[Pre] = PermissionData[Pre]().setOuter(this).setCls(currentClass.top).setLedger(ledger).setOffset(dispatch(mi.obj)) + val removeStatements = TransferPermissionRewriter(pdRemove).removePermissions(predicate) + Block[Post](Seq(removeStatements, dispatchedStatement)) + } +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/runtime/GenerateJava.scala b/src/rewrite/vct/rewrite/runtime/GenerateJava.scala new file mode 100644 index 0000000000..1b89d60a22 --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/GenerateJava.scala @@ -0,0 +1,182 @@ +package vct.rewrite.runtime + +import vct.col.ast.RewriteHelpers._ +import vct.col.ast._ +import vct.col.origin.{DiagnosticOrigin, Origin} +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} +import vct.rewrite.runtime.util.Util._ + +object GenerateJava extends RewriterBuilder { + override def key: String = "generateJava" + + override def desc: String = "Create permissions for items in arrays" +} + + +case class GenerateJava[Pre <: Generation]() extends Rewriter[Pre] { + + /** + * Create a new namespace for the program including java imports that are required by the runtime checker + * @param program + * @return + */ + override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] = { + lazy val newNameSpace = createNewNamespace + program.rewrite(declarations = globalDeclarations.collectScoped { + newNameSpace + program.declarations.foreach(dispatch) + }._1) + } + + /** + * Create a new namespace for the program including java imports that are required by the runtime checker + * the java.util.* and the org.apache.commons.math3.fraction.Fraction classes are used by the program and thus be imported + * The namespace is set to org.example + * the namespace is declared to the globaldeclarations + * @return + */ + def createNewNamespace: JavaNamespace[Post] = { + implicit val origin: Origin = DiagnosticOrigin + val importUtil = JavaImport[Post](false, JavaName(Seq("java", "util")), true) + // val importArray = JavaImport(false, JavaName(Seq("java", "lang", "reflect", "Array")), false) + val importFraction = JavaImport[Post](false, JavaName(Seq("org", "apache", "commons", "math3", "fraction", "Fraction")), false) + val newNameSpace = new JavaNamespace[Post]( + Some(JavaName[Post](Seq("org", "example"))), + Seq(importUtil, importFraction), + Nil, + ) + globalDeclarations.declare(newNameSpace) + newNameSpace + } + + /** + * Remove all procedures from the program + * Remove all start and join methods from the program + * Transform the main method to a public static void main method + * Transform the run, equals and hashcode methods to be public methods + * @param decl + */ + override def dispatch(decl: Declaration[Pre]): Unit = { + decl match { + case p: Procedure[Pre] => p.drop() + // case im: InstanceMethod[Pre] if isMethod(im, "run") => im.rewrite(overriding = true, public = true) + case im: InstanceMethod[Pre] if isMethod(im, "start") || isMethod(im, "join") => im.drop() + case im: InstanceMethod[Pre] if isMethod(im, "main") => createMainMethod(im) + case im: InstanceMethod[Pre] if isMethod(im, "run") => makeMethodPublic(im) + case im: InstanceMethod[Pre] if isMethod(im, "equals") && im.o.getDataObjectClassRuntime.nonEmpty => makeMethodPublic(im) + case im: InstanceMethod[Pre] if isMethod(im, "hashCode") && im.o.getDataObjectClassRuntime.nonEmpty => makeMethodPublic(im) + case _ => super.dispatch(decl) + } + } + + /** + * Change the procedureInvocation to a new object node since all procedures are removed + * Change the methodInvocations to work with the JavaMethod node and thus create a JavaMethodInvocation node + * Change the local variables to be JavaLocal nodes if they do not exists yet in the variables buffer + * @param e + * @return + */ + override def dispatch(e: Expr[Pre]): Expr[Rewritten[Pre]] = { + e match { + case pe@PreAssignExpression(_, p: ProcedureInvocation[Pre]) => pe.rewrite(value = procedureInvocationToNewObject(p)) + case pe@PostAssignExpression(_, p: ProcedureInvocation[Pre]) => pe.rewrite(value = procedureInvocationToNewObject(p)) + case mi: MethodInvocation[Pre] if isThreadMethod(mi, "start") => generateThreadMethodCall(mi, "start") + case mi: MethodInvocation[Pre] if isThreadMethod(mi, "join") => generateThreadMethodCall(mi, "join") + case l: Local[Pre] if variables.freeze.computeSucc(l.ref.decl).isEmpty => JavaLocal[Post](l.ref.decl.o.getPreferredNameOrElse().camel)(null)(l.o) + // case mi: MethodInvocation[Pre] if isMethod(mi.ref.decl, "equals") => generateThreadMethodCall(mi, "join") + + case _ => super.dispatch(e) + } + } + + /** + * Create a JavaInvocation node for the methodInvocation + * @param mi + * @param name + * @return + */ + def generateThreadMethodCall(mi: MethodInvocation[Pre], name: String): JavaInvocation[Post] = { + JavaInvocation[Post]( + Some(dispatch(mi.obj)), + Nil, + name, + mi.args.map(dispatch), + Nil, + Nil + )(null)(mi.o) + } + + /** + * Converts a main method to a public static void main method (JavaMethod) + * @param im + */ + def createMainMethod(im: InstanceMethod[Pre]): Unit = { + implicit val origin: Origin = im.o + val modifiers: Seq[JavaModifier[Post]] = Seq(JavaPublic[Post](), JavaStatic()) + val returnType: Type[Post] = TVoid[Post]() + val param: Seq[JavaParam[Post]] = Seq(new JavaParam[Post](Nil, "args", TArray(TString()))) + val newBody: Option[Statement[Post]] = im.body.map(dispatch) + val contract = dispatch(im.contract) + val newMethod = new JavaMethod( + modifiers, + returnType, + 0, + "main", + param, + Nil, + Nil, + newBody, + contract + )(null) + classDeclarations.succeed(im, newMethod) + } + + /** + * Transforms an InstanceMethod to a JavaMethod that is public + * @param im + */ + def makeMethodPublic(im: InstanceMethod[Pre]): Unit = { + implicit val origin: Origin = im.o + val modifiers: Seq[JavaModifier[Post]] = Seq(JavaPublic[Post]()) + val newBody: Option[Statement[Post]] = im.body.map(dispatch) + val contract = dispatch(im.contract) + val params: Seq[JavaParam[Post]] = im.args.map(v => { + new JavaParam[Post](Nil, v.o.getPreferredNameOrElse().camel, dispatch(v.t)) + }) + val newMethod = new JavaMethod( + modifiers, + dispatch(im.returnType), + 0, + im.o.getPreferredNameOrElse().camel, + params, + Nil, + Nil, + newBody, + contract + )(null) + classDeclarations.succeed(im, newMethod) + } + + /** + * Create a new object node for the procedureInvocation since all procedures are removed + * @param p + * @return + */ + override def dispatch(node: Statement[Pre]): Statement[Post] = { + node match { + case a@Assign(_, p: ProcedureInvocation[Pre]) => a.rewrite(value = procedureInvocationToNewObject(p)) + case _ => super.dispatch(node) + } + } + + /** + * Convert the procedureInvocation to a NewObject node + * @param p + * @return + */ + private def procedureInvocationToNewObject(p: ProcedureInvocation[Pre]): NewObject[Post] = { + val classDecl: Class[Pre] = p.ref.decl.returnType.asClass.get.cls.decl + NewObject[Post](this.anySucc(classDecl))(classDecl.o) + } + +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/runtime/RefactorGeneratedCode.scala b/src/rewrite/vct/rewrite/runtime/RefactorGeneratedCode.scala new file mode 100644 index 0000000000..6c104eccda --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/RefactorGeneratedCode.scala @@ -0,0 +1,74 @@ +package vct.rewrite.runtime + +import vct.col.ast.RewriteHelpers.RewriteClass +import vct.col.ast.{Class, ClassDeclaration, Declaration, GlobalDeclaration, Procedure, Program, TClass, Type} +import vct.col.print.Text +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} +import vct.col.util.SuccessionMap +import vct.rewrite.runtime.util.CreateConstructor + +object RefactorGeneratedCode extends RewriterBuilder { + override def key: String = "refactorGeneratedCode" + + override def desc: String = "Refactors the generated code to have a constructor again and remove implements and extends" +} + + +case class RefactorGeneratedCode[Pre <: Generation]() extends Rewriter[Pre] { + + private val givenClassConstrSucc: SuccessionMap[Type[Pre], Procedure[Pre]] = SuccessionMap() + private val givenClassSucc: SuccessionMap[Type[Pre], Class[Post]] = SuccessionMap() + + + override def rewriteDefault(node: Program[Pre]): Program[Rewritten[Pre]] = { + val test = super.rewriteDefault(node) + test + } + + /** + * Searches for the constructor in the procedure and restores it into a java constructor. + * If the class is an interface do not recreate a java constructor + * @param decl + */ + override def dispatch(decl: Declaration[Pre]): Unit = { + decl match { + case p: Procedure[Pre] => { + givenClassConstrSucc.update(p.returnType, p) + rewriteDefault(p) + } + case c: Class[Pre] => + val classOrInterface = c.classOrInterfaceDoc() + classOrInterface match { + case Text("class") => globalDeclarations.succeed(c, dispatchGivenClass(c)) + case _ => + println("Detected interface no creation of constructor") + rewriteDefault(c) + } + case _ => super.rewriteDefault(decl) + } + } + + /** + * Dispatches the class to the rewriter and create the new constructor + * @param c + * @return + */ + def dispatchGivenClass(c: Class[Pre]): GlobalDeclaration[Rewritten[Pre]] = { + val rw = CreateConstructor[Pre](this, givenClassSucc) + val newClass = c.rewrite(decls = createClassDeclarations(c, rw))(rw) + givenClassSucc.update(TClass(c.ref, Nil), newClass) + newClass + } + + /** + * Create the new classDeclarations including the newly created constructor + * @param c + * @param rw + * @return + */ + def createClassDeclarations(c: Class[Pre], rw: Rewriter[Pre]): Seq[ClassDeclaration[Rewritten[Pre]]] = { + classDeclarations.collect { + (givenClassConstrSucc.get(TClass(c.ref, Nil)).get +: c.declarations).foreach(d => rw.dispatch(d)) + }._1 + } +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/runtime/RemoveSelfLoops.scala b/src/rewrite/vct/rewrite/runtime/RemoveSelfLoops.scala new file mode 100644 index 0000000000..9e8512f59c --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/RemoveSelfLoops.scala @@ -0,0 +1,68 @@ +package vct.rewrite.runtime + +import vct.col.ast.RewriteHelpers.RewriteClass +import vct.col.ast.{Class, Declaration, GlobalDeclaration, Procedure, TClass, Type} +import vct.col.origin.PreferredName +import vct.col.ref.Ref +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} + +object RemoveSelfLoops extends RewriterBuilder { + override def key: String = "removeSelfLoops" + + override def desc: String = "Removing unnecessary self loop by removing Object class and corresponding procedure" +} + + +case class RemoveSelfLoops[Pre <: Generation]() extends Rewriter[Pre] { + + + /** + * Removes the extra Object class from all classes + * @param decl + */ + override def dispatch(decl: Declaration[Pre]): Unit = { + decl match { + case p: Procedure[Pre] => { + p.returnType match { + case c: TClass[Pre] => c.cls.decl.o.getPreferredNameOrElse().ucamel match { + case "Object" => + case _ => rewriteDefault(p) + } + case _ => rewriteDefault(p) + } + } + case c: Class[Pre] => + val preferredName = c.o.getPreferredNameOrElse().ucamel + preferredName match { + case "Object" => + case _ => globalDeclarations.succeed(c, dispatchGivenClass(c)) + } + case _ => { + super.rewriteDefault(decl) + } + } + } + + /** + * Recreates classes and removes the Object class as extension + * @param c + * @return + */ + def dispatchGivenClass(c: Class[Pre]): GlobalDeclaration[Post] = { + val newClass = c.rewrite( + supports = createClassSupports(c) + ) + newClass + } + + /** + * Filters the Object class from the supports list and returns the rest + * @param c + * @return + */ + def createClassSupports(c: Class[Pre]): Seq[Type[Post]] = + c.supports.filter { + case TClass(Ref(cls), _) if cls.o.find[PreferredName].contains(PreferredName(Seq("Object"))) => false + case _ => true + }.map(dispatch) +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/runtime/util/AbstractQuantifierRewriter.scala b/src/rewrite/vct/rewrite/runtime/util/AbstractQuantifierRewriter.scala new file mode 100644 index 0000000000..035dbf00f8 --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/util/AbstractQuantifierRewriter.scala @@ -0,0 +1,158 @@ +package vct.rewrite.runtime.util + +import vct.col.ast.RewriteHelpers.{RewriteDeref, RewriteVariable} +import vct.col.ast._ +import vct.col.origin.Origin +import vct.col.rewrite.{Generation, Rewriter, Rewritten} +import vct.col.util.AstBuildHelpers._ +import vct.rewrite.runtime.util.AbstractQuantifierRewriter.LoopBodyContent +import vct.rewrite.runtime.util.permissionTransfer._ + +import scala.Int.{MaxValue, MinValue} +import scala.collection.mutable.ArrayBuffer + +object AbstractQuantifierRewriter{ + + case class LoopBodyContent[G](expr: Expr[G], quantifier: Expr[G]) +} + + +/** + * Abstract class for rewriting quantifiers + * @param pd + * @param program + * @tparam Pre + */ +abstract class AbstractQuantifierRewriter[Pre <: Generation](pd: PermissionData[Pre])(implicit program: Program[Pre]) extends Rewriter[Pre] { + override val allScopes: AllScopes[Pre, Post] = pd.outer.allScopes + + /** + * Dispatches the loop body, can be overridden by other rewriters + * @param loopBodyContent + * @param origin + * @return + */ + def dispatchLoopBody(loopBodyContent: LoopBodyContent[Pre])(implicit origin: Origin): Block[Post] = Block[Post](Seq()) + + /** + * Dispatches the quantifier expression + * @param quantifier + * @return + */ + final def dispatchQuantifier(quantifier: Expr[Pre]): Scope[Post] = { + variables.collectScoped{ + quantifier match { + case q: Starall[Pre] => dispatchQuantifier(q, q.bindings, q.body) + case q: Exists[Pre] => dispatchQuantifier(q, q.bindings, q.body) + case q: Forall[Pre] => dispatchQuantifier(q, q.bindings, q.body) + case _ => ??? + } + }._2 + } + + /** + * Dispatches the quantifier expression, with its bindings and body. + * It unfolds the body and calls the createQuantifierStatement method to create a new quantifier + * @param quantifier + * @param bindings + * @param body + * @return + */ + private final def dispatchQuantifier(quantifier: Expr[Pre], bindings: Seq[Variable[Pre]], body: Expr[Pre]): Scope[Post] = { + body match { + case imp: Implies[Pre] => createQuantifierStatement(quantifier, bindings, imp.left, imp.right) + case and: And[Pre] => createQuantifierStatement(quantifier, bindings, and.left, and.right) + case _ => ??? + } + } + + /** + * createQuantifierStatement creates a new quantifier statement based on the bindings + * @param expr + * @param bindings + * @param left + * @param right + * @return + */ + private final def createQuantifierStatement(expr: Expr[Pre], bindings: Seq[Variable[Pre]], left: Expr[Pre], right: Expr[Pre]): Scope[Post] = { + implicit val origin: Origin = expr.o + val newBindings = bindings.map(b => variables.succeed(b, b.rewrite())) + val bodyLoop = createBodyQuantifier(expr, bindings, left, right) + Scope(newBindings, bodyLoop) + } + + /** + * Creates the quantifier body and starts folding the quantifiers into loops + * @param expr + * @param bindings + * @param left + * @param right + * @return + */ + private final def createBodyQuantifier(expr: Expr[Pre], bindings: Seq[Variable[Pre]], left: Expr[Pre], right: Expr[Pre]): Statement[Post] = { + implicit val origin: Origin = expr.o + val bounds: ArrayBuffer[(Variable[Pre], Option[Expr[Pre]], Option[Expr[Pre]])] = FindBoundsQuantifier[Pre](this).findBounds(expr) + val loopCondition = Branch[Post](Seq((!dispatch(left), Continue[Post](None)))) + val loopOperation: Block[Post] = dispatchLoopBody(LoopBodyContent(right, expr)) + if(loopOperation.statements.isEmpty) { + return Block[Post](Seq.empty) + } + val loopBody : Block[Post] = Block(Seq(loopCondition, loopOperation)) + bindings.reverse.foldLeft[Statement[Post]](loopBody)((acc, element) => + createQuantifier(expr, acc, element, bounds.filter(i => i._1 == element)) + ) + } + + /** + * Creates the quantifier statement using the bounds + * @param expr + * @param acc + * @param element + * @param filteredBounds + * @return + */ + private final def createQuantifier(expr: Expr[Pre], acc: Statement[Post], element: Variable[Pre], filteredBounds: ArrayBuffer[(Variable[Pre], Option[Expr[Pre]], Option[Expr[Pre]])]): Loop[Post] = { + implicit val origin: Origin = expr.o + val minValue: Expr[Pre] = filteredBounds.map(i => i._2) + .collectFirst { case Some(value: Expr[Pre]) => value } + .getOrElse(const(MinValue)) + val maxValue: Expr[Pre] = filteredBounds.map(i => i._3) + .collectFirst { case Some(value: Expr[Pre]) => value } + .getOrElse(const(MaxValue)) + val localBinding = Local[Post](variables.freeze.succ(element)) + Loop[Post]( + Assign[Post](localBinding, dispatch(minValue))(null), + localBinding < dispatch(maxValue), + Assign[Post](localBinding, localBinding + const(1))(null), + LoopInvariant[Post](tt, None)(null), + acc + ) + } + + /** + * Dispatches the expression and changes the dereferences and thisObjects + * @param e + * @return + */ + override def dispatch(e: Expr[Pre]): Expr[Rewritten[Pre]] = { + e match { + case d: Deref[Pre] => getNewExpr(d) + case t: ThisObject[Pre] => getNewExpr(t) + case _ => super.dispatch(e) + } + } + + /** + * Creates a new expression for the dereferences and thisObjects + * @param e + * @return + */ + def getNewExpr(e: Expr[Pre]): Expr[Post] = { + e match { + case d: Deref[Pre] => d.rewrite(obj = getNewExpr(d.obj)) + case t: ThisObject[Pre] => pd.getOffset(t) + case _ => dispatch(e) + } + } + +} diff --git a/src/rewrite/vct/rewrite/runtime/util/CreateConstructor.scala b/src/rewrite/vct/rewrite/runtime/util/CreateConstructor.scala new file mode 100644 index 0000000000..cabf069102 --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/util/CreateConstructor.scala @@ -0,0 +1,87 @@ +package vct.rewrite.runtime.util + +import hre.util.ScopedStack +import vct.col.ast.RewriteHelpers.{RewriteApplicableContract, RewriteDeref} +import vct.col.ast._ +import vct.col.origin.{DiagnosticOrigin, Origin} +import vct.col.rewrite.{Generation, Rewriter, Rewritten} +import vct.col.util.AstBuildHelpers.tt +import vct.col.util.SuccessionMap +import vct.result.VerificationError.Unreachable + +case class CreateConstructor[Pre <: Generation](outer: Rewriter[Pre], val givenClassSucc: SuccessionMap[Type[Pre], Class[Rewritten[Pre]]]) extends Rewriter[Pre] { + override val allScopes = outer.allScopes + + val rewritingConstr: ScopedStack[(Seq[Variable[Pre]], TClass[Pre])] = ScopedStack() + + /** + * Dispatches the declarations and converts a procedure with a class return type to a constructor + * @param decl + */ + override def dispatch(decl: Declaration[Pre]): Unit = decl match { + case p: Procedure[Pre] => p.returnType match { + case tc: TClass[Pre] => rewritingConstr.having(p.args, tc) { + classDeclarations.declare(createClassConstructor(p)) + }; + case _ => ??? //("This procedure is expected to have a class as return type"); + } + case other => rewriteDefault(other) + } + + /** + * Creates a constructor from a procedure + * @param p + * @return + */ + def createClassConstructor(p: Procedure[Pre]): JavaConstructor[Post] = { + implicit val origin: Origin = DiagnosticOrigin + new JavaConstructor[Post](Seq(JavaPublic[Post]()), + rewritingConstr.top._2.cls.decl.o.getPreferredNameOrElse().ucamel, + p.args.map(createJavaParam), + variables.dispatch(p.typeArgs), + Seq.empty, + p.body match { + case Some(s: Scope[Pre]) => s.body match { + case b: Block[Pre] => dispatch(Block(b.statements.tail.dropRight(1))) + case other => dispatch(other) + } + case Some(_) => throw Unreachable("The body of a procedure always starts with a Scope.") + case None => Block(Seq.empty) + }, + p.contract.rewrite(ensures = UnitAccountedPredicate[Post](tt)))(null) + } + + /** + * Converts a variable to a Java parameter + * @param v + * @return + */ + def createJavaParam(v: Variable[Pre]): JavaParam[Post] = + new JavaParam[Post](Seq.empty, v.o.getPreferredNameOrElse().camel, dispatch(v.t))(v.o) + + /** + * Converts expressions to Java expressions + * @param e + * @return + */ + override def dispatch(e: Expr[Pre]): Expr[Post] = e match { + case l: Local[Pre] => + if (rewritingConstr.nonEmpty && rewritingConstr.top._1.contains(l.ref.decl)) + JavaLocal[Post](l.ref.decl.o.getPreferredNameOrElse().camel)(null)(e.o) + else rewriteDefault(l) + case t: ThisObject[Pre] => + val thisClassType = TClass(t.cls, Nil) + if (rewritingConstr.nonEmpty && rewritingConstr.top._2 == thisClassType) + ThisObject(givenClassSucc.ref[Post, Class[Post]](thisClassType))(t.o) + else rewriteDefault(t) + case d: Deref[Pre] => + if (rewritingConstr.nonEmpty) + d.obj match { + case _: Local[Pre] => d.rewrite(obj = ThisObject(givenClassSucc.ref[Post, Class[Post]](rewritingConstr.top._2))(d.o)) + case other => rewriteDefault(other) + } + else rewriteDefault(d) + case other => super.dispatch(other) + } + +} diff --git a/src/rewrite/vct/rewrite/runtime/util/FindBoundsQuantifier.scala b/src/rewrite/vct/rewrite/runtime/util/FindBoundsQuantifier.scala new file mode 100644 index 0000000000..ff6ba0e269 --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/util/FindBoundsQuantifier.scala @@ -0,0 +1,142 @@ +package vct.rewrite.runtime.util + +import hre.util.ScopedStack +import vct.col.ast.RewriteHelpers._ +import vct.col.ast._ +import vct.col.origin.Origin +import vct.col.rewrite.{Generation, Rewriter} +import vct.col.util.AstBuildHelpers._ + +import scala.collection.mutable.ArrayBuffer + + +case class FindBoundsQuantifier[Pre <: Generation](outer: AbstractQuantifierRewriter[Pre]) extends Rewriter[Pre] { + override val allScopes = outer.allScopes + + /** + * Bounds stack for the variables + */ + val bounds: ScopedStack[ArrayBuffer[(Variable[Pre], Option[Expr[Pre]], Option[Expr[Pre]])]] = new ScopedStack() + + /** + * Find the bounds for the quantifier + * @param expr + * @return + */ + def findBounds(expr: Expr[Pre]): ArrayBuffer[(Variable[Pre], Option[Expr[Pre]], Option[Expr[Pre]])] = { + bounds.having(new ArrayBuffer()) { + this.dispatch(expr) + bounds.top + } + } + + /** + * Dispatches the quantifier body + * @param expr + */ + def dispatchQuantifierBody(expr: Expr[Pre]): Unit = { + expr match { + case imp: Implies[Pre] => dispatch(imp.left) + case _ => + } + } + + /** + * Dispatches the starall + * @param starAll + * @return + */ + def dispatchStarAll(starAll: Starall[Pre]): Starall[Post] = { + dispatchQuantifierBody(starAll.body) + starAll.rewrite() + } + + /** + * Dispatches the exists + * @param exists + * @return + */ + def dispatchExists(exists: Exists[Pre]): Exists[Post] = { + dispatchQuantifierBody(exists.body) + exists.rewrite() + } + + /** + * Dispatches the forall + * @param forAll + * @return + */ + def dispatchForAll(forAll: Forall[Pre]): Forall[Post] = { + dispatchQuantifierBody(forAll.body) + forAll.rewrite() + } + + /** + * Dispatches the ambiguous greater expressions and stores the bounds in the bounds stack + * @param expr + * @param origin + */ + def dispatchAmbiguousGreater(expr: (Expr[Pre], Expr[Pre]))(implicit origin: Origin): Unit = { + implicit val origin: Origin = expr._1.o + expr match { + case (local: Local[Pre], local2: Local[Pre]) => { + bounds.top.addOne((local.ref.decl, Some(local2 + const(1)), None)) + bounds.top.addOne((local2.ref.decl, None, Some(local))) + } + case (local: Local[Pre], e: Expr[Pre]) => bounds.top.addOne((local.ref.decl, Some(e + const(1)), None)) + case (e: Expr[Pre], local: Local[Pre]) => bounds.top.addOne((local.ref.decl, None, Some(e))) + case _ => + } + } + + /** + * Dispatches the ambiguous greater equal expressions and stores the bounds in the bounds stack + * @param expr + * @param origin + */ + def dispatchAmbiguousGreaterEqual(expr: (Expr[Pre], Expr[Pre]))(implicit origin: Origin): Unit = { + expr match { + case (local: Local[Pre], local2: Local[Pre]) => { + bounds.top.addOne((local.ref.decl, Some(local2), None)) + bounds.top.addOne((local2.ref.decl, None, Some(local + const(1)))) + } + case (local: Local[Pre], e: Expr[Pre]) => bounds.top.addOne((local.ref.decl, Some(e), None)) + case (e: Expr[Pre], local: Local[Pre]) => bounds.top.addOne((local.ref.decl, None, Some(e + const(1)))) + case _ => + } + } + + /** + * Dispatches the ambiguous expressions using the dispatchAmbiguousGreater and dispatchAmbiguousGreaterEqual we can determine how to store + * them in the bounds stack + * @param expr + * @param origin + * @return + */ + def dispatchAmbiguous(expr: Expr[Pre])(implicit origin: Origin): Expr[Post] = { + expr match { + case ag: AmbiguousGreater[Pre] => dispatchAmbiguousGreater((ag.left, ag.right)) + case al: AmbiguousLess[Pre] => dispatchAmbiguousGreater((al.right, al.left)) + case age: AmbiguousGreaterEq[Pre] => dispatchAmbiguousGreaterEqual((age.left, age.right)) + case ale: AmbiguousLessEq[Pre] => dispatchAmbiguousGreaterEqual((ale.right, ale.left)) + case _ => ??? //Impossible + } + super.dispatch(expr) + } + + /** + * Dispatches the expressions + * @param e + * @return + */ + override def dispatch(e: Expr[Pre]): Expr[Post] = { + implicit val origin: Origin = e.o + e match { + case starAll: Starall[Pre] => dispatchStarAll(starAll) + case exists: Exists[Pre] => dispatchExists(exists) + case forAll: Forall[Pre] => dispatchForAll(forAll) + case _: AmbiguousGreater[Pre] | _: AmbiguousLess[Pre] | _: AmbiguousGreaterEq[Pre] | _: AmbiguousLessEq[Pre] => dispatchAmbiguous(e) + case _ => super.dispatch(e) + } + } +} diff --git a/src/rewrite/vct/rewrite/runtime/util/LedgerHelper.scala b/src/rewrite/vct/rewrite/runtime/util/LedgerHelper.scala new file mode 100644 index 0000000000..79cb5dcb64 --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/util/LedgerHelper.scala @@ -0,0 +1,295 @@ +package vct.rewrite.runtime.util + +import vct.col.ast._ +import vct.col.origin.{DiagnosticOrigin, Origin, PreferredName} +import vct.col.ref.Ref +import vct.col.rewrite.{Generation, Rewriter} +import vct.col.util.AstBuildHelpers +import vct.result.VerificationError.Unreachable + +import scala.collection.mutable.ArrayBuffer + +object LedgerHelper { + + /** + * Searches for the index of the instance field in the program + * @param program + * @param instanceField + * @tparam G + * @return + */ + def findNumberInstanceField[G](program: Program[G], instanceField: InstanceField[G]): Option[Int] = { + program + .declarations + .collect { case cls: Class[G] => cls } + .map(cls => cls.declarations) + .map(decls => decls.collect { case ifd: InstanceField[G] => ifd }) + .map(ifs => ifs.indexOf(instanceField)) + .find(i => i >= 0) + } + + /** + * Rewrites the ledger class and the dataobject class and returns a ledgermethodbuilder + * @param outer + * @tparam Pre + */ + case class LedgerRewriter[Pre <: Generation](outer: Rewriter[Pre]) extends Rewriter[Pre] { + override val allScopes = outer.allScopes + + /** + * rewrites the ledger and dataobject + * @param program + * @return + */ + def rewriteLedger(program: Program[Pre]): (LedgerMethodBuilderHelper[Post], Seq[Class[Post]], Seq[GlobalDeclaration[Pre]]) = { + val (Seq(ledgerClass: Class[Pre]), od: Seq[GlobalDeclaration[Pre]]) = program.declarations.partition { + case cls: Class[Pre] if cls.o.getLedgerClassRuntime.nonEmpty => true + case _ => false + } + + val (Seq(predicateClass: Class[Pre]), otherDeclarations: Seq[GlobalDeclaration[Pre]]) = od.partition { + case cls: Class[Pre] if cls.o.getDataObjectClassRuntime.nonEmpty => true + case _ => false + } + + val newClasses = classDeclarations.collect{ + dispatch(ledgerClass) + dispatch(predicateClass) + }._1 + + val ledgerRef: Ref[Post, Class[Post]] = this.anySucc(ledgerClass) + val predicateRef: Ref[Post, Class[Post]] = this.anySucc(predicateClass) + val newClass = ledgerRef.decl + val pmbh = DataMethodBuilderHelper[Post](predicateRef, predicateRef.decl.decls) + + (LedgerMethodBuilderHelper[Post](ledgerRef, newClass.decls, pmbh), + Seq(ledgerRef.decl, predicateRef.decl), + otherDeclarations) + } + } + + /** + * Ledger properties that can be used to find certain properties of the fields in the ledger + * @param inner + * @param outerHM + * @param refCls + * @param ledger + * @param origin + * @tparam G + */ + case class LedgerProperties[G](inner: Type[G], outerHM: Type[G], refCls: Ref[G, Class[G]], ledger: Option[InstanceField[G]])(implicit origin: Origin = DiagnosticOrigin) { + def deref: Option[Deref[G]] = ledger.map(l => Deref[G](StaticClassRef[G](refCls), l.ref)(null)(l.o)) + + def get(hm: Expr[G], key: Expr[G]): RuntimeConcurrentHashMapGet[G] = RuntimeConcurrentHashMapGet[G](hm, key) + + def get(key: Expr[G]): RuntimeConcurrentHashMapGet[G] = RuntimeConcurrentHashMapGet[G](deref.get, key) + + def getOrDefault(hm: Expr[G], key: Expr[G], default: Expr[G]): RuntimeConcurrentHashMapGetOrDefault[G] = RuntimeConcurrentHashMapGetOrDefault[G](hm, key, default) + + def getOrDefault(key: Expr[G], default: Expr[G]): RuntimeConcurrentHashMapGetOrDefault[G] = RuntimeConcurrentHashMapGetOrDefault[G](deref.get, key, default) + + def put(hm: Expr[G], key: Expr[G], value: Expr[G]): RuntimeConcurrentHashMapPut[G] = RuntimeConcurrentHashMapPut[G](hm, key, value) + + def put(key: Expr[G], value: Expr[G]): RuntimeConcurrentHashMapPut[G] = RuntimeConcurrentHashMapPut[G](deref.get, key, value) + + def containsKey(hm: Expr[G], key: Expr[G]): RuntimeConcurrentHashMapContainsKey[G] = RuntimeConcurrentHashMapContainsKey[G](hm, key) + + def containsKey(key: Expr[G]): RuntimeConcurrentHashMapContainsKey[G] = RuntimeConcurrentHashMapContainsKey[G](deref.get, key) + + def keySet(hm: Expr[G]): RuntimeConcurrentHashMapKeySet[G] = RuntimeConcurrentHashMapKeySet[G](hm); + def keySet(): RuntimeConcurrentHashMapKeySet[G] = RuntimeConcurrentHashMapKeySet[G](deref.get); + + def newInner: Expr[G] = { + inner match { + case _: RuntimeConcurrentHashMap[G] => RuntimeNewConcurrentHashMap[G](inner) + case _: CopyOnWriteArrayList[G] => CopyOnWriteArrayListNew[G](inner) + case _ => throw Unreachable(s"Add implementation for type: ${inner}") + } + } + + def newOuterMap: RuntimeNewConcurrentHashMap[G] = RuntimeNewConcurrentHashMap[G](outerHM) + + + def add(obj: Expr[G], arg: Expr[G]): CopyOnWriteArrayListAdd[G] = CopyOnWriteArrayListAdd[G](obj, arg) + def remove(obj: Expr[G], arg: Expr[G]): CopyOnWriteArrayListRemove[G] = CopyOnWriteArrayListRemove[G](obj, arg) + def contains(obj: Expr[G], arg: Expr[G]): CopyOnWriteArrayListContains[G] = CopyOnWriteArrayListContains[G](obj, arg) + + } + + object LedgerMethodBuilderHelper { + def apply[G](program: Program[G]): LedgerMethodBuilderHelper[G] = { + val cls = program.declarations.collectFirst { case cls: Class[G] if cls.o.getLedgerClassRuntime.nonEmpty => cls }.get + val predicatecls = program.declarations.collectFirst { case cls: Class[G] if cls.o.getDataObjectClassRuntime.nonEmpty => cls }.get + LedgerMethodBuilderHelper[G](cls.ref, cls.decls, DataMethodBuilderHelper[G](predicatecls.ref, predicatecls.decls)) + } + } + + /** + * Ledger method builder helper that can be used to find certain methods/fields in the ledger and make + * method invocations to those methods + * @param refCls + * @param clsDeclarations + * @param pmbh + * @param origin + * @tparam G + */ + case class LedgerMethodBuilderHelper[G](refCls: Ref[G, Class[G]], clsDeclarations: Seq[ClassDeclaration[G]], pmbh: DataMethodBuilderHelper[G])(implicit origin: Origin = DiagnosticOrigin) { + def threadId: ThreadId[G] = ThreadId[G](None)(DiagnosticOrigin) + + private def findAllMethods(methodName: String): Seq[InstanceMethod[G]] = clsDeclarations.collect { case i: InstanceMethod[G] if i.o.find[PreferredName].contains(PreferredName(Seq(methodName))) => i } + + private def findMethod(methodName: String): Option[InstanceMethod[G]] = findAllMethods(methodName).headOption + + private def findMethod(methodName: String, params: Int): Option[InstanceMethod[G]] = findAllMethods(methodName).find(i => i.args.size == params) + + private def findInstanceField(instanceFieldName: String): Option[InstanceField[G]] = clsDeclarations.collectFirst { case i: InstanceField[G] if i.o.find[PreferredName].contains(PreferredName(Seq(instanceFieldName))) => i } + + def ledgerProperties: LedgerProperties[G] = LedgerProperties[G]( + RuntimeConcurrentHashMap[G](TAnyClass[G](), TRuntimeFraction[G]())(DiagnosticOrigin), + RuntimeConcurrentHashMap[G](TLongObject[G](), RuntimeConcurrentHashMap[G](TAnyClass[G](), TRuntimeFraction[G]())(DiagnosticOrigin))(DiagnosticOrigin), + refCls, + findInstanceField("__runtime__") + ) + + def ledgerJoinTokensProperites: LedgerProperties[G] = LedgerProperties[G]( + TRuntimeFraction[G](), + RuntimeConcurrentHashMap[G](TAnyClass[G](), TRuntimeFraction[G]())(DiagnosticOrigin), + refCls, + findInstanceField("__join_tokens__") + ) + + def ledgerPredicateStore: LedgerProperties[G] = LedgerProperties[G]( + CopyOnWriteArrayList[G](TClass[G](pmbh.refCls, Nil)), + RuntimeConcurrentHashMap[G](TLongObject[G](), CopyOnWriteArrayList[G](TClass[G](pmbh.refCls, Nil)))(DiagnosticOrigin), + refCls, + findInstanceField("__predicate_store__") + ) + + + def injectivityMap: LedgerProperties[G] = LedgerProperties[G]( + TRuntimeFraction[G](), + RuntimeConcurrentHashMap[G](TAnyClass[G](), TRuntimeFraction[G]())(DiagnosticOrigin), + refCls, + None + ) + + def createNewInjectivityMap: Variable[G] = new Variable[G](injectivityMap.outerHM)(DiagnosticOrigin.where(name = "injectivityMap")) + + + def createHashMaps: Option[InstanceMethod[G]] = findMethod("createHashMap") + + def miCreateHashMaps: Option[MethodInvocation[G]] = createMethodInvocation(createHashMaps, Nil) + + def getPermission(params: Int): Option[InstanceMethod[G]] = findMethod("getPermission", params) + + def miGetPermission(input: Expr[G]): Option[MethodInvocation[G]] = createMethodInvocation(getPermission(1), Seq(input)) + + def getJoinToken: Option[InstanceMethod[G]] = findMethod("getJoinToken") + + def miGetJoinToken(input: Expr[G]): Option[MethodInvocation[G]] = createMethodInvocation(getJoinToken, Seq(input)) + + def setJoinToken: Option[InstanceMethod[G]] = findMethod("setJoinToken") + + def miSetJoinToken(input: Expr[G], value: Expr[G]): Option[MethodInvocation[G]] = createMethodInvocation(setJoinToken, Seq(input, value)) + + def setPermission(params: Int): Option[InstanceMethod[G]] = findMethod("setPermission", params) + + def miSetPermission(input: Expr[G], value: Expr[G]): Option[MethodInvocation[G]] = createMethodInvocation(setPermission(2), Seq(input, value)) + + def initiatePermission: Option[InstanceMethod[G]] = findMethod("initiatePermission", 2) + + def initiatePermission(params: Int): Option[InstanceMethod[G]] = findMethod("initiatePermission", params) + + def miInitiatePermission(input: Expr[G]): Option[MethodInvocation[G]] = createMethodInvocation(initiatePermission(1), Seq(input)) + + def miInitiatePermission(input: Expr[G], size: Expr[G]): Option[MethodInvocation[G]] = createMethodInvocation(initiatePermission(2), Seq(input, size)) + + + def hasPredicateCheck: Option[InstanceMethod[G]] = findMethod("hasPredicateCheck") + def miHasPredicateCheck(input: Expr[G]): Option[MethodInvocation[G]] = createMethodInvocation(hasPredicateCheck, Seq(input)) + + def foldPredicate: Option[InstanceMethod[G]] = findMethod("foldPredicate") + def miFoldPredicate(input: Expr[G]): Option[MethodInvocation[G]] = createMethodInvocation(foldPredicate, Seq(input)) + + def unfoldPredicate: Option[InstanceMethod[G]] = findMethod("unfoldPredicate") + def miUnfoldPredicate(input: Expr[G]): Option[MethodInvocation[G]] = createMethodInvocation(unfoldPredicate, Seq(input)) + + def checkForInjectivity: Option[InstanceMethod[G]] = findMethod("checkForInjectivity") + def miCheckForInjectivity(input: Expr[G]): Option[MethodInvocation[G]] = createMethodInvocation(checkForInjectivity, Seq(input)) + + def createMethodInvocation(imo: Option[InstanceMethod[G]], args: Seq[Expr[G]]): Option[MethodInvocation[G]] = imo.map(im => MethodInvocation[G]( + StaticClassRef[G](refCls), + im.ref, + args, + Nil, + Nil, + Nil, + Nil)(null)(im.o)) + + def createMethod(returnType: Type[G], args: Seq[Variable[G]], body: Option[Scope[G]], methodName: String): InstanceMethod[G] = { + new InstanceMethod( + returnType, + args, + Nil, + Nil, + body, + AstBuildHelpers.contract(null), + static = true + )(null)(DiagnosticOrigin.where(name = methodName).addLedgerClass()) + } + } + + /** + * Data method builder helper that can be used to find certain methods/fields in the DataObject and make + * method invocations to those methods + * @param refCls + * @param clsDeclarations + * @param origin + * @tparam G + */ + case class DataMethodBuilderHelper[G](refCls: Ref[G, Class[G]], clsDeclarations: Seq[ClassDeclaration[G]])(implicit origin: Origin = DiagnosticOrigin) { + + private def findAllMethods(methodName: String): Seq[InstanceMethod[G]] = clsDeclarations.collect { case i: InstanceMethod[G] if i.o.find[PreferredName].contains(PreferredName(Seq(methodName))) => i } + + private def findMethod(methodName: String): Option[InstanceMethod[G]] = findAllMethods(methodName).headOption + + private def findMethod(methodName: String, params: Int): Option[InstanceMethod[G]] = findAllMethods(methodName).find(i => i.args.size == params) + + private def findInstanceField(instanceFieldName: String): Option[InstanceField[G]] = clsDeclarations.collectFirst { case i: InstanceField[G] if i.o.find[PreferredName].contains(PreferredName(Seq(instanceFieldName))) => i } + + def dataField: Option[InstanceField[G]] = findInstanceField("data") + + def setData(params: Int): Option[InstanceMethod[G]] = findMethod("setData", params) + + def miSetData(obj: Expr[G], data: Expr[G]): Option[MethodInvocation[G]] = createMethodInvocation(setData(1), Seq(data), Some(obj)) + + def create: Option[InstanceMethod[G]] = findMethod("create") + + def miCreate(obj: Expr[G]): Option[MethodInvocation[G]] = createMethodInvocation(create, Seq(obj)) + + def createMethodInvocation(imo: Option[InstanceMethod[G]], args: Seq[Expr[G]], nonStatic: Option[Expr[G]] = None): Option[MethodInvocation[G]] = imo.map(im => MethodInvocation[G]( + nonStatic.getOrElse(StaticClassRef[G](refCls)), + im.ref, + args, + Nil, + Nil, + Nil, + Nil)(null)(im.o)) + + def createMethod(returnType: Type[G], args: Seq[Variable[G]], body: Option[Scope[G]], methodName: String, static: Boolean = true): InstanceMethod[G] = { + new InstanceMethod( + returnType, + args, + Nil, + Nil, + body, + AstBuildHelpers.contract(null), + static = static + )(null)(DiagnosticOrigin.where(name = methodName).addDataObjectClass()) + } + } + + + + +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/runtime/util/RewriteContractExpr.scala b/src/rewrite/vct/rewrite/runtime/util/RewriteContractExpr.scala new file mode 100644 index 0000000000..5b5f6f620b --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/util/RewriteContractExpr.scala @@ -0,0 +1,182 @@ +package vct.rewrite.runtime.util + +import hre.util.ScopedStack +import vct.col.ast.RewriteHelpers.RewriteDeref +import vct.col.ast._ +import vct.col.origin.{DiagnosticOrigin, Origin, PositionRange} +import vct.col.rewrite.{Generation, Rewritten} +import vct.col.util.AstBuildHelpers._ +import vct.result.VerificationError.Unreachable +import vct.rewrite.runtime.util.AbstractQuantifierRewriter.LoopBodyContent +import vct.rewrite.runtime.util.LedgerHelper._ +import vct.rewrite.runtime.util.Util.permissionToRuntimeValueRewrite +import vct.rewrite.runtime.util.permissionTransfer.PermissionData + + +case class RewriteContractExpr[Pre <: Generation](pd: PermissionData[Pre])(implicit program: Program[Pre]) extends AbstractQuantifierRewriter[Pre](pd) { + override val allScopes = pd.outer.allScopes + + /** + * Dispatches the loop body content + * defines that we are in a quantifier and unfolds the content of the loopbodyexpr + * @param loopBodyContent + * @param origin + * @return + */ + override def dispatchLoopBody(loopBodyContent: LoopBodyContent[Pre])(implicit origin: Origin): Block[Post] = { + inQuantifier.having(true){ + Block[Post](unfoldStar(loopBodyContent.expr).map(dispatchExpr)) + } + } + + + val inQuantifier: ScopedStack[Boolean] = ScopedStack() + inQuantifier.push(false) + val ledger: LedgerMethodBuilderHelper[Post] = pd.ledger.get + var injectivityMap: Variable[Post] = pd.injectivityMap.get + + + /** + * Creates assertions for a given contract expression + * @param expr + * @return + */ + def createAssertions(expr: Expr[Pre]): Statement[Post] = { + implicit val origin: Origin = expr.o + val (initInjectivityMap, checkInjectivtyMap) = createInjectivityMap + val unfoldedExpr = unfoldStar(expr) + val assertionChecks = unfoldedExpr.map(dispatchExpr) + assertionChecks match { + case Nil => Block[Post](Nil) + case _ => Block[Post](initInjectivityMap +: assertionChecks :+ checkInjectivtyMap) + } + } + + /** + * Creates a map for the injectivity map and creates a method invocation for checking the injectivity + * @return + */ + private def createInjectivityMap: (Statement[Post], Statement[Post]) = { + implicit val origin: Origin = DiagnosticOrigin + val assignInjectivtyMap = Assign[Post](injectivityMap.get, ledger.injectivityMap.newOuterMap)(null) + val checkInjectivityMap = Eval[Post](ledger.miCheckForInjectivity(injectivityMap.get).get) + (assignInjectivtyMap, checkInjectivityMap) + } + + /** + * Dispatches the expression and transform dereferences using the ThisObject by using the offset of the PermissionData + * class + * @param e + * @return + */ + override def dispatch(e: Expr[Pre]): Expr[Rewritten[Pre]] = { + e match { + case d@Deref(t@ThisObject(_), _) => d.rewrite(obj = pd.getOffset(t)) + case _ => super.dispatch(e) + } + } + + /** + * Dispatches the contract expression and determines what kind of assertions are needed to be created + * @param + * @param e + * @return + */ + private def dispatchExpr(e: Expr[Pre]): Statement[Post] = { + implicit val origin: Origin = e.o + e match { + case _: Star[Pre] => createAssertions(e) + case p: Perm[Pre] => dispatchPermission(p) + case ipa: InstancePredicateApply[Pre] => dispatchInstancePredicateApply(ipa) + case _: Starall[Pre] | _: Exists[Pre] | _: Forall[Pre] => { + super.dispatchQuantifier(e) + } + case _ => { + val rangeContent = e.o.find[PositionRange] + val readableContent = e.o.getReadable + + val linenum = rangeContent.map(_.startLineIdx).getOrElse(-1) + val lineDetails: String = (rangeContent, readableContent) match { + case Some(range) -> Some(readable) => readable.readable.readLines()(range.startLineIdx-1).replaceAll("\\\\", "").trim + case _ => "unknown line" + } + + RuntimeAssert[Post](super.dispatch(e), s"Assertion failed on line: ${linenum}\\n${lineDetails}")(null) + } + } + } + + /** + * Creates a permission assertion for array permissions and normal permissions + * @param p + * @param origin + * @return + */ + private def dispatchPermission(p: Perm[Pre])(implicit origin: Origin = p.o): Block[Post] = { + val cond = permissionToRuntimeValueRewrite(p) + val dataObject: Expr[Post] = p.loc.asInstanceOf[AmbiguousLocation[Pre]].expr match { + case d@Deref(o, _) => { + ledger.pmbh.miCreate(CreateObjectArray[Post]( + Seq(getNewExpr(o), + dispatch(const[Pre](findNumberInstanceField(program, d.ref.decl).get))) + )).get + } + case AmbiguousSubscript(coll, index) => { + ledger.pmbh.miCreate(CreateObjectArray[Post](Seq(getNewExpr(coll), dispatch(index)))).get + } + case _ => throw Unreachable(s"This type of permissions transfer is not yet supported: ${p}") + } + + val rangeContent = p.o.find[PositionRange] + val readableContent = p.o.getReadable + + val linenum = rangeContent.map(_.startLineIdx).getOrElse(-1) + val lineDetails: String = (rangeContent, readableContent) match { + case Some(range) -> Some(readable) => readable.readable.readLines()(range.startLineIdx-1).replaceAll("\\\\", "").trim + case _ => "unknown line" + } + + val getPermission = ledger.miGetPermission(dataObject).get + val injectivityMapFunctionality: Statement[Post] = if(inQuantifier.top){ + val containsInMap = ledger.injectivityMap.containsKey(injectivityMap.get, dataObject) + val checkDuplicates = RuntimeAssert[Post](!containsInMap, s"Permission cannot be checked twice for the same object in a quantifier, line: ${linenum}\\n ${lineDetails}")(null) + val putInjectivity = Eval[Post](ledger.injectivityMap.put(injectivityMap.get, dataObject, cond)) + Block[Post](Seq(checkDuplicates, putInjectivity)) + }else{ + val getOrDefaultPerm = ledger.injectivityMap.getOrDefault(injectivityMap.get, dataObject, RuntimeFractionZero[Post]()) + val putPermissionInjectivity = ledger.injectivityMap.put(injectivityMap.get, dataObject, getOrDefaultPerm r_+ cond) + Eval[Post](putPermissionInjectivity) + } + val check: Expr[Post] = (getPermission r_<=> cond) !== const(-1) // test if the value is equal or bigger than the required permission + val assertion = RuntimeAssertExpected[Post](check, cond, getPermission, s"Permission is not enough, line: ${linenum}\\n ${lineDetails}")(null) + Block[Post](Seq(injectivityMapFunctionality, assertion)) + } + + /** + * Dispatches the expression and transform dereferences using the ThisObject by using the offset of the PermissionData + * @param e + * @return + */ + override def getNewExpr(e: Expr[Pre]): Expr[Post] = { + e match { + case d: Deref[Pre] => d.rewrite(obj = getNewExpr(d.obj)) + case t: ThisObject[Pre] => pd.getOffset(t) + case _ => dispatch(e) + } + } + + /** + * dispatches the instance predicate apply and creates a method invocation to the ledger to check if the thread has the predicate + * @param ipa + * @return + */ + private def dispatchInstancePredicateApply(ipa: InstancePredicateApply[Pre]): Block[Post] = { + implicit val origin: Origin = ipa.o + val allArgs: Seq[Expr[Pre]] = ipa.args :+ ipa.obj :+ StringValue(ipa.ref.decl.o.getPreferredNameOrElse().camel) + val dispatchedArgs: Seq[Expr[Post]] = allArgs.map(dispatch) + val newObject = CreateObjectArray[Post](dispatchedArgs) + val mi: MethodInvocation[Post] = ledger.miHasPredicateCheck(newObject).get + Block[Post](Seq(Eval[Post](mi))) + } + +} diff --git a/src/rewrite/vct/rewrite/runtime/util/TransferPermissionRewriter.scala b/src/rewrite/vct/rewrite/runtime/util/TransferPermissionRewriter.scala new file mode 100644 index 0000000000..8ac653a7c1 --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/util/TransferPermissionRewriter.scala @@ -0,0 +1,139 @@ +package vct.rewrite.runtime.util + +import vct.col.ast.RewriteHelpers.RewriteDeref +import vct.col.ast._ +import vct.col.origin.Origin +import vct.col.rewrite.Generation +import vct.col.util.AstBuildHelpers._ +import vct.result.VerificationError.Unreachable +import vct.rewrite.runtime.util.AbstractQuantifierRewriter.LoopBodyContent +import vct.rewrite.runtime.util.LedgerHelper._ +import vct.rewrite.runtime.util.Util._ +import vct.rewrite.runtime.util.permissionTransfer.PermissionData + +case class TransferPermissionRewriter[Pre <: Generation](pd: PermissionData[Pre])(implicit program: Program[Pre]) extends AbstractQuantifierRewriter[Pre](pd) { + override val allScopes = pd.outer.allScopes + + implicit var add: Boolean = _ + + val ledger: LedgerMethodBuilderHelper[Post] = pd.ledger.get + + /** + * Adds the permissions to the thread + * @param predicate + * @return + */ + def addPermissions(predicate: Expr[Pre]): Block[Post] = { + add = true + transferPermissions(predicate) + } + + /** + * Removes the permissions from the thread + * @param predicate + * @return + */ + def removePermissions(predicate: Expr[Pre]): Block[Post] = { + add = false + transferPermissions(predicate) + } + + /** + * Dispatches the loop body content + * @param loopBodyContent + * @param origin + * @return the block returns by the addPermissions or removePermissions + */ + override def dispatchLoopBody(loopBodyContent: LoopBodyContent[Pre])(implicit origin: Origin): Block[Post] = { + if (add) { + TransferPermissionRewriter(pd).addPermissions(loopBodyContent.expr) + } else { + TransferPermissionRewriter(pd).removePermissions(loopBodyContent.expr) + } + } + + /** + * Dispatches the expression and only permissions and starall are dispatched to a block, the rest is dispatched to a empty block + * @param e + * @param origin + * @return the transferring statement block + */ + def dispatchExpr(e: Expr[Pre]): Statement[Post] = { + implicit val origin: Origin = e.o + e match { + case p: Perm[Pre] => Eval[Post](dispatchPerm(p)) + case s: Starall[Pre] => super.dispatchQuantifier(s) //Let the AbstractQuantifier rewrite the StarAll, since it is the only one that can hold permissions + case _ => Block[Post](Seq.empty) + } + } + + /** + * If the class needs to add use the + operator, otherwise use the - operator + * @param a + * @param b + * @param origin + * @return the function of the operator + */ + private def op(a: Expr[Post], b: Expr[Post])(implicit origin: Origin): Expr[Post] = if (add) a r_+ b else a r_- b + + /** + * Unfolds the predicate expression and collects the permissions + * @param predicate + * @return the permissions + */ + private def unfoldPredicate(predicate: Expr[Pre]): Seq[Expr[Pre]] = + unfoldStar(predicate).collect { case p@(_: Perm[Pre] | _: Starall[Pre] | _: InstancePredicateApply[Pre]) => p } + + /** + * transforms the predicate expression to a block of statements that add/remove permissions of a thread + * @param predicate + * @return + */ + private def transferPermissions(predicate: Expr[Pre]): Block[Post] = { + implicit val origin: Origin = predicate.o + Block[Post](unfoldPredicate(predicate).map(dispatchExpr)) + } + + /** + * Dispatches the permission and adds/removes the permission to the thread for normal permissions/ array permissions + * @param p + * @param origin + * @return the transferm permission statement + */ + private def dispatchPerm(p: Perm[Pre])(implicit origin: Origin): Expr[Post] = { + val newValue: Expr[Post] = pd.factored(permissionToRuntimeValueRewrite(p)) + + val pt: Option[Expr[Post]] = p.loc.asInstanceOf[AmbiguousLocation[Pre]].expr match { + case d@Deref(o, _) => { + val newDataObject: MethodInvocation[Post] = ledger.pmbh.miCreate( + CreateObjectArray[Post]( + Seq(getNewExpr(o),locationExpression(d.ref.decl)) + )).get + + val getPerm = ledger.miGetPermission(newDataObject).get + ledger.miSetPermission(newDataObject, op(getPerm, newValue)) + } + case AmbiguousSubscript(coll, index) => { + val newDataObject: MethodInvocation[Post] = ledger.pmbh.miCreate( + CreateObjectArray[Post](Seq(getNewExpr(coll), dispatch(index)))).get + val getPerm = ledger.miGetPermission(newDataObject).get + ledger.miSetPermission(newDataObject, op(getPerm, newValue)) + } + case _ => throw Unreachable(s"This type of permissions transfer is not yet supported: ${p}") + } + pt.getOrElse(tt) + } + + override def getNewExpr(e: Expr[Pre]): Expr[Post] = { + e match { + case d: Deref[Pre] => d.rewrite(obj = getNewExpr(d.obj)) + case t: ThisObject[Pre] => pd.getOffset(t) + case _ => dispatch(e) + } + } + + private def locationExpression(instanceField: InstanceField[Pre])(implicit origin: Origin): Expr[Post] = { + dispatch(const[Pre](findNumberInstanceField(program, instanceField).get)) + } + +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/runtime/util/Util.scala b/src/rewrite/vct/rewrite/runtime/util/Util.scala new file mode 100644 index 0000000000..2abf3dac14 --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/util/Util.scala @@ -0,0 +1,180 @@ +package vct.rewrite.runtime.util + + +import vct.col.ast._ +import vct.col.origin.{Origin, PreferredName} +import vct.col.ref.Ref +import vct.col.rewrite.{Generation, Rewriter, Rewritten} +import vct.col.util.AstBuildHelpers._ +import vct.col.util.FrozenScopes +import vct.result.VerificationError.Unreachable + +object Util { + + /** + * Collects all the classes that are extending a Thread + * @param declarations + * @tparam G + * @return + */ + def collectThreadClasses[G](declarations: Seq[Declaration[G]]): Seq[Class[G]] = { + declarations.collect { case c: Class[G] => c }.filter(isExtendingThread) + } + + /** + * get the run method of a start/join MethodInvocation + * @param mi + * @tparam G + * @return + */ + def getRunMethod[G](mi: MethodInvocation[G]): InstanceMethod[G] = { + if (!isThreadMethod(mi, "start") && !isThreadMethod(mi, "join")) { + throw Unreachable("Looking up the run method requires a start/join method as input") + } + getRunMethod(getClassOfMethodInvocation(mi)) + } + + /** + * Get the run method of the class + * @param cls + * @tparam G + * @return + */ + def getRunMethod[G](cls: Class[G]): InstanceMethod[G] = { + if (!isExtendingThread(cls)) { + throw Unreachable("Can only get a run method if the class is extending a Thread") + } + cls.declarations.collect { case i: InstanceMethod[G] => i }.find(i => isMethod(i, "run")).getOrElse({ + throw Unreachable("Extending Thread class should have a run method") + }) + } + + /** + * Does the method has the method name + * @param i + * @param methodName + * @tparam G + * @return + */ + def isMethod[G](i: InstanceMethod[G], methodName: String): Boolean = { + i.o.find[PreferredName].contains(PreferredName(Seq(methodName))) + } + + /** + * Is the class extending a Thread + * @param cls + * @tparam G + * @return + */ + def isExtendingThread[G](cls: Class[G]): Boolean = { + cls.supports.collectFirst { case TClass(Ref(cls), _) if cls.o.getPreferredNameOrElse().ucamel.contains("Thread") => () }.nonEmpty + } + + /** + * is the method a method with a certain name and is the class of the method extending a thread + * @param mi + * @param methodName + * @tparam G + * @return + */ + def isThreadMethod[G](mi: MethodInvocation[G], methodName: String): Boolean = { + isMethod(mi.ref.decl, methodName) && isExtendingThread(getClassOfMethodInvocation(mi)) + } + + /** + * + * @param mi + * @tparam G + * @return + */ + private def getClassOfMethodInvocation[G](mi: MethodInvocation[G]): Class[G] = { + mi.obj match { + case l: Local[G] => l.ref.decl.t.asInstanceOf[TClass[G]].cls.decl + case d: Deref[G] => d.ref.decl.t.asInstanceOf[TClass[G]].cls.decl + case _ => ??? + } + } + + /** + * Collects the method body + * @param i + * @tparam G + * @return + */ + def collectMethodBody[G](i: InstanceMethod[G]): Scope[G] = { + i.body match { + case Some(sc: Scope[G]) => sc + case _ => ??? + } + } + + /** + * Collects the block of the scope + * @param s + * @tparam G + * @return + */ + def collectBlockScope[G](s: Scope[G]): Block[G] = { + s.body match { + case b: Block[G] => b + case _ => ??? + } + } + + /** + * Converts a permission to a runtime value + * @param perm + * @param origin + * @tparam G + * @return + */ + def permissionToRuntimeValue[G](perm: Perm[G])(implicit origin: Origin): Expr[G] = { + permissionToRuntimeValue(perm.perm) + } + + /** + * Converts a permission expression to a runtime value + * @param expr + * @param origin + * @tparam G + * @return + */ + def permissionToRuntimeValue[G](expr: Expr[G])(implicit origin: Origin): Expr[G] = { + expr match { + case _: WritePerm[G] => RuntimeFractionOne() + case _: ReadPerm[G] => RuntimeFractionZero() + case d: RatDiv[G] => RuntimeFractionDiff[G](d.left, d.right) + case d: FloorDiv[G] => RuntimeFractionDiff[G](d.left, d.right) + case IntegerValue(n: BigInt) if n == 1 => RuntimeFractionOne() + case _ => expr + } + } + + /** + * Converts a permission to a runtime value and dispatches it to the next generation + * @param permission + * @param origin + * @tparam Pre + * @return + */ + def permissionToRuntimeValueRewrite[Pre <: Generation](permission: Perm[Pre])(implicit origin: Origin): Expr[Rewritten[Pre]] = { + type Post = Rewritten[Pre] + val rw = new Rewriter[Pre]() + val oldExpr: Expr[Pre] = permissionToRuntimeValue(permission.perm) + rw.dispatch(oldExpr) + } + + /** + * Returns the closest injectivity map, these are always present in the methods + * @param sc + * @tparam Pre + * @return + */ + def findClosestInjectivityMap[Pre <: Generation](sc: FrozenScopes[Pre, Rewritten[Pre], Variable[Pre], Variable[Rewritten[Pre]]]): Variable[Rewritten[Pre]] = { + sc.scopes.collectFirst{ + case m if m.values.exists(v => v.o.find[PreferredName].contains(PreferredName(Seq("injectivityMap")))) => + m.values.find(v => v.o.find[PreferredName].contains(PreferredName(Seq("injectivityMap")))).get + }.get + } + +} diff --git a/src/rewrite/vct/rewrite/runtime/util/permissionTransfer/PermissionData.scala b/src/rewrite/vct/rewrite/runtime/util/permissionTransfer/PermissionData.scala new file mode 100644 index 0000000000..d55e0574fe --- /dev/null +++ b/src/rewrite/vct/rewrite/runtime/util/permissionTransfer/PermissionData.scala @@ -0,0 +1,106 @@ +package vct.rewrite.runtime.util.permissionTransfer + +import vct.col.ast.{Variable, _} +import vct.col.origin.Origin +import vct.col.rewrite.{Generation, Rewriter, Rewritten} +import vct.col.util.AstBuildHelpers._ +import vct.rewrite.runtime.util.LedgerHelper.LedgerMethodBuilderHelper + +import scala.annotation.tailrec +import scala.collection.immutable.Seq + + +/** + * PermissionData is a data structure that holds the permission content + * to be used in the permission rewriters + * @tparam G + */ +sealed trait PermissionContent[G <: Generation] +case class ClassArg[G <: Generation](cls: Class[G]) extends PermissionContent[G] +case class Outer[G <: Generation](outer: Rewriter[G]) extends PermissionContent[G] +case class FactorContent[G <: Generation](factor: Expr[Rewritten[G]]) extends PermissionContent[G] +case class TreadIdContent[G <: Generation](threadId: Expr[Rewritten[G]]) extends PermissionContent[G] +case class Offset[G <: Generation](offset: Expr[Rewritten[G]]) extends PermissionContent[G] +case class Ledger[G <: Generation](ledger: LedgerMethodBuilderHelper[Rewritten[G]]) extends PermissionContent[G] +case class InjectivityMap[G <: Generation](map: Variable[Rewritten[G]]) extends PermissionContent[G] + +object PermissionData { + def apply[Pre <: Generation](): PermissionData[Pre] = { + PermissionData[Pre](Seq.empty) + } +} + +case class PermissionData[Pre <: Generation](permissionContent: Seq[PermissionContent[Pre]]) { + type Post = Rewritten[Pre] + + lazy val cls : Option[Class[Pre]] = permissionContent.collectFirst { case c: ClassArg[Pre] => c }.map(c => c.cls) + lazy val outer : Rewriter[Pre] = permissionContent.collectFirst { case o: Outer[Pre] => o }.map(o => o.outer).getOrElse(new Rewriter()) + lazy val factor: Option[Expr[Post]] = permissionContent.collectFirst { case o: FactorContent[Pre] => o }.map(f => f.factor) + lazy val threadId: ThreadId[Post] = ThreadId[Post](permissionContent.collectFirst { case o: TreadIdContent[Pre] => o }.map(t => t.threadId))(Origin(Seq.empty)) + lazy val offset: Option[Expr[Post]] = permissionContent.collectFirst { case o: Offset[Pre] => o }.map(o => o.offset) + lazy val ledger: Option[LedgerMethodBuilderHelper[Post]] = permissionContent.collectFirst { case o: Ledger[Pre] => o }.map(o => o.ledger) + lazy val injectivityMap: Option[Variable[Post]] = permissionContent.collectFirst { case o: InjectivityMap[Pre] => o }.map(o => o.map) + + + def factored(e: Expr[Post])(implicit origin: Origin = e.o): Expr[Post] = factor match { + case Some(f: Expr[Post]) => f r_* e + case _ => e + } + + def getOffset(e: Expr[Pre]): Expr[Post] = { + if(offset.isEmpty) { + return outer.dispatch(e) + } + offset.get + } + + def setCls(newArg: Class[Pre]): PermissionData[Pre] = { + PermissionData[Pre](permissionContent.flatMap{ + case ea: ClassArg[Pre] => Nil + case o => Seq(o) + } :+ ClassArg[Pre](newArg)) + } + + def setOuter(newArg: Rewriter[Pre]): PermissionData[Pre] = { + PermissionData[Pre](permissionContent.flatMap{ + case _: Outer[Pre] => Nil + case o => Seq(o) + } :+ Outer[Pre](newArg)) + } + + def setFactor(newArg: Expr[Post]): PermissionData[Pre] = { + PermissionData[Pre](permissionContent.flatMap{ + case ea: FactorContent[Pre] => Nil + case o => Seq(o) + } :+ FactorContent[Pre](newArg)) + } + + def setThreadId(newArg: Expr[Post]): PermissionData[Pre] = { + PermissionData[Pre](permissionContent.flatMap{ + case ea: TreadIdContent[Pre] => Nil + case o => Seq(o) + } :+ TreadIdContent[Pre](newArg)) + } + + def setOffset(newArg: Expr[Post]): PermissionData[Pre] = { + PermissionData[Pre](permissionContent.flatMap{ + case ea: Offset[Pre] => Nil + case o => Seq(o) + } :+ Offset[Pre](newArg)) + } + + def setLedger(newArg: LedgerMethodBuilderHelper[Post]): PermissionData[Pre] = { + PermissionData[Pre](permissionContent.flatMap { + case ea: Ledger[Pre] => Nil + case o => Seq(o) + } :+ Ledger[Pre](newArg)) + } + + def setInjectivityMap(newArg: Variable[Post]): PermissionData[Pre] = { + PermissionData[Pre](permissionContent.flatMap { + case ea: InjectivityMap[Pre] => Nil + case o => Seq(o) + } :+ InjectivityMap[Pre](newArg)) + } +} + diff --git a/test/main/vct/test/integration/examples/RuntimeSpec.scala b/test/main/vct/test/integration/examples/RuntimeSpec.scala new file mode 100644 index 0000000000..4e784725dc --- /dev/null +++ b/test/main/vct/test/integration/examples/RuntimeSpec.scala @@ -0,0 +1,11 @@ +package vct.test.integration.examples + +import vct.test.integration.helper.VercorsSpec + +import scala.language.postfixOps + +class RuntimeSpec extends VercorsSpec { + // Demos + vercors should verify using runtime example "runtime/test.java" in 20 + +} diff --git a/test/main/vct/test/integration/helper/VercorsSpec.scala b/test/main/vct/test/integration/helper/VercorsSpec.scala index 048f559b8b..d35f53eba5 100644 --- a/test/main/vct/test/integration/helper/VercorsSpec.scala +++ b/test/main/vct/test/integration/helper/VercorsSpec.scala @@ -5,6 +5,10 @@ import hre.io.{LiteralReadable, Readable} import org.scalactic.source import org.scalatest.Tag import org.scalatest.concurrent.TimeLimits.failAfter +import org.scalatest.concurrent.TimeLimits.{cancelAfter, failAfter} +import org.scalatest.events.TestCanceled +import org.scalatest.exceptions.TestCanceledException +import org.scalatest.time._ import org.scalatest.flatspec.AnyFlatSpec import org.scalatest.time._ import org.slf4j.LoggerFactory @@ -12,9 +16,9 @@ import scopt.OParser import vct.col.origin.{BlameUnreachable, VerificationFailure} import vct.col.rewrite.bip.BIP.Standalone.VerificationReport import vct.main.Main.TemporarilyUnsupported -import vct.main.modes.Verify +import vct.main.modes.{RuntimeVerification, Verify} import vct.options.{Options, types} -import vct.options.types.{Backend, PathOrStd} +import vct.options.types.{Backend, Mode, PathOrStd} import vct.parsers.err.ParseError import vct.result.VerificationError import vct.result.VerificationError.{SystemError, UserError} @@ -41,6 +45,14 @@ abstract class VercorsSpec extends AnyFlatSpec { case Error(_) => "error" } } + + sealed trait RuntimeType { + override def toString: String = this match { + case Runtime => "runtime" + } + } + + case object Runtime extends RuntimeType case object Pass extends Verdict case object AnyFail extends Verdict case class Fail(code: String) extends Verdict @@ -99,6 +111,40 @@ abstract class VercorsSpec extends AnyFlatSpec { } } + + private def registerRuntimeTest(verdict: VercorsSpec.this.Verdict, input: PathOrStd, time: Int, desc: String): Unit = { + val fullDesc: String = s"${desc.capitalize} produces verdict $verdict with runtime".replaceAll("should", "shld") + val tags: Seq[Tag] = Seq(new Tag("exampleCaseRuntime")) + val matrixId = Math.floorMod(fullDesc.hashCode, MATRIX_COUNT) + val matrixTag = Tag(s"MATRIX[$matrixId]") + + val options: Options = Options(mode = Mode.RuntimeVerification, inputs = Seq(input), runtimeOutput = Path.of("output.java")) + registerTest(fullDesc, (Tag("MATRIX") +: matrixTag +: tags): _*) { + +// TODO build something that detects if a program terminated without errors + var testCanceled = false + try { + cancelAfter(Span(time, Seconds)) { + RuntimeVerification.runOptions(options) + } + }catch { + case tc: TestCanceledException => testCanceled = true + } + + if (!testCanceled) { + fail("Program terminated") + } + + } + + +// registerTest(fullDesc, (Tag("MATRIX") +: matrixTag +: tags): _*) { +// cancelAfter(Span(time, Seconds)) { +// RuntimeVerification.runOptions() +// } +// } + } + private def matchVerdict(verdict: Verdict, value: Either[VerificationError, (Seq[VerificationFailure], VerificationReport)]): Unit = { value match { case Left(err: TemporarilyUnsupported) => @@ -181,6 +227,19 @@ abstract class VercorsSpec extends AnyFlatSpec { class VerdictPhrase(val verdict: Verdict, val reportPath: Option[Path]) { def using(backend: Seq[Backend]): BackendPhrase = new BackendPhrase(verdict, reportPath, backend, Nil) + def using(runtime: RuntimeType) = new RuntimePhrase(verdict) + } + + class RuntimePhrase(verdict: Verdict) { + def example(path: String)(implicit pos: source.Position): TimePhrase = { + new TimePhrase(verdict, PathOrStd.Path(Path.of(s"examples/$path"))) + } + } + + class TimePhrase(verdict: Verdict, input: PathOrStd) { + def in(time: Int): Unit = { + registerRuntimeTest(verdict, input, time, s"Runtime example ${input.fileName}") + } } class BackendPhrase(val verdict: Verdict, val reportPath: Option[Path], val backends: Seq[Backend], val _flags: Seq[String]) { @@ -229,6 +288,7 @@ abstract class VercorsSpec extends AnyFlatSpec { val verify: Verdict = Pass val fail: IncompleteVerdict = IncompleteVerdict(Fail) val error: ErrorVerdict.type = ErrorVerdict + val runtime: RuntimeType = Runtime val silicon: Seq[Backend] = Seq(types.Backend.Silicon) val carbon: Seq[Backend] = Seq(types.Backend.Carbon)