val lvalue_computation (exp: expression_t) (actor: tid_t) (s: Armada.State.t)
    : GTot (conditional_computation_t Armada.Pointer.t)
val lvalue_computation (exp: expression_t) (actor: tid_t) (s: Armada.State.t)
    : GTot (conditional_computation_t Armada.Pointer.t)
let rec rvalue_computation
  (exp: expression_t)
  (actor: tid_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t (valid_object_value_t (expression_to_td exp)))
  (decreases exp) =
  if not (expression_valid exp) then
    ComputationImpossible
  else
    match exp with
    | ExpressionConstant value -> return value
    | ExpressionGlobalVariable td var_id ->
        dereference_as_td_computation (PointerRoot (RootIdGlobal var_id)) td actor s.mem
    | ExpressionLocalVariable td var_id ->
        let thread = s.threads actor in
        if not (list_contains var_id thread.top.local_variables) then
          ComputationImpossible
        else
          dereference_as_td_computation
            (PointerRoot (RootIdStack actor thread.top.method_id thread.top.frame_uniq var_id)) td actor s.mem
    | ExpressionUnaryOperator operand_td result_td operator operand ->
        let? operand_value = rvalue_computation operand actor s in
        eval_unary_op operator operand_value
    | ExpressionBinaryOperator operand_td1 operand_td2 result_td operator operand1 operand2 ->
        let? operand_value1 = rvalue_computation operand1 actor s in
        let? operand_value2 = rvalue_computation operand2 actor s in
        eval_binary_op operator operand_value1 operand_value2
    | ExpressionIf td cond operand_then operand_else ->
        let? cond_value = rvalue_computation cond actor s in
        let? operand_then_value = rvalue_computation operand_then actor s in
        let? operand_else_value = rvalue_computation operand_else actor s in
        let b = PrimitiveBoxBool?.b (ObjectValuePrimitive?.value cond_value) in
        (ComputationProduces (if b then operand_then_value else operand_else_value))
    | ExpressionDereference td ptr ->
        let? ptr_value = rvalue_computation ptr actor s in
        let p = PrimitiveBoxPointer?.ptr (ObjectValuePrimitive?.value ptr_value) in
        dereference_as_td_computation p td actor s.mem
    | ExpressionAddressOf obj ->
        let? p = lvalue_computation obj actor s in
        return (ObjectValuePrimitive (PrimitiveBoxPointer p) <: valid_object_value_t (expression_to_td exp))
    | ExpressionPointerOffset ptr offset ->
        let? ptr_value = rvalue_computation ptr actor s in
        let? offset_value = rvalue_computation offset actor s in
        let p = PrimitiveBoxPointer?.ptr (ObjectValuePrimitive?.value ptr_value) in
        // It's undefined behavior to offset a pointer that doesn't point into an array,
        // or to offset outside of the array, except exactly one past the end of the array
        // (idx == array_len).  This is part of C semantics:  As described in
        // https://en.cppreference.com/w/cpp/language/operator_arithmetic, "Any
        // other situations (that is, attempts to generate a pointer that isn't pointing
        // at an element of the same array or one past the end) invoke undefined
        // behavior."
        (match p with
         | PointerIndex array_ptr idx ->
             let offset_int = ObjectValueAbstract?.value offset_value in
             let? array_value = dereference_computation array_ptr s.mem in
             (match array_value with
              | ObjectStorageArray _ elements ->
                  let new_idx: int = (idx <: int) + offset_int in
                  // It's OK to be equal to `length elements` (one past the end), but not OK to be any higher
                  if new_idx < 0 || new_idx > length elements then
                    ComputationUndefined
                  else
                    let p' = PointerIndex array_ptr new_idx in
                    let obj = ObjectValuePrimitive (PrimitiveBoxPointer p') in
                    return (obj <: valid_object_value_t (expression_to_td exp))
              | _ -> ComputationUndefined)
         | _ -> ComputationUndefined)
    | ExpressionFieldOf td obj field_id ->
        let? obj_ptr = lvalue_computation obj actor s in
        dereference_as_td_computation (PointerField obj_ptr field_id) td actor s.mem
    | ExpressionAllocated ptr ->
        let? ptr_value = rvalue_computation ptr actor s in
        let p = PrimitiveBoxPointer?.ptr (ObjectValuePrimitive?.value ptr_value) in
        return (ObjectValuePrimitive (PrimitiveBoxBool (p <> PointerUninitialized))
                <: valid_object_value_t (expression_to_td exp))
    | ExpressionApplyFunction td operands return_type operand_types fn ->
        let? operand_values = rvalues_computation operands actor s in
        let? value = apply_function_to_operands operand_values return_type operand_types fn in
        let v: valid_object_value_t td = ObjectValueAbstract return_type value in
        return v
    | ExpressionIfUndefined td potentially_unsafe safe_substitution ->
        (match rvalue_computation potentially_unsafe actor s with
         | ComputationImpossible -> ComputationImpossible
         | ComputationUndefined -> rvalue_computation safe_substitution actor s
         | ComputationProduces value -> return value)
    | ExpressionInitialTid ->
        return (ObjectValueAbstract tid_t s.initial_tid)
    | ExpressionUniqsUsed ->
        return (ObjectValueAbstract (list root_id_uniquifier_t) s.uniqs_used)
    | ExpressionStopReason ->
        return (ObjectValueAbstract stop_reason_t s.stop_reason)

and lvalue_computation
  (exp: expression_t)
  (actor: tid_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.Pointer.t) =
  if not (expression_valid exp) then
    ComputationImpossible
  else
    match exp with
    | ExpressionGlobalVariable _ var_id -> return (PointerRoot (RootIdGlobal var_id))
    | ExpressionLocalVariable _ var_id ->
        let thread = s.threads actor in
        if not (list_contains var_id thread.top.local_variables) then
          ComputationImpossible
        else
          return (PointerRoot (RootIdStack actor thread.top.method_id thread.top.frame_uniq var_id))
    | ExpressionDereference _ ptr ->
        let? ptr_value = rvalue_computation ptr actor s in
        return (PrimitiveBoxPointer?.ptr (ObjectValuePrimitive?.value ptr_value))
    | ExpressionFieldOf td obj field_id ->
        let? obj_ptr = lvalue_computation obj actor s in
        return (PointerField obj_ptr field_id)
    | _ -> ComputationImpossible

and rvalues_computation
  (exps: list expression_t)
  (actor: tid_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t (list object_value_t)) =
  match exps with
  | [] -> return []
  | first_exp :: remaining_exps ->
      let? first_value = rvalue_computation first_exp actor s in
      let? remaining_values = rvalues_computation remaining_exps actor s in
      return (first_value :: remaining_values)
module Armada.Expression

open Armada.Base
open Armada.BinaryOp
open Armada.BoundedInt
open Armada.Computation
open Armada.Memory
open Armada.Pointer
open Armada.State
open Armada.Thread
open Armada.Type
open Armada.UnaryOp
open FStar.Sequence.Base
open Spec.List
open Spec.Ubool
open Util.List

let rec build_function_type (return_type: Type0) (operand_types: list Type0) : Type =
  match operand_types with
  | [] -> conditional_computation_t return_type
  | first_type :: remaining_types -> (first_type -> GTot (build_function_type return_type remaining_types))

noeq type expression_t =
  | ExpressionConstant: (value: object_value_t) -> expression_t
  | ExpressionGlobalVariable: (td: object_td_t) -> (var_id: var_id_t) -> expression_t
  | ExpressionLocalVariable: (td: object_td_t) -> (var_id: var_id_t) -> expression_t
  | ExpressionUnaryOperator:
      (operand_td: object_td_t) -> (result_td: object_td_t) ->
      (operator: unary_op_t operand_td result_td) -> (operand: expression_t) -> expression_t
  | ExpressionBinaryOperator:
      (operand_td1: object_td_t) -> (operand_td2: object_td_t) -> (result_td: object_td_t) ->
      (operator: binary_op_t operand_td1 operand_td2 result_td) ->
      (operand1: expression_t) -> (operand2: expression_t) -> expression_t
  | ExpressionIf: (td: object_td_t) -> (cond: expression_t) -> (operand_then: expression_t) ->
      (operand_else: expression_t) -> expression_t
  | ExpressionDereference: (td: object_td_t) -> (ptr: expression_t) -> expression_t
  | ExpressionAddressOf: (obj: expression_t) -> expression_t
  | ExpressionPointerOffset: (ptr: expression_t) -> (offset: expression_t) -> expression_t
  | ExpressionFieldOf: (td: object_td_t) -> (obj: expression_t) -> (field_id: nat) -> expression_t
  | ExpressionAllocated: (ptr: expression_t) -> expression_t
  | ExpressionApplyFunction:
      (td: object_td_t) -> (operands: list expression_t) -> (return_type: Type0) -> (operand_types: list Type0) ->
      (fn: build_function_type return_type operand_types) -> expression_t
  | ExpressionIfUndefined:
      (td: object_td_t) -> (potentially_unsafe: expression_t) -> (safe_substitution: expression_t) -> expression_t
  | ExpressionInitialTid: expression_t
  | ExpressionUniqsUsed: expression_t
  | ExpressionStopReason: expression_t

let expression_to_td (exp: expression_t) : GTot object_td_t =
  match exp with
  | ExpressionConstant value -> object_value_to_td value
  | ExpressionGlobalVariable td _ -> td
  | ExpressionLocalVariable td _ -> td
  | ExpressionUnaryOperator _ result_td _ _ -> result_td
  | ExpressionBinaryOperator _ _ result_td _ _ _ -> result_td
  | ExpressionIf td _ _ _ -> td
  | ExpressionDereference td _ -> td
  | ExpressionAddressOf obj -> ObjectTDPrimitive PrimitiveTDPointer
  | ExpressionPointerOffset _ _ -> ObjectTDPrimitive PrimitiveTDPointer
  | ExpressionFieldOf td _ _ -> td
  | ExpressionAllocated _ -> ObjectTDPrimitive PrimitiveTDBool
  | ExpressionApplyFunction td _ _ _ _ -> td
  | ExpressionIfUndefined td _ _ -> td
  | ExpressionInitialTid -> ObjectTDAbstract tid_t
  | ExpressionUniqsUsed -> ObjectTDAbstract (list root_id_uniquifier_t)
  | ExpressionStopReason -> ObjectTDAbstract stop_reason_t

let rec expressions_to_tds (exps: list expression_t) : GTot (list object_td_t) =
  match exps with
  | [] -> []
  | first_exp :: remaining_exps -> (expression_to_td first_exp) :: (expressions_to_tds remaining_exps)

let rec types_to_tds (tys: list Type0) : (list object_td_t) =
  match tys with
  | [] -> []
  | first_ty :: remaining_tys -> (ObjectTDAbstract first_ty) :: (types_to_tds remaining_tys)

let rec expression_valid (exp: expression_t) : GTot bool =
  match exp with
  | ExpressionConstant value -> object_value_valid value
  | ExpressionGlobalVariable td _ -> true
  | ExpressionLocalVariable td _ -> true
  | ExpressionUnaryOperator operand_td result_td operator operand ->
         expression_valid operand
      && eqb (expression_to_td operand) operand_td
  | ExpressionBinaryOperator operand_td1 operand_td2 result_td operator operand1 operand2 ->
         expression_valid operand1
      && expression_valid operand2
      && eqb (expression_to_td operand1) operand_td1
      && eqb (expression_to_td operand2) operand_td2
  | ExpressionIf td cond operand_then operand_else ->
         expression_valid cond
      && expression_valid operand_then
      && expression_valid operand_else
      && eqb (expression_to_td cond) (ObjectTDPrimitive PrimitiveTDBool)
      && eqb (expression_to_td operand_then) td
      && eqb (expression_to_td operand_else) td
  | ExpressionDereference td ptr ->
         expression_valid ptr
      && eqb (expression_to_td ptr) (ObjectTDPrimitive PrimitiveTDPointer)
  | ExpressionAddressOf obj -> expression_valid obj
  | ExpressionPointerOffset ptr offset ->
         expression_valid ptr
      && expression_valid offset
      && eqb (expression_to_td ptr) (ObjectTDPrimitive PrimitiveTDPointer)
      && eqb (expression_to_td offset) (ObjectTDAbstract int)
  | ExpressionFieldOf td obj field_id ->
         expression_valid obj
      && ObjectTDStruct? (expression_to_td obj)
      && 0 <= field_id
      && field_id < length (ObjectTDStruct?.field_tds (expression_to_td obj))
      && eqb td ((ObjectTDStruct?.field_tds (expression_to_td obj)) `index` field_id)
  | ExpressionAllocated ptr ->
         expression_valid ptr
      && eqb (expression_to_td ptr) (ObjectTDPrimitive PrimitiveTDPointer)
  | ExpressionApplyFunction td operands return_type operand_types _ ->
         eqb td (ObjectTDAbstract return_type)
      && eqb (expressions_to_tds operands) (types_to_tds operand_types)
  | ExpressionIfUndefined td potentially_unsafe safe_substitution ->
         eqb td (expression_to_td potentially_unsafe)
      && eqb td (expression_to_td safe_substitution)
  | ExpressionInitialTid -> true
  | ExpressionUniqsUsed -> true
  | ExpressionStopReason -> true

type valid_expression_t = value: expression_t{expression_valid value}

let rec apply_function_to_operands
  (operands: list object_value_t)
  (return_type: Type0)
  (operand_types: list Type0)
  (fn: build_function_type return_type operand_types)
  : GTot (conditional_computation_t return_type) =
  match operands, operand_types with
  | [], [] -> fn
  | first_operand :: remaining_operands, first_operand_type :: remaining_operand_types ->
      (match first_operand with
       | ObjectValueAbstract ty value ->
           if eqb first_operand_type ty then
             let fn_cast: first_operand_type -> GTot (build_function_type return_type remaining_operand_types) = fn in
             apply_function_to_operands remaining_operands return_type remaining_operand_types (fn_cast value)
           else
             ComputationUndefined
       | _ -> ComputationUndefined)
  | _ -> ComputationImpossible
/
Util.List.fst.checked Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.UnaryOp.fst.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.Computation.fst.checked Armada.BoundedInt.fst.checked Armada.BinaryOp.fst.checked Armada.Base.fst.checked
Armada.Expression.fst
exp: Armada.Expression.expression_t -> actor: Armada.Base.tid_t -> s: Armada.State.t
  -> Prims.GTot (Armada.Computation.conditional_computation_t Armada.Pointer.t)
Armada.Expression.expression_t Armada.Base.tid_t Armada.State.t Prims.op_Negation Armada.Expression.expression_valid Armada.Computation.ComputationImpossible Armada.Pointer.t Prims.bool Armada.Type.object_td_t Armada.Base.var_id_t Armada.Computation.return Armada.Pointer.PointerRoot Armada.Base.RootIdGlobal Spec.List.list_contains Armada.Thread.__proj__Mkstack_frame_t__item__local_variables Armada.Thread.__proj__Mkt__item__top Armada.Base.RootIdStack Armada.Thread.__proj__Mkstack_frame_t__item__method_id Armada.Thread.__proj__Mkstack_frame_t__item__frame_uniq Armada.Computation.conditional_computation_t Armada.Thread.t Armada.State.__proj__Mkt__item__threads Armada.Computation.op_let_Question Armada.Type.valid_object_value_t Armada.Expression.expression_to_td Armada.Expression.rvalue_computation Armada.Type.__proj__PrimitiveBoxPointer__item__ptr Armada.Type.__proj__ObjectValuePrimitive__item__value Prims.nat Armada.Expression.lvalue_computation Armada.Pointer.PointerField
let rec lvalue_computation (exp: expression_t) (actor: tid_t) (s: Armada.State.t)
    : GTot (conditional_computation_t Armada.Pointer.t) =
  
if not (expression_valid exp)
then ComputationImpossible
else
  match exp with
  | ExpressionGlobalVariable _ var_id -> return (PointerRoot (RootIdGlobal var_id))
  | ExpressionLocalVariable _ var_id ->
    let thread = s.threads actor in
    if not (list_contains var_id thread.top.local_variables)
    then ComputationImpossible
    else return (PointerRoot (RootIdStack actor thread.top.method_id thread.top.frame_uniq var_id))
  | ExpressionDereference _ ptr ->
    let? ptr_value = rvalue_computation ptr actor s in
    return (PrimitiveBoxPointer?.ptr (ObjectValuePrimitive?.value ptr_value))
  | ExpressionFieldOf td obj field_id ->
    let? obj_ptr = lvalue_computation obj actor s in
    return (PointerField obj_ptr field_id)
  | _ -> ComputationImpossible