Veymont pre

col/src/main/java/vct/col/ast/Node.scala

@@ -58,10 +58,11 @@ import vct.col.ast.statement.composite._
 import vct.col.ast.statement.exceptional._
 import vct.col.ast.statement.nonexecutable._
 import vct.col.ast.statement.terminal._
+import vct.col.ast.statement.veymont.VeyMontCommImpl
 import vct.col.ast.util.Declarator
 import vct.col.debug._
 import vct.col.origin._
-import vct.col.ref.Ref
+import vct.col.ref.{DirectRef, Ref}
 import vct.col.resolve._
 import vct.col.resolve.ctx._
 import vct.col.resolve.lang.JavaAnnotationData
@@ -127,6 +128,8 @@ final case class TZFraction[G]()(implicit val o: Origin = DiagnosticOrigin) exte
 sealed trait DeclaredType[G] extends Type[G] with DeclaredTypeImpl[G]
 final case class TModel[G](model: Ref[G, Model[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TModelImpl[G]
 final case class TClass[G](cls: Ref[G, Class[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TClassImpl[G]
+final case class TSeqProg[G](cls: Ref[G, VeyMontSeqProg[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TSeqProgImpl[G]
+final case class TVeyMontThread[G](cls: Ref[G, VeyMontThread[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TVeyMontThreadImpl[G]
 final case class TAnyClass[G]()(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TAnyClassImpl[G]
 final case class TAxiomatic[G](adt: Ref[G, AxiomaticDataType[G]], args: Seq[Type[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TAxiomaticImpl[G]
 final case class TEnum[G](enum: Ref[G, Enum[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G]
@@ -212,6 +215,8 @@ sealed trait GlobalDeclaration[G] extends Declaration[G] with GlobalDeclarationI
 final class SimplificationRule[G](val axiom: Expr[G])(implicit val o: Origin) extends GlobalDeclaration[G] with SimplificationRuleImpl[G]
 final class AxiomaticDataType[G](val decls: Seq[ADTDeclaration[G]], val typeArgs: Seq[Variable[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with AxiomaticDataTypeImpl[G]
 final class Class[G](val declarations: Seq[ClassDeclaration[G]], val supports: Seq[Ref[G, Class[G]]], val intrinsicLockInvariant: Expr[G])(implicit val o: Origin) extends GlobalDeclaration[G] with ClassImpl[G]
+final class VeyMontSeqProg[G](val contract: ApplicableContract[G], val progArgs : Seq[Variable[G]], val threads: Seq[VeyMontThread[G]], val runMethod: ClassDeclaration[G], val methods: Seq[ClassDeclaration[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with VeyMontSeqProgImpl[G]
+final class VeyMontThread[G](val threadType: Type[G], val args: Seq[Expr[G]])(implicit val o: Origin) extends Declaration[G]
 final class Model[G](val declarations: Seq[ModelDeclaration[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with Declarator[G] with ModelImpl[G]
 final class Function[G](val returnType: Type[G], val args: Seq[Variable[G]], val typeArgs: Seq[Variable[G]],
                val body: Option[Expr[G]], val contract: ApplicableContract[G], val inline: Boolean = false, val threadLocal: Boolean = false)
@@ -405,6 +410,7 @@ final case class AmbiguousThis[G]()(implicit val o: Origin) extends Expr[G] with
 
 final case class ThisObject[G](cls: Ref[G, Class[G]])(implicit val o: Origin) extends Expr[G] with ThisObjectImpl[G]
 final case class ThisModel[G](cls: Ref[G, Model[G]])(implicit val o: Origin) extends Expr[G] with ThisModelImpl[G]
+final case class ThisSeqProg[G](cls: Ref[G, VeyMontSeqProg[G]])(implicit val o: Origin) extends Expr[G] with ThisSeqProgImpl[G]
 
 final case class AmbiguousResult[G]()(implicit val o: Origin) extends Expr[G] with AmbiguousResultImpl[G] {
   var ref: Option[ResultTarget[G]] = None
@@ -445,6 +451,7 @@ sealed trait HeapDeref[G] extends Expr[G] with HeapDerefImpl[G]
 final case class Deref[G](obj: Expr[G], ref: Ref[G, InstanceField[G]])(val blame: Blame[InsufficientPermission])(implicit val o: Origin) extends Expr[G] with HeapDeref[G] with DerefImpl[G]
 final case class ModelDeref[G](obj: Expr[G], ref: Ref[G, ModelField[G]])(val blame: Blame[ModelInsufficientPermission])(implicit val o: Origin) extends Expr[G] with ModelDerefImpl[G]
 final case class DerefPointer[G](pointer: Expr[G])(val blame: Blame[PointerDerefError])(implicit val o: Origin) extends Expr[G] with DerefPointerImpl[G]
+final case class DerefVeyMontThread[G](ref: Ref[G,VeyMontThread[G]])(implicit val o: Origin) extends Expr[G] with DerefVeyMontThreadImpl[G]
 final case class PointerAdd[G](pointer: Expr[G], offset: Expr[G])(val blame: Blame[PointerAddError])(implicit val o: Origin) extends Expr[G] with PointerAddImpl[G]
 final case class AddrOf[G](e: Expr[G])(implicit val o: Origin) extends Expr[G] with AddrOfImpl[G]
 final case class FunctionOf[G](binding: Ref[G, Variable[G]], vars: Seq[Ref[G, Variable[G]]])(implicit val o: Origin) extends Expr[G] with FunctionOfImpl[G]
@@ -522,6 +529,7 @@ final case class Star[G](left: Expr[G], right: Expr[G])(implicit val o: Origin)
 final case class Wand[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends Expr[G] with WandImpl[G]
 final case class Scale[G](scale: Expr[G], res: Expr[G])(val blame: Blame[ScaleNegative])(implicit val o: Origin) extends Expr[G] with ScaleImpl[G]
 final case class ScaleByParBlock[G](block: Ref[G, ParBlockDecl[G]], res: Expr[G])(implicit val o: Origin) extends Expr[G] with ScaleByParBlockImpl[G]
+final case class VeyMontCondition[G](condition: Seq[(Ref[G,VeyMontThread[G]],Expr[G])])(implicit val o: Origin) extends Expr[G] with VeyMontConditionImpl[G]
 final case class PolarityDependent[G](onInhale: Expr[G], onExhale: Expr[G])(implicit val o: Origin) extends Expr[G] with PolarityDependentImpl[G]
 
 final case class Unfolding[G](res: Expr[G], body: Expr[G])(val blame: Blame[UnfoldFailed])(implicit val o: Origin) extends Expr[G] with UnfoldingImpl[G]
@@ -647,6 +655,8 @@ final case class SuperType[G](left: Expr[G], right: Expr[G])(implicit val o: Ori
 final case class IndeterminateInteger[G](min: Expr[G], max: Expr[G])(implicit val o: Origin) extends Expr[G] with IndeterminateIntegerImpl[G]
 
 sealed trait AssignExpression[G] extends Expr[G] with AssignExpressionImpl[G]
+final case class VeyMontCommExpression[G](receiver: Ref[G,VeyMontThread[G]], sender : Ref[G,VeyMontThread[G]], assign: Statement[G])(implicit val o: Origin) extends Statement[G] with VeyMontCommImpl[G]
+final case class VeyMontAssignExpression[G](thread : Ref[G,VeyMontThread[G]], assign: Statement[G])(implicit val o: Origin) extends Statement[G]
 final case class PreAssignExpression[G](target: Expr[G], value: Expr[G])(val blame: Blame[AssignFailed])(implicit val o: Origin) extends AssignExpression[G] with PreAssignExpressionImpl[G]
 final case class PostAssignExpression[G](target: Expr[G], value: Expr[G])(val blame: Blame[AssignFailed])(implicit val o: Origin) extends AssignExpression[G] with PostAssignExpressionImpl[G]
 

col/src/main/java/vct/col/ast/declaration/global/VeyMontSeqProgImpl.scala

@@ -0,0 +1,11 @@
+package vct.col.ast.declaration.global
+
+import vct.col.ast.{Class, Declaration, VeyMontSeqProg}
+import vct.col.ast.util.Declarator
+import vct.col.check.{CheckContext, CheckError}
+import vct.col.origin.Origin
+
+trait VeyMontSeqProgImpl[G] extends Declarator[G] { this: VeyMontSeqProg[G] =>
+  def members: Seq[Declaration[G]] = threads ++ Seq(runMethod) ++ methods
+  override def declarations: Seq[Declaration[G]] = progArgs ++ members
+}

col/src/main/java/vct/col/ast/expr/context/ThisSeqProgImpl.scala

@@ -0,0 +1,7 @@
+package vct.col.ast.expr.context
+
+import vct.col.ast.{TAnyClass, TSeqProg, ThisSeqProg, Type}
+
+trait ThisSeqProgImpl[G] { this: ThisSeqProg[G] =>
+  override def t: Type[G] = TSeqProg(cls)
+}

col/src/main/java/vct/col/ast/expr/heap/read/DerefVeyMontThreadImpl.scala

@@ -0,0 +1,8 @@
+package vct.col.ast.expr.heap.read
+
+import vct.col.ast.{DerefVeyMontThread, Type}
+
+trait DerefVeyMontThreadImpl[G] {
+  this: DerefVeyMontThread[G] =>
+  override def t: Type[G] = ref.decl.threadType
+}

col/src/main/java/vct/col/ast/expr/op/bool/VeyMontConditionImpl.scala

@@ -0,0 +1,7 @@
+package vct.col.ast.expr.op.bool
+
+import vct.col.ast.{TBool, Type, VeyMontCondition}
+
+trait VeyMontConditionImpl[G] { this: VeyMontCondition[G] =>
+  override def t: Type[G] = TBool()
+}

col/src/main/java/vct/col/ast/lang/PVLLocalImpl.scala

@@ -12,5 +12,6 @@ trait PVLLocalImpl[G] { this: PVLLocal[G] =>
     case ref: RefClass[G] => Types.notAValue(ref)
     case ref: RefField[G] => ref.decl.t
     case ref: RefModelField[G] => ref.decl.t
+    case ref: RefVeyMontThread[G] => ref.decl.threadType
   }
 }

col/src/main/java/vct/col/ast/statement/veymont/VeyMontCommImpl.scala

@@ -0,0 +1,7 @@
+package vct.col.ast.statement.veymont
+
+import vct.col.ast.{VeyMontCommExpression}
+
+trait VeyMontCommImpl[G] { this: VeyMontCommExpression[G] =>
+
+}

col/src/main/java/vct/col/ast/type/TSeqProgImpl.scala

@@ -0,0 +1,7 @@
+package vct.col.ast.`type`
+
+import vct.col.ast.TSeqProg
+
+trait TSeqProgImpl[G] { this: TSeqProg[G] =>
+
+}

col/src/main/java/vct/col/ast/type/TVeyMontThreadImpl.scala

@@ -0,0 +1,7 @@
+package vct.col.ast.`type`
+
+import vct.col.ast.TVeyMontThread
+
+trait TVeyMontThreadImpl[G] { this: TVeyMontThread[G] =>
+
+}

col/src/main/java/vct/col/print/Printer.scala

@@ -454,6 +454,10 @@ case class Printer(out: Appendable,
       statement("return", space, result)
     case Assign(target, value) =>
       statement(target, space, "=", space, value)
+    case va: VeyMontAssignExpression[_] =>
+      statement(va.assign.asInstanceOf[Assign[_]].target, space, "=", space, va.assign.asInstanceOf[Assign[_]].value)
+    case vc: VeyMontCommExpression[_] =>
+      statement(vc.assign.asInstanceOf[Assign[_]].target, space, "=", space, vc.assign.asInstanceOf[Assign[_]].value)
     case block: Block[_] =>
       printBlock(block, newline = true)
     case Scope(locals, body) =>
@@ -465,15 +469,21 @@ case class Printer(out: Appendable,
     case Branch(branches) =>
       val `if` = (phrase("if (", branches.head._1, ")"), branches.head._2)
       val others = branches.tail.map {
-        case (cond, impl) => (phrase("else if (", cond, ")"), impl)
+        case (cond, impl) =>
+          if(cond match{ case BooleanValue(value) => value}) { //if cond == true
+            (phrase("else"),impl)
+          } else
+            (phrase("else if(", cond, ")"), impl) //never reached since the two branches in else { if(cond) statement } are mapped separately
       }
       controls(`if` +: others)
     case Switch(expr, body) =>
       control(phrase("switch (", expr, ")"), body)
     case Loop(Block(Nil), cond, Block(Nil), invariant, body) =>
       control(phrase(printLoopInvariant(invariant), newline, "while (", cond, ")"), body)
     case Loop(init, cond, update, invariant, body) =>
-      control(phrase(printLoopInvariant(invariant), newline, "for (", statement_no_semicolon(init), "; ", cond, "; ", statement_no_semicolon(update), ")"), body)
+      if(isSkip(init) && isSkip(update))
+        control(phrase(printLoopInvariant(invariant), newline, "while(", cond, ")"), body)
+      else control(phrase(printLoopInvariant(invariant), newline, "for(", init, "; ", cond, "; ", statement_no_semicolon(update), ")"), body)
     case TryCatchFinally(body, after, catches) =>
       controls(
         Seq((phrase("try"), body)) ++
@@ -735,6 +745,11 @@ case class Printer(out: Appendable,
       phrase(name(ref.decl), "(", commas(args.map(NodePhrase)), ")")
   }
 
+  private def isSkip(st: Statement[_]): Boolean = st match {
+    case Block(stmts) => stmts.isEmpty
+    case _ => false
+  }
+
   def printExpr(e: Expr[_]): Unit =
     say(expr(e)._1)
 
@@ -833,6 +848,8 @@ case class Printer(out: Appendable,
       (phrase("running", "(", thread, ")"), 100)
     case Starall(bindings, triggers, body) =>
       (phrase("(", "\\forall*", space, commas(bindings.map(NodePhrase)), "; true; ", body, ")"), 120)
+    case VeyMontCondition(c) =>
+      (phrase(intersperse(" && ", c.map{case (t,e) => e})),40)
     case Star(left, right) =>
       (phrase(assoc(40, left), space, "**", space, assoc(40, right)), 40)
     case Wand(left, right) =>
@@ -927,6 +944,7 @@ case class Printer(out: Appendable,
       (phrase(name(ref.decl)), 110)
     case Deref(obj, ref) =>
       (phrase(assoc(100, obj), ".", name(ref.decl)), 100)
+    case DerefVeyMontThread(ref) => (phrase(name(ref.decl)), 110)
     case ModelDeref(obj, ref) =>
       (phrase(assoc(100, obj), ".", name(ref.decl)), 100)
     case DerefPointer(pointer) =>
@@ -946,7 +964,10 @@ case class Printer(out: Appendable,
     case FunctionInvocation(ref, args, typeArgs, givenMap, yields) =>
       (phrase(name(ref.decl), "(", commas(args.map(NodePhrase)), ")"), 100)
     case MethodInvocation(obj, ref, args, outArgs, typeArgs, givenMap, yields) =>
-      (phrase(assoc(100, obj), ".", name(ref.decl), "(", commas(args.map(NodePhrase)), ")"), 100)
+      obj match {
+        case o:ThisSeqProg[_] => (phrase(name(ref.decl), "(", commas(args.map(NodePhrase)), ")"), 100)
+        case _ => (phrase(assoc(100, obj), ".", name(ref.decl), "(", commas(args.map(NodePhrase)), ")"), 100)
+      }
     case InstanceFunctionInvocation(obj, ref, args, typeArgs, givenMap, yields) =>
       (phrase(assoc(100, obj), ".", name(ref.decl), "(", commas(args.map(NodePhrase)), ")"), 100)
     case UMinus(arg) =>
@@ -1005,12 +1026,16 @@ case class Printer(out: Appendable,
       (phrase(bind(60, left), space, ">", space, bind(60, right)), 60)
     case Less(left, right) =>
       (phrase(bind(60, left), space, "<", space, bind(60, right)), 60)
+    case AmbiguousLess(left, right) =>
+      (phrase(bind(60, left), space, "<", space, bind(60, right)), 60)
     case AmbiguousGreaterEq(left, right) =>
       (phrase(bind(60, left), space, ">=", space, bind(60, right)), 60)
     case GreaterEq(left, right) =>
       (phrase(bind(60, left), space, ">=", space, bind(60, right)), 60)
     case LessEq(left, right) =>
       (phrase(bind(60, left), space, "<=", space, bind(60, right)), 60)
+    case AmbiguousLessEq(left, right) =>
+      (phrase(bind(60, left), space, "<=", space, bind(60, right)), 60)
     case SubSet(left, right) =>
       ???
     case SubSetEq(left, right) =>
@@ -1377,6 +1402,21 @@ case class Printer(out: Appendable,
       ???
     case field: ModelField[_] =>
       ???
+    case seqprog: VeyMontSeqProg[_] => phrase(
+      doubleline,
+      seqprog.contract, newline,
+      "seq_program", space, name(seqprog),"(",commas(seqprog.progArgs.map(NodePhrase)) ,")", space, "{",
+      indent(phrase(seqprog.members.map(NodePhrase): _*)),
+      "}",
+      doubleline)
+    case thread: VeyMontThread[_] => phrase(newline,"thread",space,name(thread),space,"=",space,thread.threadType,"(",commas(thread.args.map(NodePhrase)),")",newline)
+    case runMethod : RunMethod[_] => {
+      val header = phrase(runMethod.contract,"run")
+      runMethod.body match {
+        case Some(body) => control(header, body)
+        case None => phrase(doubleline, header, ";", doubleline)
+      }
+    }
   })
 
   def printApplicableContract(node: ApplicableContract[_]): Unit =

col/src/main/java/vct/col/resolve/ctx/Referrable.scala

@@ -56,6 +56,8 @@ sealed trait Referrable[G] {
     case RefModelField(decl) => Referrable.originName(decl)
     case RefModelProcess(decl) => Referrable.originName(decl)
     case RefModelAction(decl) => Referrable.originName(decl)
+    case RefSeqProg(decl) => Referrable.originName(decl)
+    case RefVeyMontThread(decl) => Referrable.originName(decl)
     case BuiltinField(_) => ""
     case BuiltinInstanceMethod(_) => ""
     case RefPVLConstructor(decl) => ""
@@ -119,6 +121,8 @@ case object Referrable {
     case decl: CLocalDeclaration[G] => return decl.decl.inits.indices.map(RefCLocalDeclaration(decl, _))
     case decl: JavaLocalDeclaration[G] => return decl.decls.indices.map(RefJavaLocalDeclaration(decl, _))
     case decl: PVLConstructor[G] => RefPVLConstructor(decl)
+    case decl: VeyMontSeqProg[G] => RefSeqProg(decl)
+    case decl: VeyMontThread[G] => RefVeyMontThread(decl)
     case decl: JavaBipGlueContainer[G] => RefJavaBipGlueContainer()
   })
 
@@ -218,6 +222,9 @@ case class RefJavaBipStatePredicate[G](state: String, decl: JavaAnnotation[G]) e
 case class RefJavaBipGuard[G](decl: JavaMethod[G]) extends Referrable[G] with JavaNameTarget[G]
 case class RefJavaBipGlueContainer[G]() extends Referrable[G] // Bip glue jobs are not actually referrable
 
+case class RefSeqProg[G](decl: VeyMontSeqProg[G]) extends Referrable[G]
+case class RefVeyMontThread[G](decl: VeyMontThread[G]) extends Referrable[G] with PVLNameTarget[G]
+
 case class BuiltinField[G](f: Expr[G] => Expr[G]) extends Referrable[G] with SpecDerefTarget[G]
 case class BuiltinInstanceMethod[G](f: Expr[G] => Seq[Expr[G]] => Expr[G]) extends Referrable[G] with SpecInvocationTarget[G]
 

col/src/main/java/vct/col/typerules/CoercingRewriter.scala

@@ -841,10 +841,13 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
         CurPerm(loc)
       case CurrentThreadId() =>
         CurrentThreadId()
+      //case deref @ DerefVeyMontThread(ref) =>
+        //DerefVeyMontThread( TVeyMontThread[Pre](ref))
       case deref @ Deref(obj, ref) =>
         Deref(cls(obj), ref)(deref.blame)
       case deref @ DerefPointer(p) =>
         DerefPointer(pointer(p)._1)(deref.blame)
+      case deref @ DerefVeyMontThread(ref) => deref
       case div @ Div(left, right) =>
         firstOk(e, s"Expected both operands to be rational.",
           // PB: horrible hack: Div ends up being silver.PermDiv, which expects an integer divisor. In other cases,
@@ -1022,7 +1025,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
       case MatrixSum(indices, mat) =>
         MatrixSum(coerce(indices, TSeq[Pre](TInt())), coerce(mat, TSeq[Pre](TRational())))
       case inv @ MethodInvocation(obj, ref, args, outArgs, typeArgs, givenMap, yields) =>
-        MethodInvocation(cls(obj), ref, coerceArgs(args, ref.decl, typeArgs), outArgs, typeArgs, coerceGiven(givenMap), coerceYields(yields, inv))(inv.blame)
+        MethodInvocation(obj, ref, coerceArgs(args, ref.decl, typeArgs), outArgs, typeArgs, coerceGiven(givenMap), coerceYields(yields, inv))(inv.blame)
       case Minus(left, right) =>
         firstOk(e, s"Expected both operands to be numeric, but got ${left.t} and ${right.t}.",
           Minus(int(left), int(right)),
@@ -1265,6 +1268,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
         Then(value, post)
       case ThisModel(ref) =>
         ThisModel(ref)
+      case ThisSeqProg(ref) =>
+        ThisSeqProg(ref)
       case ThisObject(ref) =>
         ThisObject(ref)
       case TupGet(tup, index) =>
@@ -1318,6 +1323,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
         With(pre, value)
       case WritePerm() =>
         WritePerm()
+      case VeyMontCondition(c) => VeyMontCondition(c)
       case localIncoming: BipLocalIncomingData[Pre] => localIncoming
       case glue: JavaBipGlue[Pre] => glue
     }
@@ -1391,6 +1397,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
       case w @ Wait(obj) => Wait(cls(obj))(w.blame)
       case w @ WandApply(assn) => WandApply(res(assn))(w.blame)
       case w @ WandPackage(expr, stat) => WandPackage(res(expr), stat)(w.blame)
+      case VeyMontAssignExpression(t,a) => VeyMontAssignExpression(t,a)
+      case VeyMontCommExpression(r,s,a) => VeyMontCommExpression(r,s,a)
     }
   }
 
@@ -1493,6 +1501,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
           case JavaVariableDeclaration(name, dims, Some(v)) =>
             JavaVariableDeclaration(name, dims, Some(coerce(v, FuncTools.repeat[Type[Pre]](TArray(_), dims, declaration.t))))
         })
+      case seqProg: VeyMontSeqProg[Pre] => seqProg
+      case thread: VeyMontThread[Pre] => thread
       case bc: BipComponent[Pre] =>
         new BipComponent(bc.fqn, bc.constructors, res(bc.invariant), bc.initial)
       case bsp: BipStatePredicate[Pre] =>