val build_reserved_args_ins (l: list instr_operand) (reserved: (reg_64 -> bool))
    : Tot (reg_64 -> bool) (decreases l)
let rec build_reserved_args_ins (l:list instr_operand) (reserved:reg_64 -> bool)
  : Tot (reg_64 -> bool)
  (decreases l) =
  fun r ->
  match l with
  | [] -> reserved r
  | hd::tl ->
    let reserved : (reg_64 -> bool) = (fun r ->
      match hd with
      | IOpIm (IOp64One (OReg reg)) ->
          // Implicit register, adding it to "reserved" registers
          if r = reg then true else reserved r
      | _ -> reserved r)
    in build_reserved_args_ins tl reserved r
val build_reserved_args_ins (l: list instr_operand) (reserved: (reg_64 -> bool))
    : Tot (reg_64 -> bool) (decreases l)
let rec build_reserved_args_ins (l: list instr_operand) (reserved: (reg_64 -> bool))
    : Tot (reg_64 -> bool) (decreases l) =
fun r ->
  match l with
  | [] -> reserved r
  | hd :: tl ->
    let reserved:(reg_64 -> bool) =
      (fun r ->
          match hd with
          | IOpIm (IOp64One (OReg reg)) -> if r = reg then true else reserved r
          | _ -> reserved r)
    in
    build_reserved_args_ins tl reserved r
Vale.X64.Print_Inline_s.fst.checked
Vale.X64.Print_s.fst.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Interop.X64.fsti.checked Vale.Interop.Base.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked
Vale.X64.Print_Inline_s.fst
Prims.list Vale.X64.Instruction_s.instr_operand Vale.X64.Machine_s.reg_64 Prims.bool Vale.X64.Print_Inline_s.build_reserved_args_ins Prims.op_Equality
module Vale.X64.Print_Inline_s

open FStar.Mul
open FStar.List.Tot
open Vale.X64.Machine_s
open Vale.X64.Bytes_Code_s
open Vale.X64.Machine_Semantics_s
open Vale.X64.Instruction_s
open FStar.IO
open Vale.Interop.Base
open Vale.Interop.X64
module P = Vale.X64.Print_s

let print_rettype (ret_val:option string) = match ret_val with
  | None -> "void"
  | Some _ -> "uint64_t"

let print_basetype (t:base_typ) = match t with
  | TUInt8 -> "uint8_t"
  | TUInt16 -> "uint16_t"
  | TUInt32 -> "uint32_t"
  | TUInt64 -> "uint64_t"
  | TUInt128 -> "ERROR"

// Returns "uint8_t arg2" or "uint64_t* arg0" for instance
let print_arg (a:td) (i:nat) (names:nat -> string) = match a with
  | TD_Base src -> print_basetype src ^ " " ^ names i
  | TD_Buffer src _ _ | TD_ImmBuffer src _ _ -> print_basetype src ^ " *" ^ names i

// Prints a list of args with their types, separated by a comma
let rec print_args (args:list td) (i:nat) (names:nat -> string) = match args with
  | [] -> ""
  | [a] -> print_arg a i names
  | a::q -> print_arg a i names ^ ", " ^ print_args q (i+1) names

let rec build_reserved_args_outs (l:list instr_out) (reserved:reg_64 -> bool)
  : Tot (reg_64 -> bool)
  (decreases l) =
  fun r ->
  match l with
  | [] -> reserved r
  | hd::tl ->
    let (_, op) = hd in
    let reserved : (reg_64 -> bool) = (fun r ->
      match op with
      | IOpIm (IOp64One (OReg reg)) ->
          // Implicit register, adding it to "reserved" registers
          if r = reg then true else reserved r
      | _ -> reserved r)
    in build_reserved_args_outs tl reserved r

let rec build_reserved_args_ins (l:list instr_operand) (reserved:reg_64 -> bool)
  : Tot (reg_64 -> bool)
val build_reserved_args_ins (l: list instr_operand) (reserved: (reg_64 -> bool))
    : Tot (reg_64 -> bool) (decreases l)

    l: Prims.list Vale.X64.Instruction_s.instr_operand ->
    reserved: (_: Vale.X64.Machine_s.reg_64 -> Prims.bool)
  -> Prims.Tot (_: Vale.X64.Machine_s.reg_64 -> Prims.bool)