val atomic_exchange_statement_computation
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (old_val target new_val: expression_t)
      (s: Armada.State.t)
    : GTot (conditional_computation_t Armada.State.t)
val atomic_exchange_statement_computation
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (old_val target new_val: expression_t)
      (s: Armada.State.t)
    : GTot (conditional_computation_t Armada.State.t)
let atomic_exchange_statement_computation
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (old_val: expression_t)
  (target: expression_t)
  (new_val: expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || neqb (expression_to_td target) (expression_to_td old_val)
     || neqb (expression_to_td target) (expression_to_td new_val) then
     ComputationImpossible
  else (
    // pre-update
    let? _ = check_expression_up_to_date_for_rmw target actor s in
    let? target_value = rvalue_computation target actor s in
    let? new_value = rvalue_computation new_val actor s in
    let? old_ptr = lvalue_computation old_val actor s in
    let? target_ptr = lvalue_computation target actor s in
    // post-update
    let? s' = update_pointed_to_value old_ptr actor start_pc 0 false target_value s in
    update_pointed_to_value target_ptr actor start_pc 1 false new_value s'
  )
module Armada.Statement

open Armada.Base
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.State
open Armada.Thread
open Armada.Threads
open Armada.Type
open FStar.Sequence.Base
open Spec.List
open Spec.Map
open Spec.Ubool

noeq type t =
  | AssumeExpressionStatement: (exp: expression_t) -> t
  | AssumePredicateStatement: (pred: Armada.State.t -> GTot bool) -> t
  | AssertTrueStatement: (exp: expression_t) -> t
  | AssertFalseStatement: (exp: expression_t) -> t
  | ConditionalJumpStatement: (cond: expression_t) -> t // if or while
  | UnconditionalJumpStatement: t // skip, jump past else, jump back to loop head, break, continue, goto, if *, while *
  | UpdateStatement: (bypassing_write_buffer: bool) -> // whether ::= is used
                     (dst: expression_t) -> (src: expression_t) -> t
  | NondeterministicUpdateStatement: (bypassing_write_buffer: bool) -> // whether ::= is used
                                     (dst: expression_t) -> t
  | PropagateWriteMessageStatement: t
  | CompareAndSwapStatement: (target: expression_t) ->  // the location to compare to and possibly store into
                             (old_val: expression_t) -> // the value to compare the current value to
                             (new_val: expression_t) -> // the value to swap in if the equality comparison succeeds
                             (bypassing_write_buffer: bool) -> // whether ::= is used for assigning optional_result
                             (optional_result: option expression_t) -> t // where to write the boolean "did swap happen?"
  | AtomicExchangeStatement: (old_val: expression_t) -> // where the old value of target will be put
                             (target: expression_t) ->  // where the new value should be assigned to 
                             (new_val: expression_t) -> t // the new value
                             // e.g., x := atomic_exchange(y, 3) has old_val x, target y, and new_val 3,
                             // and means to atomically set x := y then y := 3
  | CreateThreadStatement: (method_id: method_id_t) ->
                           (initial_pc: pc_t) ->              // initial PC of created thread
                           (bypassing_write_buffer: bool) ->  // whether ::= is used for assigning the new thread ID
                           (optional_result: option expression_t) -> // where the resulting thread ID should be
                                                                    // written (optional)
                           (parameter_var_ids: list var_id_t) ->  // local variables to store parameters
                                                                 // (assumed strongly consistent)
                           (parameter_expressions: list expression_t) -> // expressions to be stored as parameters
                           (local_variable_initializers: list initializer_t) ->  t
  | MethodCallStatement: (method_id: method_id_t) ->
                         (return_pc: pc_t) ->
                         (parameter_var_ids: list var_id_t) -> // local variables to store parameters
                                                              // (assumed strongly consistent)
                         (parameter_expressions: list expression_t) -> // expressions to be stored as parameters
                         (local_variable_initializers: list initializer_t) ->
                            // If this is an external method, there should be one local variable initializer for
                            // each reads clause. The types of these initializers should match the types of those
                            // reads clauses, in order. So, for instance if it has "reads p[3], x" and the types of
                            // p[3] and x are t1 and t2, then the local variable initializers should be a list
                            // whose first element is an initializer with type t1 and whose second element is
                            // an initializer of type t2.
                         (stack_overflow: bool) -> t
  | ReturnStatement: (method_id: method_id_t) ->
                     (bypassing_write_buffer: bool) ->   // whether ::= is used for assigning output variables
                     (output_dsts: list expression_t) ->
                     (output_srcs: list expression_t) -> // output sources to be evaluated before popping the stack;
                                                        // generally, each of these will be an ExpressionLocalVariable
                                                        // corresponding to an output stack variable
                     t
  | TerminateThreadStatement: (method_id: method_id_t) -> t  // top-level method being returned from
  | TerminateProcessStatement: (method_id: method_id_t) -> t // main method ID being returned from
  | JoinStatement: (join_tid: expression_t) -> t // in concrete levels, this expression shouldn't read shared state
  | MallocSuccessfulStatement: (bypassing_write_buffer: bool) -> // whether ::= is used to write the resulting pointer
                               (result: expression_t) ->         // where the resulting pointer is written
                               (allocation_td: object_td_t) ->   // type being allocated
                               (count: expression_t) ->          // count must be a nat
                               t
  | MallocReturningNullStatement: (bypassing_write_buffer: bool) -> (result: expression_t) -> (count: expression_t) -> t
  | CallocSuccessfulStatement: (bypassing_write_buffer: bool) -> (result: expression_t) -> // result must be a pointer
                               (allocation_td: object_td_t) -> (count: expression_t) ->    // count must be a nat
                               t
  | CallocReturningNullStatement: (bypassing_write_buffer: bool) ->
                                  (result: expression_t) -> // result must be a pointer
                                  (count: expression_t) ->  // count must be a nat
                                  t
  | DeallocStatement: (ptr: expression_t) -> t
  | SomehowStatement: (undefined_unless_cond: expression_t) -> // undefined_unless conditions combined with &&
                      (bypassing_write_buffer: bool) ->        // whether updates to modifies clauses
                                                              //   bypass write buffers
                      (modifies_clauses: list expression_t) ->
                      (ensures_cond: expression_t) ->          // ensures conditions combined with &&
                      t
  | FenceStatement: t
  | ExternalMethodStartStatement: (await_cond: expression_t) ->            // awaits conditions combined with &&
                                  (undefined_unless_cond: expression_t) -> // undefined_unless conditions
                                                                          //   combined with &&
                                  (bypassing_write_buffer: bool) ->        // whether havocs of modifies clauses
                                                                          //   bypass write buffer
                                  (modifies_clauses: list expression_t) -> // modifies clauses to havoc
                                  (reads_clauses: list (var_id_t * expression_t)) -> // reads clauses to snapshot
                                  t
  | ExternalMethodMiddleStatement: (bypassing_write_buffer: bool) ->        // whether havocs of modifies clauses
                                                                           //   bypass write buffer
                                   (modifies_clauses: list expression_t) -> // modifies clauses to havoc
                                   (reads_clauses: list (var_id_t * expression_t)) -> // reads clauses to snapshot
                                   t
  | ExternalMethodEndStatement: (ensures_cond: expression_t) ->             // ensures clauses combined with &&
                                (logs_clauses: list expression_t) ->        // values to be appended to
                                                                           //   external-event trace
                                t

let assume_expression_statement_computation
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || neqb (expression_to_td exp) (ObjectTDAbstract bool) then
     ComputationImpossible
  else (
    let? value = rvalue_computation exp actor s in
    if ObjectValueAbstract?.value value <> true then
      ComputationImpossible
    else
      return s
  )

let assume_predicate_statement_computation
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (pred: Armada.State.t -> GTot bool)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || not (pred s) then
    ComputationImpossible
  else
    return s

let assert_true_statement_computation
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || neqb (expression_to_td exp) (ObjectTDAbstract bool) then
     ComputationImpossible
  else (
    let? value = rvalue_computation exp actor s in
    if ObjectValueAbstract?.value value <> true then
      ComputationImpossible
    else
      return s
  )

let assert_false_statement_computation
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || neqb (expression_to_td exp) (ObjectTDAbstract bool) then
     ComputationImpossible
  else (
    let? value = rvalue_computation exp actor s in
    if ObjectValueAbstract?.value value <> false then
      ComputationImpossible
    else
      let s' = { s with stop_reason = StopReasonAssertionFailure } in
      return s'
  )

let conditional_jump_statement_computation
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || neqb (expression_to_td exp) (ObjectTDAbstract bool) then
    ComputationImpossible
  else (
    let? value = rvalue_computation exp actor s in
    if ObjectValueAbstract?.value value <> true then
      ComputationImpossible
    else
      return s
  )

let unconditional_jump_statement_computation
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if Cons? nd then
    ComputationImpossible
  else
    return s

let update_statement_computation
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (bypassing_write_buffer: bool)
  (dst: expression_t)
  (src: expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || neqb (expression_to_td dst) (expression_to_td src) then
    ComputationImpossible
  else (
    let? src_value = rvalue_computation src actor s in
    update_expression dst actor start_pc 0 bypassing_write_buffer src_value s
  )

let nondeterministic_update_statement_computation
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (bypassing_write_buffer: bool)
  (dst: expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   list_len nd <> 1
     || neqb (object_value_to_td (Cons?.hd nd)) (expression_to_td dst) then
    ComputationImpossible
  else (
    let nd_value = Cons?.hd nd in
    if not (object_value_has_all_pointers_uninitialized nd_value) then
      ComputationImpossible
    else
      update_expression dst actor start_pc 0 bypassing_write_buffer nd_value s
  )

let propagate_write_message_statement_computation
  (actor: tid_t)
  (nd: nondeterminism_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   list_len nd <> 1
     || neqb (object_value_to_td (Cons?.hd nd)) (ObjectTDAbstract tid_t) then
    ComputationImpossible
  else
    let receiver_tid: tid_t = ObjectValueAbstract?.value (Cons?.hd nd) in
    if receiver_tid = actor then // can't propagate to the same thread
      ComputationImpossible
    else
      let propagator_thread = s.threads actor in
      let receiver_thread = s.threads receiver_tid in
      let which_message = receiver_thread.position_in_other_write_buffers actor in
      if which_message >= length propagator_thread.write_buffer then
        ComputationImpossible
      else
        let write_message = index propagator_thread.write_buffer which_message in
        let position_in_other_write_buffers' =
          Spec.Map.upd receiver_thread.position_in_other_write_buffers actor (which_message + 1) in
        let receiver_thread' =
          { receiver_thread with position_in_other_write_buffers = position_in_other_write_buffers' } in
        let threads' = Spec.Map.upd s.threads receiver_tid receiver_thread' in
        match propagate_write_message write_message receiver_tid s.mem with
        | ComputationImpossible
        | ComputationUndefined ->
            // If propagate would trigger undefined behavior (e.g., by propagating to freed memory),
            // it just leaves memory unchanged.
            return ({ s with threads = threads'; })
        | ComputationProduces mem' ->
            return ({ s with mem = mem'; threads = threads'; })

let compare_and_swap_statement_computation
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (target: expression_t)
  (old_val: expression_t)
  (new_val: expression_t)
  (bypassing_write_buffer: bool)
  (optional_result: option expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || neqb (expression_to_td target) (expression_to_td old_val)
     || neqb (expression_to_td target) (expression_to_td new_val)
     || (match optional_result with
        | Some result -> neqb (expression_to_td result) (ObjectTDPrimitive PrimitiveTDBool)
        | None -> false) then
    ComputationImpossible
  else (
    let? _ = check_expression_up_to_date_for_rmw target actor s in
    let? old_value = rvalue_computation old_val actor s in
    let? target_value = rvalue_computation target actor s in
    let? new_value = rvalue_computation new_val actor s in
    let? target_ptr = lvalue_computation target actor s in
    let swap = eqb target_value old_value in
    let? s' = (if swap then update_pointed_to_value target_ptr actor start_pc 0 false new_value s else return s) in
    match optional_result with
    | None -> return s'
    | Some result ->
        // this line is deceptive, and we might be potentially bitten by it later
        // but it simplify the control flow
        let? result_ptr = lvalue_computation result actor s in
        let swap_value = ObjectValuePrimitive (PrimitiveBoxBool swap) in
        update_pointed_to_value result_ptr actor start_pc 1 bypassing_write_buffer swap_value s'
  )
/
Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Threads.fst.checked Armada.Thread.fst.checked Armada.State.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked
Armada.Statement.fst

    actor: Armada.Base.tid_t ->
    nd: Armada.Type.nondeterminism_t ->
    start_pc: Armada.Base.pc_t ->
    old_val: Armada.Expression.expression_t ->
    target: Armada.Expression.expression_t ->
    new_val: Armada.Expression.expression_t ->
    s: Armada.State.t
  -> Prims.GTot (Armada.Computation.conditional_computation_t Armada.State.t)
Armada.Base.tid_t Armada.Type.nondeterminism_t Armada.Base.pc_t Armada.Expression.expression_t Armada.State.t Prims.op_BarBar Prims.uu___is_Cons Armada.Type.object_value_t Spec.Ubool.neqb Armada.Type.object_td_t Armada.Expression.expression_to_td Armada.Computation.ComputationImpossible Prims.bool Armada.Computation.op_let_Question Prims.unit Armada.Expression.check_expression_up_to_date_for_rmw Armada.Type.valid_object_value_t Armada.Expression.rvalue_computation Armada.Pointer.t Armada.Expression.lvalue_computation Armada.Expression.update_pointed_to_value Armada.Computation.conditional_computation_t
let atomic_exchange_statement_computation
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (old_val target new_val: expression_t)
      (s: Armada.State.t)
    : GTot (conditional_computation_t Armada.State.t) =
  
if
  Cons? nd || neqb (expression_to_td target) (expression_to_td old_val) ||
  neqb (expression_to_td target) (expression_to_td new_val)
then ComputationImpossible
else
  (let? _ = check_expression_up_to_date_for_rmw target actor s in
    let? target_value = rvalue_computation target actor s in
    let? new_value = rvalue_computation new_val actor s in
    let? old_ptr = lvalue_computation old_val actor s in
    let? target_ptr = lvalue_computation target actor s in
    let? s' = update_pointed_to_value old_ptr actor start_pc 0 false target_value s in
    update_pointed_to_value target_ptr actor start_pc 1 false new_value s')