Merge pull request #1208 from utwente-fmt/rasi_generator

Rasi generator

src/main/vct/main/stages/GenerateRASI.scala

@@ -1,10 +1,10 @@
 package vct.main.stages
 
 import hre.stages.Stage
-import vct.col.ast.{InstanceField, InstanceMethod, Node}
+import vct.col.ast.{InstanceField, InstanceMethod, InstancePredicate, Node}
 import vct.col.rewrite.Generation
 import vct.options.Options
-import vct.rewrite.rasi.{ConcreteVariable, FieldVariable, IndexedVariable, RASIGenerator}
+import vct.rewrite.rasi.{ConcreteVariable, FieldVariable, IndexedVariable, RASIGenerator, SizeVariable}
 
 import java.nio.file.Path
 
@@ -24,10 +24,15 @@ case class GenerateRASI(vars: Option[Seq[String]], out: Path) extends Stage[Node
     val in = in1.asInstanceOf[Node[Generation]]
     val main_method = in.transSubnodes.collectFirst{ case m: InstanceMethod[_] if m.o.getPreferredName.get.snake.equals("main") => m }.get
     val variables: Set[ConcreteVariable[Generation]] = vars.getOrElse(Seq()).map(s => resolve_variable(in, s)).toSet
-    RASIGenerator().test(main_method, variables, out)
+    val parameter_invariant: InstancePredicate[Generation] = get_parameter_invariant(in)
+    new RASIGenerator().test(main_method, variables, parameter_invariant, out)
   }
 
   private def resolve_variable(in: Node[Generation], name: String): ConcreteVariable[Generation] = {
+    if (name.contains("|")) {
+      val var_name = name.substring(1, name.length - 1)
+      return SizeVariable(in.transSubnodes.collectFirst{ case f: InstanceField[_] if f.o.getPreferredName.get.snake.equals(var_name) => f }.get)
+    }
     val name_len = name.indexOf("[")
     val var_name = if (name_len == -1) name else name.substring(0, name_len)
     val index: Option[Integer] = if (name_len == -1) None else Some(Integer.valueOf(name.substring(name_len + 1, name.length - 1)))
@@ -37,4 +42,8 @@ case class GenerateRASI(vars: Option[Seq[String]], out: Path) extends Stage[Node
       case None => FieldVariable(instance_field)
     }
   }
+
+  private def get_parameter_invariant(in: Node[Generation]): InstancePredicate[Generation] = {
+    in.transSubnodes.collectFirst{ case p: InstancePredicate[_] if p.o.getPreferredName.get.snake.equals("parameter_invariant") => p }.get
+  }
 }

src/parsers/vct/parsers/transform/systemctocol/engine/MainTransformer.java

@@ -1007,8 +1007,12 @@ private Statement<T> create_scheduler_body() {
             joins.add(new Join<>(proc_deref, new GeneratedBlame<>(), OriGen.create()));
         }
 
+        java.util.List<Statement<T>> body = new java.util.ArrayList<>();
+
         // Add forks to method body
-        java.util.List<Statement<T>> body = new java.util.ArrayList<>(forks);
+        body.add(new Lock<>(col_system.THIS, new GeneratedBlame<>(), OriGen.create()));
+        body.addAll(forks);
+        body.add(new Unlock<>(col_system.THIS, new GeneratedBlame<>(), OriGen.create()));
 
         // Add scheduler loop to method body
         Statement<T> loop_body = create_scheduler_loop_body();

src/rewrite/vct/rewrite/cfg/CFGGenerator.scala

@@ -1,16 +1,20 @@
 package vct.rewrite.cfg
 
+import com.typesafe.scalalogging.LazyLogging
 import vct.col.ast._
 
 import scala.collection.mutable
 
-case class CFGGenerator[G]() {
+case class CFGGenerator[G]() extends LazyLogging {
   private val found_labels: mutable.Map[LabelDecl[G], CFGNode[G]] = mutable.HashMap[LabelDecl[G], CFGNode[G]]()
   private val searched_labels: mutable.Map[LabelDecl[G], mutable.Set[CFGNode[G]]] = mutable.HashMap[LabelDecl[G], mutable.Set[CFGNode[G]]]()
   private val converted_nodes: mutable.Map[GlobalIndex[G], CFGNode[G]] = mutable.HashMap[GlobalIndex[G], CFGNode[G]]()
 
   def generate(entry: InstanceMethod[G]): CFGNode[G] = {
-    convert(entry.body.get, GlobalIndex[G](mutable.Seq(InitialIndex(entry))))
+    logger.info("Generating control flow graph")
+    val res = convert(entry.body.get, GlobalIndex[G](mutable.Seq(InitialIndex(entry))))
+    logger.info("Control flow graph generation complete")
+    res
   }
 
   private def convert(node: Statement[G], context: GlobalIndex[G]): CFGNode[G] = {

src/rewrite/vct/rewrite/rasi/AbstractProcess.scala

@@ -5,33 +5,48 @@ import vct.rewrite.cfg.{CFGEdge, CFGEntry, CFGNode, CFGTerminal}
 
 import scala.collection.mutable
 
+
+// TODO: Can only one thread per class instance be launched?
 case class AbstractProcess[G](obj: Expr[G]) {
 
   /**
    * Simulates an atomic execution step for this process on the given abstract state.
    *
    * @param starting_state Abstract starting state
-   * @return A set of all successor states
+   * @return A description of all reachable post-states
    */
-  def atomic_step(starting_state: AbstractState[G]): Set[AbstractState[G]] = {
-    var (atomic, states): (Boolean, Set[AbstractState[G]]) = small_step(starting_state.processes(this), starting_state)
-    while (atomic) {
-      val next: Set[(Boolean, Set[AbstractState[G]])] = states.map(s => small_step_if_atomic(s))
-      states = next.flatMap(t => t._2)
-      atomic = next.exists(t => t._1)
+  def atomic_step(starting_state: AbstractState[G]): RASISuccessor[G] = {
+    val (atomic, successor): (Boolean, RASISuccessor[G]) = small_step(starting_state.processes(this), starting_state)
+
+    var end_states: Set[AbstractState[G]] = if (!atomic) successor.successors else Set.empty[AbstractState[G]]
+    var intermediate: Set[AbstractState[G]] = if (atomic) successor.successors else Set.empty[AbstractState[G]]
+    var explored: Set[AbstractState[G]] = intermediate
+
+    var variables: Set[ConcreteVariable[G]] = successor.deciding_variables
+
+    while (intermediate.nonEmpty) {
+      val next: Set[(Boolean, RASISuccessor[G])] = intermediate.map(s => small_step_if_atomic(s, starting_state))
+
+      variables ++= next.map(s => s._2).flatMap(s => s.deciding_variables)
+      end_states ++= next.filter(s => !s._1).map(s => s._2).flatMap(s => s.successors)
+      intermediate = next.filter(s => s._1).map(s => s._2).flatMap(s => s.successors).diff(explored)
+      explored ++= intermediate
     }
-    states
+
+    RASISuccessor(variables, end_states)
   }
 
   /**
    * Tests if another small step can be executed without breaking the current atomic block, and if so, executes the next
    * small step.
    *
    * @param state Current abstract state
-   * @return A tuple of a boolean indicating whether atomic progress could be made and a set of all successor states
+   * @param initial_state State before the atomic step
+   * @return A tuple of a boolean indicating if atomic progress could be made and a descriptor of all successor states
    */
-  private def small_step_if_atomic(state: AbstractState[G]): (Boolean, Set[AbstractState[G]]) = {
-    if (!state.processes.contains(this) || !is_atomic(state.processes(this))) (false, Set(state))
+  private def small_step_if_atomic(state: AbstractState[G], initial_state: AbstractState[G]): (Boolean, RASISuccessor[G]) = {
+    val vars_changed: Boolean = state.valuations != initial_state.valuations
+    if (!state.processes.contains(this) || (vars_changed && !is_atomic(state.processes(this)))) (false, RASISuccessor(Set(), Set(state)))
     else small_step(state.processes(this), state)
   }
 
@@ -41,75 +56,104 @@ case class AbstractProcess[G](obj: Expr[G]) {
    *
    * @param node CFG node to simulate
    * @param state Current abstract state
-   * @return A tuple of a boolean indicating whether progress was made and a set of all successor states.
+   * @return A tuple of a boolean indicating whether progress was made and a descriptor of all successor states
    */
-  private def small_step(node: CFGEntry[G], state: AbstractState[G]): (Boolean, Set[AbstractState[G]]) = node match {
-    case CFGTerminal() => (false, Set(state.without_process(this)))
+  private def small_step(node: CFGEntry[G], state: AbstractState[G]): (Boolean, RASISuccessor[G]) = node match {
+    case CFGTerminal() => (false, RASISuccessor(Set(), Set(state.without_process(this))))
     case CFGNode(n, succ) => n match {
       // Assign statements change the state of variables directly (if they appear in the valuation)
       case Assign(target, value) => (true, target.t match {
-        case _: IntType[_] | TBool() => viable_edges(succ, state).map(e => take_edge(e, state.with_valuation(target, state.resolve_expression(value))))
-        case _: TSeq[_] => viable_edges(succ, state).map(e => take_edge(e, state.with_updated_collection(target, value)))   // TODO: Consider arrays
-        case _ => viable_edges(succ, state).map(e => take_edge(e, state))
+        case _: IntType[_] | TBool() => take_viable_edges(succ, state, RASISuccessor(Set(), Set(state.with_valuation(target, state.resolve_expression(value)))))
+        case _: TSeq[_] => take_viable_edges(succ, state, RASISuccessor(Set(), Set(state.with_updated_collection(target, value))))   // TODO: Consider arrays
+        case _ => take_viable_edges_from_state(succ, state)
       })
-      case Havoc(loc) => (true, viable_edges(succ, state).map(e => take_edge(e, state.with_valuation(loc, UncertainValue.uncertain_of(loc.t)))))
+      case Havoc(loc) => (true, take_viable_edges(succ, state, RASISuccessor(Set(), Set(state.with_valuation(loc, UncertainValue.uncertain_of(loc.t))))))
       // Statements that induce assumptions about the state, such as assume, inhale, or a method's postcondition, might change the state implicitly
-      case Assume(assn) => (true, viable_edges(succ, state).flatMap(e => state.with_assumption(assn).map(s => take_edge(e, s))))
-      case Inhale(res) => (true, viable_edges(succ, state).flatMap(e => state.with_assumption(res).map(s => take_edge(e, s))))
+      case Assume(assn) => (true, take_viable_edges(succ, state, state.with_assumption(assn)))
+      case Inhale(res) => (true, take_viable_edges(succ, state, state.with_assumption(res)))
       // Abstract procedures, constructors and methods are defined by their postconditions      TODO: Handle local variables
       case InvokeProcedure(ref, args, _, _, _, _) => (true, ref.decl.body match {
-        case Some(_) => viable_edges(succ, state).map(e => take_edge(e, state))
-        case None => viable_edges(succ, state).flatMap(e => state.with_postcondition(ref.decl.contract.ensures, Map.from(ref.decl.args.zip(args))).map(s => take_edge(e, s)))
+        case Some(_) => take_viable_edges_from_state(succ, state)
+        case None => take_viable_edges(succ, state, state.with_postcondition(ref.decl.contract.ensures, Map.from(ref.decl.args.zip(args))))
       })
-      case InvokeConstructor(ref, _, _, args, _, _, _, _) => (true, ref.decl.body match {
-        case Some(_) => viable_edges(succ, state).map(e => take_edge(e, state))
-        case None => viable_edges(succ, state).flatMap(e => state.with_postcondition(ref.decl.contract.ensures, Map.from(ref.decl.args.zip(args))).map(s => take_edge(e, s)))
+      case InvokeConstructor(ref, _, args, _, _, _, _, _) => (true, ref.decl.body match {
+        case Some(_) => take_viable_edges_from_state(succ, state)
+        case None => take_viable_edges(succ, state, state.with_postcondition(ref.decl.contract.ensures, Map.from(ref.decl.args.zip(args))))
       })
       case InvokeMethod(_, ref, args, _, _, _, _) => (true, ref.decl.body match {
-        case Some(_) => viable_edges(succ, state).map(e => take_edge(e, state))
-        case None => viable_edges(succ, state).flatMap(e => state.with_postcondition(ref.decl.contract.ensures, Map.from(ref.decl.args.zip(args))).map(s => take_edge(e, s)))
+        case Some(_) => take_viable_edges_from_state(succ, state)
+        case None => take_viable_edges(succ, state, state.with_postcondition(ref.decl.contract.ensures, Map.from(ref.decl.args.zip(args))))
       })
       // TODO: Handle local variables
-      case Return(result) => (true, viable_edges(succ, state).map(e => take_edge(e, state)))
+      case Return(result) => (true, take_viable_edges_from_state(succ, state))
       // TODO: What do wait and notify do?
-      case Wait(obj) => (true, viable_edges(succ, state).map(e => take_edge(e, state)))
-      case Notify(obj) => (true, viable_edges(succ, state).map(e => take_edge(e, state)))
+      case Wait(obj) => (true, take_viable_edges_from_state(succ, state))
+      case Notify(obj) => (true, take_viable_edges_from_state(succ, state))
       // Lock and Unlock manipulate the global lock and are potentially blocking      TODO: Differentiate between locks!
       case Lock(_) => state.lock match {
-        case Some(proc) => if (!proc.equals(this)) (false, Set(state))
+        case Some(proc) => if (!proc.equals(this)) (false, RASISuccessor(Set(), Set(state)))
                            else throw new IllegalStateException("Trying to lock already acquired lock")
-        case None => (true, viable_edges(succ, state).map(e => take_edge(e, state).locked_by(this)))
+        case None => (true, take_viable_edges(succ, state, RASISuccessor(Set(), Set(state.locked_by(this)))))
       }
-      case Unlock(_) => state.lock match {    // TODO: Progress was made, but this is still false to allow other processes to execute
-        case Some(proc) => if (proc.equals(this)) (false, viable_edges(succ, state).map(e => take_edge(e, state).unlocked()))
+      case Unlock(_) => state.lock match {    // Progress was made, but the atomic flag is still false to allow other processes to execute
+        case Some(proc) => if (proc.equals(this)) (false, take_viable_edges(succ, state, RASISuccessor(Set(), Set(state.unlocked()))))
                            else throw new IllegalStateException("Trying to unlock lock owned by other process")
         case None => throw new IllegalStateException("Trying to unlock unlocked lock")
       }
       // When forking a new process, make the step of creating it simultaneously to the normal steps
       case Fork(obj) =>
-        val edges: (Set[CFGEdge[G]], Set[CFGEdge[G]]) = viable_edges(succ, state).partition(e => e.target match {
+        val edges: (mutable.Set[CFGEdge[G]], mutable.Set[CFGEdge[G]]) = succ.partition(e => e.target match {
           case CFGTerminal() => false
           case CFGNode(t, _) => t.equals(obj.t.asClass.get.cls.decl.declarations.collect{ case r: RunMethod[G] => r }.head.body.get)
         })
-        (true, edges._2.map(e => take_edge(e, state.with_process_at(AbstractProcess(obj), edges._1.head.target))))    // TODO: Can only one thread per class instance be launched?
+        val relevant: Boolean = edges._1.size == 1 && (edges._1.head.target match {
+          case CFGTerminal() => false
+          case target: CFGNode[G] => new StaticScanner(target, state).scan_can_change_variables()
+        })
+        (true, take_viable_edges(edges._2, state, RASISuccessor(Set(), Set(if (relevant) state.with_process_at(AbstractProcess(obj), edges._1.head.target) else state))))
       case Join(obj) =>
-        if (state.processes.keys.forall(p => p.obj != obj)) (true, viable_edges(succ, state).map(e => take_edge(e, state)))
-        else (false, Set(state))
+        if (state.processes.keys.forall(p => p.obj != obj)) (true, take_viable_edges_from_state(succ, state))
+        else (false, RASISuccessor(Set(), Set(state)))
       // Everything else does not affect the state, so simply go to the next step
-      case _ => (true, viable_edges(succ, state).map(e => take_edge(e, state)))
+      case _ => (true, take_viable_edges_from_state(succ, state))
     }
   }
 
   /**
-   * Filters out CFG edges from a given set based on whether they would be viable in the given abstract state.
+   * Helper function for <code>take_viable_edges</code> if there is no other change to the state.
+   */
+  private def take_viable_edges_from_state(edges: mutable.Set[CFGEdge[G]], state: AbstractState[G]): RASISuccessor[G] =
+    take_viable_edges(edges, state, RASISuccessor(Set(), Set(state)))
+  /**
+   * Returns a successor object representing all states reachable in one state from the given starting state with the
+   * given control flow graph edges.
+   *
+   * @param edges Edges that are possible to take (might not be enabled)
+   * @param starting_state Starting state for the step
+   * @param new_states A descriptor containing possible initial states for the transition, in case another operation has
+   *                   been conducted on <code>starting_state</code>, e.g. changed variable valuations
+   * @return A successor object that contains all possible successor states
+   */
+  private def take_viable_edges(edges: mutable.Set[CFGEdge[G]], starting_state: AbstractState[G], new_states: RASISuccessor[G]): RASISuccessor[G] = {
+    val enabled_edges: (Set[CFGEdge[G]], Set[ConcreteVariable[G]]) = viable_edges(edges, starting_state)
+    RASISuccessor(new_states.deciding_variables ++ enabled_edges._2, enabled_edges._1.flatMap(e => new_states.successors.map(s => take_edge(e, s))))
+  }
+
+  /**
+   * Filters out CFG edges from a given set based on whether they would be viable in the given abstract state. Also
+   * returns the set of variables that can cause nondeterministic overapproximation in this step.
    *
    * @param edges A set of CFG edges
    * @param state Current abstract state
-   * @return A set of those entries of <code>edges</code> whose conditions could evaluate to <code>true</code> in the
-   *         given abstract state
+   * @return A tuple with a set of those entries of <code>edges</code> whose conditions could evaluate to
+   *         <code>true</code> in the given <code>state</code> and a set of variables that caused overapproximation in
+   *         this step
    */
-  private def viable_edges(edges: mutable.Set[CFGEdge[G]], state: AbstractState[G]): Set[CFGEdge[G]] =
-    edges.filter(e => e.condition.isEmpty || state.resolve_boolean_expression(e.condition.get).can_be_true).toSet
+  private def viable_edges(edges: mutable.Set[CFGEdge[G]], state: AbstractState[G]): (Set[CFGEdge[G]], Set[ConcreteVariable[G]]) = {
+    val viable: Set[CFGEdge[G]] = edges.filter(e => e.condition.isEmpty || state.resolve_boolean_expression(e.condition.get).can_be_true).toSet
+    val variables: Set[ConcreteVariable[G]] = new VariableSelector(state).deciding_variables(viable.map(e => e.condition))
+    (viable, variables)
+  }
 
   /**
    * Returns the abstract state that results in this process taking a transition in the CFG.
@@ -119,7 +163,7 @@ case class AbstractProcess[G](obj: Expr[G]) {
    * @return Copy of <code>state</code> with this process at the target node of the CFG transition
    */
   private def take_edge(edge: CFGEdge[G], state: AbstractState[G]): AbstractState[G] =
-    state.with_process_at(this, edge.target)
+    state.with_process_at(this, edge.target).with_condition(edge.condition)
 
   /**
    * Checks whether the considered block is still atomic when adding the next node.