val locations_of_operand128 (o: operand128) : locations & locations
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]
val locations_of_operand128 (o: operand128) : locations & locations
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]
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
Vale.X64.Machine_s.operand128 Vale.X64.Machine_s.quad32 FStar.Pervasives.Native.Mktuple2 Vale.Transformers.Locations.locations Prims.Nil Vale.Transformers.Locations.location Vale.X64.Machine_s.reg_xmm Prims.Cons Vale.Transformers.Locations.ALocReg Vale.X64.Machine_s.Reg Vale.X64.Machine_s.maddr Vale.Arch.HeapTypes_s.taint Vale.Transformers.BoundedInstructionEffects.locations_of_maddr Vale.Transformers.Locations.ALocMem Vale.X64.Machine_s.rRsp Vale.Transformers.Locations.ALocStack FStar.Pervasives.Native.tuple2
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]
val locations_of_operand128 (o: operand128) : locations & locations
o: Vale.X64.Machine_s.operand128
  -> Vale.Transformers.Locations.locations * Vale.Transformers.Locations.locations