val aux_read_set0 (args: list instr_operand) (oprs: instr_operands_t_args args) : locations
let rec aux_read_set0 (args:list instr_operand) (oprs:instr_operands_t_args args) : locations =
  match args with
  | [] -> []
  | (IOpEx i) :: args ->
    let l, r = coerce #(instr_operand_t i & instr_operands_t_args args) oprs in
    both (locations_of_explicit i l) `L.append` aux_read_set0 args r
  | (IOpIm i) :: args ->
    both (locations_of_implicit i) `L.append` aux_read_set0 args (coerce #(instr_operands_t_args args) oprs)
val aux_read_set0 (args: list instr_operand) (oprs: instr_operands_t_args args) : locations
let rec aux_read_set0 (args: list instr_operand) (oprs: instr_operands_t_args args) : locations =
match args with
| [] -> []
| IOpEx i :: args ->
  let l, r = coerce #(instr_operand_t i & instr_operands_t_args args) oprs in
  (both (locations_of_explicit i l)) `L.append` (aux_read_set0 args r)
| IOpIm i :: args ->
  (both (locations_of_implicit i))
  `L.append`
  (aux_read_set0 args (coerce #(instr_operands_t_args args) oprs))
Vale.Transformers.BoundedInstructionEffects.fst.checked
Vale.X64.Print_s.fst.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Instructions_s.fsti.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Transformers.Locations.fst.checked Vale.Transformers.Locations.fst.checked Vale.Def.PossiblyMonad.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Option.fst.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
Vale.Transformers.BoundedInstructionEffects.fst
Prims.list Vale.X64.Instruction_s.instr_operand Vale.X64.Instruction_s.instr_operands_t_args Prims.Nil Vale.Transformers.Locations.location Vale.X64.Instruction_s.instr_operand_explicit Vale.X64.Instruction_s.instr_operand_t FStar.List.Tot.Base.append Vale.Transformers.BoundedInstructionEffects.both Vale.Transformers.BoundedInstructionEffects.locations_of_explicit Vale.Transformers.BoundedInstructionEffects.aux_read_set0 Vale.Transformers.Locations.locations FStar.Pervasives.Native.tuple2 Vale.X64.Instruction_s.coerce Vale.X64.Instruction_s.instr_operand_implicit Vale.Transformers.BoundedInstructionEffects.locations_of_implicit
module Vale.Transformers.BoundedInstructionEffects

open Vale.X64.Bytes_Code_s
open Vale.X64.Instruction_s
open Vale.X64.Instructions_s
open Vale.X64.Machine_Semantics_s
open Vale.X64.Machine_s
open Vale.X64.Print_s

open Vale.Def.PossiblyMonad

open Vale.Transformers.Locations
friend Vale.Transformers.Locations

module L = FStar.List.Tot


let locations_of_maddr (m:maddr) (mem:location) : locations =
  mem :: (
    match m with
    | MConst _ -> []
    | MReg r _ -> [ALocReg r]
    | MIndex b _ i _ -> [ALocReg b; ALocReg i]
  )

let locations_of_operand64 (o:operand64) : locations & locations =
  match o with
  | OConst _ -> [], []
  | OReg r -> [], [ALocReg (Reg 0 r)]
  | OMem (m, _) -> locations_of_maddr m ALocMem, [ALocMem]
  | OStack (m, _) -> (ALocReg (Reg 0 rRsp)) :: locations_of_maddr m ALocStack, [ALocStack]

let locations_of_operand128 (o:operand128) : locations & locations =
  match o with
  | OConst _ -> [], []
  | OReg r -> [], [ALocReg (Reg 1 r)]
  | OMem (m, _) -> locations_of_maddr m ALocMem, [ALocMem]
  | OStack (m, _) -> (ALocReg (Reg 0 rRsp)) :: locations_of_maddr m ALocStack, [ALocStack]

let locations_of_explicit (t:instr_operand_explicit) (i:instr_operand_t t) : locations & locations =
  match t with
  | IOp64 -> locations_of_operand64 i
  | IOpXmm -> locations_of_operand128 i

let locations_of_implicit (t:instr_operand_implicit) : locations & locations =
  match t with
  | IOp64One i -> locations_of_operand64 i
  | IOpXmmOne i -> locations_of_operand128 i
  | IOpFlagsCf -> [], [ALocCf]
  | IOpFlagsOf -> [], [ALocOf]

let both (x: locations & locations) =
  let a, b = x in
  a `L.append` b
val aux_read_set0 (args: list instr_operand) (oprs: instr_operands_t_args args) : locations

    args: Prims.list Vale.X64.Instruction_s.instr_operand ->
    oprs: Vale.X64.Instruction_s.instr_operands_t_args args
  -> Vale.Transformers.Locations.locations