coreHint.atd

type scope = [ Source | Target ] <ocaml repr="classic">

type position_phinode = {
  prev_block_name : string;
}

type position_command = {
  index : int;
  register_name : string;
}

(* Position of an instruction is phinode or register *)
type instr_index = [
  | Phinode of position_phinode
  | Command of position_command
  ] <ocaml repr="classic">

type position = {
  scope : scope;
  block_name : string;
  instr_index : instr_index;
}

(* If tag of register is one of Physical, Previous, and Ghost *)
type tag = [ Physical | Previous | Ghost ] <ocaml repr="classic">

type register = {
  name : string; (* identifier of a register *)
  tag : tag;     (* indicates whether this register is physical or previous or ghost *)
}

type bop = [ | BopAdd | BopSub | BopMul | BopUdiv 
             | BopSdiv | BopUrem | BopSrem | BopShl 
             | BopLshr | BopAshr | BopAnd | BopOr 
             | BopXor ] <ocaml repr="classic">

type fbop = [ BopFadd | BopFsub | BopFmul | BopFdiv | BopFrem ] <ocaml repr="classic">

type icmp_pred = [ | CondEq | CondNe | CondUgt | CondUge | CondUlt 
              | CondUle | CondSgt | CondSge | CondSlt | CondSle ] <ocaml repr="classic">

type fcmp_pred = [ CondFfalse | CondFoeq | CondFogt | CondFoge | CondFolt | CondFole | CondFone | CondFord | CondFuno | CondFueq | CondFugt | CondFuge | CondFult | CondFule | CondFune | CondFtrue ] <ocaml repr="classic">

(* integer type of bitsize *)
type int_type = [ IntType of int ] <ocaml repr="classic">

(* float type *)
(* http://llvm.org/docs/LangRef.html#floating-point-types *)
(* http://llvm.org/docs/doxygen/html/classllvm_1_1APFloat.html *)
type float_type = [ 
    | HalfType (* equivalent to Llvm.APFloat.Semantics.IEEEhalf in LLVM ocaml binding *)
               (* no matching type in Vellvm *)
    | FloatType (* equivalent to Llvm.APFloat.Semantics.IEEEsingle in LLVM ocaml binding *)
                (* equivalent to Syntax.LLVMsyntax.Coq_fp_float in Vellvm *)
    | DoubleType (* equivalent to Llvm.APFloat.Semantics.IEEEdouble in LLVM ocaml binding *)
                 (* equivalent to Syntax.LLVMsyntax.Coq_fp_double in Vellvm *)
    | FP128Type (* equivalent to Llvm.APFloat.Semantics.IEEEquad in LLVM ocaml binding*)
                (* equivalent to Syntax.LLVMsyntax.Coq_fp_fp128 in Vellvm*)
    | PPC_FP128Type (* equivalent to Llvm.APFloat.Semantics.PPCDoubleDouble in LLVM ocaml binding *)
                    (* equivalent to Syntax.LLVMsyntax.Coq_fp_ppc_fp128 in Vellvm*)
    | X86_FP80Type (* equivalent to Llvm.APFloat.Semantics.X87DoubleExternded in LLVM ocaml binding *)
                   (* equivalent to Syntax.LLVMsyntax.Coq_fp_x86_fp80 in Vellvm*)
    ] <ocaml repr="classic">

type value_type = [
    | VoidType
    | IntValueType of int_type
    | FloatValueType of float_type
    | NamedType of string
    | PtrType of (int * value_type) (* (addr space, type) *)
    | ArrayType of (int * value_type)
    | FunctionType of (value_type * (value_type list) * bool * int) (* (return-type, argument-type, is-var-arg, arg-size) *)
    | VectorType of (int * value_type)
    | StructType of (value_type list) (* list of elements *)
    ] <ocaml repr="classic">

type const_int = {
  int_value : string;
  int_type : int_type;
}

type const_float = {
  float_value : string;
  float_type : float_type;
}

type const_global_var_addr = {
  var_id : string;
  var_type : value_type;
}

type const_expr_get_element_ptr = {
  srcelemty : value_type;
  v : constant;
  idxlist : constant list;
  dstty : value_type;
  is_inbounds : bool;
}

type const_expr_bitcast = {
  v : constant;
  dstty : value_type;
}

type const_expr_inttoptr = {
  v : constant;
  dstty : value_type;
}

type const_expr_ptrtoint = {
  v : constant;
  dstty : value_type;
}

type const_expr_binaryop = {
  opcode : bop;
  v1 : constant;
  v2 : constant;
}

type constant_expr = [
  | ConstExprGetElementPtr of const_expr_get_element_ptr
  | ConstExprBitcast of const_expr_bitcast 
  | ConstExprInttoptr of const_expr_inttoptr
  | ConstExprPtrtoint of const_expr_ptrtoint
  | ConstExprBinaryOp of const_expr_binaryop
  ] <ocaml repr="classic">

type constant = [
  | ConstInt of const_int
  | ConstFloat of const_float
  | ConstNull of (int * value_type) (* addr space, type *)
  | ConstUndef of value_type 
  | ConstGlobalVarAddr of const_global_var_addr 
  | ConstDataVector of (value_type * constant list)
  | ConstZeroInitializer of value_type
  | ConstExpr of constant_expr
  ] <ocaml repr="classic">

type value = [ Id of register | ConstVal of constant ] <ocaml repr="classic">

type size = [ Size of int ] <ocaml repr="classic">

type pointer = {
  v : value;
  ty : value_type;
}

type binary_operator = {
  opcode : bop;
  operandtype : value_type;
  operand1 : value;
  operand2 : value;
}

type float_binary_operator = {
  opcode : fbop;
  operandtype : value_type;
  operand1 : value;
  operand2 : value;
}

type integer_compare_inst = {
  predicate : icmp_pred;
  operandtype : value_type;
  operand1 : value;
  operand2 : value;
}

type float_compare_inst = {
  predicate : fcmp_pred;
  operandtype : value_type;
  operand1 : value;
  operand2 : value;
}

type load_inst = {
  pointertype : value_type;
  valtype : value_type;
  ptrvalue : value;
  align : int;
}

type bit_cast_inst = {
  fromty : value_type;
  v : value;
  toty : value_type;
}

type get_element_ptr_inst = {
  ty : value_type;
  retty : value_type;
  ptr : value;
  indexes : (size * value) list;
  is_inbounds : bool;
}

type int_to_ptr_inst = {
  fromty : value_type;
  v : value;
  toty : value_type;
}

type ptr_to_int_inst = {
  fromty : value_type;
  v : value;
  toty : value_type;
}

type fpext_inst = {
  fromty : value_type;
  v : value;
  toty : value_type;
}

type fptrunc_inst = {
  fromty : value_type;
  v : value;
  toty : value_type;
}

type zext_inst = {
  fromty : value_type;
  v : value;
  toty : value_type;
}

type sext_inst = {
  fromty : value_type;
  v : value;
  toty : value_type;
}

type trunc_inst = {
  fromty : value_type;
  v : value;
  toty : value_type;
}

type fptosi_inst = {
  fromty : value_type;
  v : value;
  toty : value_type;
}

type sitofp_inst = {
  fromty : value_type;
  v : value;
  toty : value_type;
}

type uitofp_inst = {
  fromty : value_type;
  v : value;
  toty : value_type;
}

type select_inst = {
  cond : value;
  valty : value_type;
  trueval : value;
  falseval : value;
}

type extract_value_inst = {
  aggrty : value_type;
  aggrv : value;
  idx : int list;
  retty : value_type;
}

type insert_value_inst = {
  aggrty : value_type;
  aggrv : value;
  argty : value_type;
  argv : value;
  idx : int list;
}

type instruction = [ 
  | BinaryOp of binary_operator
  | FloatBinaryOp of float_binary_operator
  | ICmpInst of integer_compare_inst
  | FCmpInst of float_compare_inst
  | LoadInst of load_inst
  | BitCastInst of bit_cast_inst
  | GetElementPtrInst of get_element_ptr_inst
  | SelectInst of select_inst
  | IntToPtrInst of int_to_ptr_inst
  | PtrToIntInst of ptr_to_int_inst
  | FpextInst of fpext_inst
  | FptruncInst of fptrunc_inst
  | ZextInst of zext_inst
  | SextInst of sext_inst
  | TruncInst of trunc_inst
  | FptosiInst of fptosi_inst
  | SitofpInst of sitofp_inst
  | UitofpInst of uitofp_inst
  | InsertValueInst of insert_value_inst
  | ExtractValueInst of extract_value_inst
] <ocaml repr="classic">

type expr = [
  | Var of register
  | Rhs of (register * scope)
  | Const of constant
  | Insn of instruction
] <ocaml repr="classic">


(*****************************************)
(*              Propagates               *)
(*****************************************)

type propagate_lessdef = {
  lhs : expr;
  rhs : expr;
  scope : scope;
}

type propagate_noalias = {
  lhs : pointer;
  rhs : pointer;
  scope : scope;
}

type propagate_diffblock = {
  lhs : value;
  rhs : value;
  scope : scope;
}

type propagate_unique = {
  register_name : string;
  scope : scope;
}

type propagate_private = {
  p : register;
  scope : scope;
}

type propagate_object = [
  | Lessdef of propagate_lessdef
  | Noalias of propagate_noalias
  | Diffblock of propagate_diffblock
  | Maydiff of register
  | Unique of propagate_unique
  | Private of propagate_private
  ] <ocaml repr="classic">

type propagate_range = [
  | Bounds of (position * position)
  | BoundSet of (position * position list)
  | Global
  ] <ocaml repr="classic">

type propagate = {
  propagate : propagate_object;
  propagate_range : propagate_range;
}

(*****************************************)
(*             Inference rules           *)
(*****************************************)

type add_sub = {
  minusy : register;
  z : register;
  x : value;
  y : value;
  sz : size;
}

type add_commutative_tgt = {
  z : register;
  x : value;
  y : value;
  sz : size;
}


type add_dist_sub = {
  z : register;
  minusx : register;
  minusy : value;
  w : register;
  x : value;
  y : value;
  sz : size;
}

type add_shift = {
  y : register;
  v : value;
  sz : size;
}

type add_signbit = {
  x : register;
  e1 : value;
  e2 : value;
  sz : size;
}

type transitivity = {
  e1 : expr;
  e2 : expr;
  e3 : expr;
}

type transitivity_tgt = {
  e1 : expr;
  e2 : expr;
  e3 : expr;
}

type transitivity_pointer_lhs = {
  p : value;
  q : value;
  v : value;
  typ : value_type;
  align : size;
}

type transitivity_pointer_rhs = {
  p : value;
  q : value;
  v : value;
  typ : value_type;
  align : size;
}

type substitute = {
  x : register;
  y : value;
  e : expr;
}

type substitute_rev = {
  x : register;
  y : value;
  e : expr;
}

type substitute_tgt = {
  x : register;
  y : value;
  e : expr;
}

type add_onebit = {
  z : register;
  x : value;
  y : value;
}

type add_zext_bool = {
  x : register;
  y : register;
  b : value;
  c : const_int;
  cprime : const_int;
  sz : size;
}

type add_const_not = {
  z : register;
  y : register;
  x : value;
  c1 : const_int;
  c2 : const_int;
  sz : size;
}

type add_mask = {
  z : register;
  y : register;
  yprime : register;
  x : value;
  c1 : const_int;
  c2 : const_int;
  sz : size;
}

type add_select_zero = {
  z : register;
  x : register;
  y : register;
  c : value;
  n : value;
  a : value;
  sz : size;
}

type add_select_zero2 = {
  z : register;
  x : register;
  y : register;
  c : value;
  n : value;
  a : value;
  sz : size;
}


type add_xor_and = {
  z : register;
  a : value;
  b : value;
  x : register;
  y : register;
  sz : size;
}

type add_or_and = {
  z : register;
  a : value;
  b : value;
  x : register;
  y : register;
  sz : size;
}

type and_de_morgan = {
  z : register;
  x : register;
  y : register;
  zprime : register;
  a : value;
  b : value;
  sz : size;
}

type and_mone = {
  z : value;
  x : value;
  sz : size;
}

type and_not = {
  z : value;
  x : value;
  y : value;
  sz : size;
}

type and_or = {
  z : value;
  x : value;
  y : value;
  a : value;
  sz : size;
}

type and_or_const2 = {
  z : register;
  y : register;
  yprime : register;
  x : value;
  c1 : const_int;
  c2 : const_int;
  c3 : const_int;
  sz : size;
}

type and_same = {
  z : value;
  x : value;
  sz : size;
}

type and_true_bool = {
  x : value;
  y : value;
}

type and_true_bool_tgt = {
  x : value;
  y : value;
}

type and_undef = {
  z : value;
  x : value;
  sz : size;
}

type and_xor_const = {
  z : register;
  y : register;
  yprime : register;
  x : value;
  c1 : const_int;
  c2 : const_int;
  c3 : const_int;
  sz : size;
}

type and_zero = {
  z : value;
  x : value;
  sz : size;
}

type and_or_not1 = {
  z : register;
  x : register;
  y : register;
  a : value;
  b : value;
  sz : size;
}

type bitcast_bitcast = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type bitcast_double_i64 = {
    src : constant;
    tgt : const_int;
}

type bitcast_load = {
    ptr : value;
    ptrty : value_type;
    v1 : value;
    ptrty2 : value_type;
    v2 : value;
    a : size;
}

type bop_associative = {
  x : register;
  y : register;
  z : register;
  bop : bop;
  c1 : const_int;
  c2 : const_int;
  c3 : const_int;
  sz : size;
}

type bop_commutative = {
  e : expr;
  bop : bop;
  x : value;
  y : value;
  sz : size;
}

type bop_commutative_rev = {
  e : expr;
  bop : bop;
  x : value;
  y : value;
  sz : size;
}

type bop_commutative_tgt = {
  e : expr;
  bop : bop;
  x : value;
  y : value;
  sz : size;
}

type bop_commutative_rev_tgt = {
  e : expr;
  bop : bop;
  x : value;
  y : value;
  sz : size;
}

type fbop_commutative = {
  e : expr;
  fbop : fbop;
  x : value;
  y : value;
  fty : float_type;
}

type fbop_commutative_rev = {
  e : expr;
  fbop : fbop;
  x : value;
  y : value;
  fty : float_type;
}

type fbop_commutative_tgt = {
  e : expr;
  fbop : fbop;
  x : value;
  y : value;
  fty : float_type;
}

type fbop_commutative_rev_tgt = {
  e : expr;
  fbop : fbop;
  x : value;
  y : value;
  fty : float_type;
}

type bop_distributive_over_selectinst = {
  opcode : bop;
  r : register;
  s : register;
  tprime : register;
  t0 : register;
  x : value;
  y : value;
  z : value;
  c : value;
  bopsz : size;
  selty : value_type;
}

type bitcastptr = {
  vprime : value;
  bitcastinst : expr;
}

type bitcast_fpext = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type bitcast_fptosi = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type bitcast_fptoui = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type bitcast_fptrunc = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type bitcast_inttoptr = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type bitcast_ptrtoint = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type bitcast_sext = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type bitcast_sametype = {
    src : value;
    dst : value;
    tty : value_type;
}

type bitcast_sitofp = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type bitcast_trunc = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type bitcast_uitofp = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type bitcast_zext = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type bop_distributive_over_selectinst2 = {
  opcode : bop;
  r : register;
  s : register;
  tprime : register;
  t0 : register;
  x : value;
  y : value;
  z : value;
  c : value;
  bopsz : size;
  selty : value_type;
}

type fadd_commutative_tgt = {
  z : register;
  x : value;
  y : value;
  fty : float_type;
}

type fbop_distributive_over_selectinst = {
  fopcode : fbop;
  r : register;
  s : register;
  tprime : register;
  t0 : register;
  x : value;
  y : value;
  z : value;
  c : value;
  fbopty : float_type;
  selty : value_type;
}

type fbop_distributive_over_selectinst2 = {
  fopcode : fbop;
  r : register;
  s : register;
  tprime : register;
  t0 : register;
  x : value;
  y : value;
  z : value;
  c : value;
  fbopty : float_type;
  selty : value_type;
}

type fmul_commutative_tgt = {
  z : register;
  x : value;
  y : value;
  fty : float_type;
}

type fpext_fpext = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type fpext_bitcast = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type fptosi_bitcast = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type fptosi_fpext = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type fptoui_bitcast = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type fptoui_fpext = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type fptrunc_bitcast = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type fptrunc_fpext = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type gepzero = {
  vprime : value;
  gepinst : expr;
}

type gep_inbounds_remove = {
  gepinst : expr;
}

type gep_inbounds_add = {
    v : value;
    ptr : value;
    loadty : value_type;
    al : size;
    e : expr;
}

type intro_ghost = {
  x : expr;
  g : register;
}

type intro_ghost_src = {
  x : expr;
  g : register;
}

type intro_eq = {
  x : expr;
}

type intro_eq_tgt = {
  x : expr;
}

type inttoptr_load = {
    ptr : value;
    intty : value_type;
    v1 : value;
    ptrty : value_type;
    v2 : value;
    a : size;
}

type inttoptr_bitcast = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type inttoptr_ptrtoint = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type inttoptr_zext = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type lessthan_undef = {
  ty : value_type;
  v : value;
}

type lessthan_undef_tgt = {
  ty : value_type;
  v : value;
}

type mul_bool = {
  z :register;
  x :register;
  y :register;
}

type mul_mone = {
  z : register;
  x : value;
  sz : size;
}

type mul_neg = {
  z : register;
  mx : value;
  my : value;
  x : value;
  y : value;
  sz : size;
}

type mul_shl = {
  z : register;
  y : register;
  x : value;
  a : value;
  sz : size;
}


type mul_add_distributive = {
  z : register;
  x : register;
  y : register;
  w : register;
}

type neg_val = {
  c1 : const_int;
  c2 : const_int;
  sz : size;
}

type diffblock_lessthan = {
  x : value;
  y : value;
  xprime : value;
  yprime : value;
}

type diffblock_noalias = {
  x : value;
  y : value;
  xprime : pointer;
  yprime : pointer;
}

type diffblock_global_global = {
  gx : constant;
  gy : constant;
}

type diffblock_global_unique = {
    gx : constant;
    y : register;
}

type diffblock_unique = {
  x : register;
  y : register;
}

type or_and = {
  z : value;
  y : value;
  x : value;
  a : value;
  sz : size;
}

type or_and_xor = {
  z : value;
  x : value;
  y : value;
  a : value;
  b : value;
  sz : size;
}

type or_commutative_tgt = {
  z : register;
  x : value;
  y : value;
  sz : size;
}

type or_false = {
  x : value;
  y : value;
  sz : size;
}

type or_false_tgt = {
  x : value;
  y : value;
  sz : size;
}

type or_mone = {
  z : value;
  a : value;
  sz : size;
}

type or_not = {
  z : value;
  y : value;
  x : value;
  sz : size;
}

type or_or = {
  z : value;
  x : value;
  y : value;
  a : value;
  b : value;
  sz : size;
}

type or_or2 = {
  z : value;
  x : value;
  y : value;
  yprime : value;
  a : value;
  b : value;
  sz : size;
}

type or_same = {
  z : value;
  a : value;
  sz : size;
}

type or_undef = {
  z : value;
  a : value;
  sz : size;
}

type or_xor = {
  w : value;
  z : value;
  x : value;
  y : value;
  a : value;
  b : value;
  sz : size;
}

type or_xor2 = {
  z : value;
  x1 : value;
  y1 : value;
  x2 : value;
  y2 : value;
  a : value;
  b : value;
  sz : size;
}

type or_xor3 = {
  z : value;
  y : value;
  a : value;
  b : value;
  sz : size;
}

type or_xor4 = {
  z : value;
  x : value;
  y : value;
  a : value;
  b : value;
  nb : value;
  sz : size;
}

type or_zero = {
  z : value;
  a : value;
  sz : size;
}

type ptrtoint_bitcast = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type ptrtoint_inttoptr = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type ptrtoint_load = {
    ptr : value;
    ptrty : value_type;
    v1 : value;
    intty : value_type;
    v2 : value;
    a : size;
}

type ptrtoint_zero = {
    ptrty : value_type;
    intty : value_type;
}

type rem_neg = {
  z : register;
  my : value;
  x : value;
  y : value;
  sz : size;
}

type select_icmp_eq = {
    z : value;
    y : value;
    x : value;
    v : value;
    c : constant;
    cty : value_type;
}

type select_icmp_eq_xor1 = {
    z : value;
    zprime : value;
    v : value;
    x : value;
    u : value;
    w : value;
    c : const_int;
    cprime : const_int;
    s : size;
}

type select_icmp_eq_xor2 = {
    z : value;
    zprime : value;
    v : value;
    x : value;
    u : value;
    w : value;
    c : const_int;
    s : size;
}

type select_icmp_ne = {
    z : value;
    y : value;
    x : value;
    v : value;
    c : constant;
    cty : value_type;
}

type select_icmp_ne_xor1 = {
    z : value;
    zprime : value;
    v : value;
    x : value;
    u : value;
    w : value;
    c : const_int;
    cprime : const_int;
    s : size;
}

type select_icmp_ne_xor2 = {
    z : value;
    zprime : value;
    v : value;
    x : value;
    u : value;
    w : value;
    c : const_int;
    s : size;
}

type select_icmp_sgt_const = {
    z : register;
    y : value;
    x : value;
    c : const_int;
    cprime : const_int;
    selcomm : bool;
    s : size;
}

type select_icmp_sgt_xor1 = {
    z : value;
    zprime : value;
    v : value;
    x : value;
    u : value;
    c : const_int;
    cprime : const_int;
    s : size;
}

type select_icmp_sgt_xor2 = {
    z : value;
    zprime : value;
    v : value;
    x : value;
    u : value;
    c : const_int;
    s : size;
}

type select_icmp_slt_const = {
    z : register;
    y : value;
    x : value;
    c : const_int;
    cprime : const_int;
    selcomm : bool;
    s : size;
}

type select_icmp_slt_xor1 = {
    z : value;
    zprime : value;
    v : value;
    x : value;
    u : value;
    c : const_int;
    cprime : const_int;
    s : size;
}

type select_icmp_slt_xor2 = {
    z : value;
    zprime : value;
    v : value;
    x : value;
    u : value;
    c : const_int;
    s : size;
}

type select_icmp_ugt_const = {
    z : register;
    y : value;
    x : value;
    c : const_int;
    cprime : const_int;
    selcomm : bool;
    s : size;
}

type select_icmp_ult_const = {
    z : register;
    y : value;
    x : value;
    c : const_int;
    cprime : const_int;
    selcomm : bool;
    s : size;
}

type sext_ashr = {
  z : value;
  zprime : value;
  x : value;
  x0 : value;
  y : value;
  w : value;
  c1 : const_int;
  c2 : const_int;
  sz1 : size;
  sz2 : size;
}

type sext_bitcast = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type sext_trunc = {
  z : value;
  x : value;
  y : value;
  c : const_int;
  sz1 : size;
  sz2 : size;
}

type sext_trunc_ashr = {
    z : value;
    x : value;
    xprime : value;
    v : value;
    s1 : size;
    s2 : size;
    i3 : const_int;
}

type shift_undef1 = {
    z : value;
    y : value;
    s : size;
}

type shift_undef2 = {
    z : value;
    y : value;
    c : const_int;
    s : size;
}

type shift_zero1 = {
    z : value;
    y : value;
    s : size;
}

type shift_zero2 = {
    z : value;
    y : value;
    s : size;
}

type sitofp_bitcast = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type sitofp_sext = {
  src : value;
  mid : value;
  dst : value;
  srcty : value_type;
  midty : value_type;
  dstty : value_type;
}

type sitofp_zext = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type sub_add = {
  z : register;
  my : value;
  x : value;
  y : value;
  sz : size;
}

type sub_mone = {
  z : register;
  x : value;
  sz : size;
}

type sub_const_not = {
  z : register;
  y : register;
  x : value;
  c1 : const_int;
  c2 : const_int;
  sz : size;
}

type sub_remove = {
  z : register;
  y : register;
  a : value;
  b : value;
  sz : size;
}

type sub_onebit = {
  z : register;
  x : value;
  y : value;
}

type sub_or_xor = {
  z : register;
  a : value;
  b : value;
  x : register;
  y : register;
  sz : size;
}

type sub_const_add = {
  z : register;
  y : register;
  x : value;
  c1 : const_int;
  c2 : const_int;
  c3 : const_int;
  sz : size;
}

type sub_sdiv = {
  z : register;
  y : register;
  x : value;
  c : const_int;
  cprime : const_int;
  sz : size;
}

type sub_shl = {
  z : register;
  x : value;
  y : register;
  mx : value;
  a : value;
  sz : size;
}

type sub_sub = {
  z : register;
  x : value;
  y : value;
  w : value;
  sz : size;
}

type sdiv_mone = {
  z : register;
  x : value;
  sz : size;
}

type sdiv_sub_srem = {
  z : register;
  b : register;
  a : register;
  x : value;
  y : value;
  sz : size;
}

type sext_sext = {
  src : value;
  mid : value;
  dst : value;
  srcty : value_type;
  midty : value_type;
  dstty : value_type;
}

type sext_zext = {
  src : value;
  mid : value;
  dst : value;
  srcty : value_type;
  midty : value_type;
  dstty : value_type;
}

type trunc_bitcast = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type trunc_onebit = {
    z : value;
    x : value;
    y : value;
    orgsz : size;
}

type trunc_ptrtoint = {
  src : value;
  mid : value;
  dst : value;
  srcty : value_type;
  midty : value_type;
  dstty : value_type;
}

type trunc_sext = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type trunc_zext = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type trunc_trunc = {
  src : value;
  mid : value;
  dst : value;
  srcty : value_type;
  midty : value_type;
  dstty : value_type;
}

type udiv_sub_urem = {
  z : register;
  b : register;
  a : register;
  x : value;
  y : value;
  sz : size;
}

type udiv_zext = {
  z : register;
  x : register;
  y : register;
  k : register;
  a : value;
  b : value;
  sz1 : size;
  sz2 : size;
}

type udiv_zext_const = {
  z : register;
  x : register;
  c : const_int;
  k : register;
  a : value;
  sz1 : size;
  sz2 : size;
}

type uitofp_bitcast = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type uitofp_zext = {
  src : value;
  mid : value;
  dst : value;
  srcty : value_type;
  midty : value_type;
  dstty : value_type;
}

type urem_zext = {
  z : register;
  x : register;
  y : register;
  k : register;
  a : value;
  b : value;
  sz1 : size;
  sz2 : size;
}

type urem_zext_const = {
  z : register;
  x : register;
  c : const_int;
  k : register;
  a : value;
  sz1 : size;
  sz2 : size;
}

type xor_commutative_tgt = {
  z : register;
  x : value;
  y : value;
  sz : size;
}

type xor_same = {
    z : value;
    a : value;
    s : size;
}

type xor_undef = {
    z : value;
    a : value;
    s : size;
}

type xor_zero = {
    z : value;
    a : value;
    s : size;
}

type xor_not = {
    z : value;
    y : value;
    x : value;
    s : size;
}

type zext_bitcast = {
    src : value;
    mid : value;
    dst : value;
    srcty : value_type;
    midty : value_type;
    dstty : value_type;
}

type zext_trunc_and = {
    z : value;
    x : value;
    y : value;
    w : value;
    c : constant;
    s : size;
    sprime : size;
}

type zext_trunc_and_xor = {
    z : value;
    x : value;
    v : value;
    w : value;
    y : value;
    yprime : value;
    c : constant;
    s : size;
    sprime : size;
}

type zext_xor = {
    z : value;
    y : value;
    yprime : value;
    x : value;
    s : size;
}

type zext_zext = {
  src : value;
  mid : value;
  dst : value;
  srcty : value_type;
  midty : value_type;
  dstty : value_type;
}

type icmp_inverse = {
  predicate : icmp_pred;
  ty : value_type;
  x : value;
  y : value;
  boolean : const_int;
}

type icmp_inverse_rhs = {
  predicate : icmp_pred;
  ty : value_type;
  x : value;
  y : value;
  boolean : const_int;
}

type icmp_inverse_tgt = {
  predicate : icmp_pred;
  ty : value_type;
  x : value;
  y : value;
  boolean : const_int;
}

type icmp_inverse_rhs_tgt = {
  predicate : icmp_pred;
  ty : value_type;
  x : value;
  y : value;
  boolean : const_int;
}

type icmp_swap_operands = {
  predicate : icmp_pred;
  ty : value_type;
  x : value;
  y : value;
  e : expr;
}

type icmp_swap_operands_rev = {
  predicate : icmp_pred;
  ty : value_type;
  x : value;
  y : value;
  e : expr;
}

type icmp_swap_operands_tgt = {
  predicate : icmp_pred;
  ty : value_type;
  x : value;
  y : value;
  e : expr;
}

type icmp_swap_operands_rev_tgt = {
  predicate : icmp_pred;
  ty : value_type;
  x : value;
  y : value;
  e : expr;
}

type fcmp_swap_operands = {
  predicate : fcmp_pred;
  fty : float_type;
  x : value;
  y : value;
  e : expr;
}

type fcmp_swap_operands_rev = {
  predicate : fcmp_pred;
  fty : float_type;
  x : value;
  y : value;
  e : expr;
}

type fcmp_swap_operands_tgt = {
  predicate : fcmp_pred;
  fty : float_type;
  x : value;
  y : value;
  e : expr;
}

type fcmp_swap_operands_rev_tgt = {
  predicate : fcmp_pred;
  fty : float_type;
  x : value;
  y : value;
  e : expr;
}

type implies_false = {
  c1 : constant;
  c2 : constant;
}

type icmp_eq_add_add = {
    z : value;
    w : value;
    x : value;
    y : value;
    a : value;
    b : value;
    s : size;
}

type icmp_eq_same = {
  ty : value_type;
  x : value;
  y : value;
}

type icmp_eq_same_tgt = {
  ty : value_type;
  x : value;
  y : value;
}

type icmp_eq_srem = {
    z : value;
    w : value;
    x : value;
    y : value;
    s : size;
}

type icmp_eq_sub = {
    z : value;
    x : value;
    a : value;
    b : value;
    s : size;
}

type icmp_eq_sub_sub = {
    z : value;
    w : value;
    x : value;
    y : value;
    a : value;
    b : value;
    s : size;
}

type icmp_eq_xor_not = {
    z : value;
    zprime : value;
    a : value;
    b : value;
    s : size;
}

type icmp_eq_xor_xor = {
    z : value;
    w : value;
    x : value;
    y : value;
    a : value;
    b : value;
    s : size;
}

type icmp_ne_add_add = {
    z : value;
    w : value;
    x : value;
    y : value;
    a : value;
    b : value;
    s : size;
}

type icmp_ne_sub = {
    z : value;
    x : value;
    a : value;
    b : value;
    s : size;
}

type icmp_ne_sub_sub = {
    z : value;
    w : value;
    x : value;
    y : value;
    a : value;
    b : value;
    s : size;
}

type icmp_ne_srem = {
    z : value;
    w : value;
    x : value;
    y : value;
    s : size;
}

type icmp_neq_same = {
  ty : value_type;
  x : value;
  y : value;
}

type icmp_neq_same_tgt = {
  ty : value_type;
  x : value;
  y : value;
}

type icmp_ne_xor = {
    z : value;
    a : value;
    b : value;
    s : size;
}

type icmp_ne_xor_xor = {
    z : value;
    w : value;
    x : value;
    y : value;
    a : value;
    b : value;
    s : size;
}

type icmp_sge_or_not = {
    z : value;
    zprime : value;
    a : value;
    b : value;
    s : size;
}

type icmp_sgt_and_not = {
    z : value;
    zprime : value;
    a : value;
    b : value;
    s : size;
}

type icmp_sle_or_not = {
    z : value;
    zprime : value;
    a : value;
    b : value;
    s : size;
}

type icmp_slt_and_not = {
    z : value;
    zprime : value;
    a : value;
    b : value;
    s : size;
}

type icmp_uge_or_not = {
    z : value;
    zprime : value;
    a : value;
    b : value;
    s : size;
}

type icmp_ugt_and_not = {
    z : value;
    zprime : value;
    a : value;
    b : value;
    s : size;
}

type icmp_ule_or_not = {
    z : value;
    zprime : value;
    a : value;
    b : value;
    s : size;
}

type icmp_ult_and_not = {
    z : value;
    zprime : value;
    a : value;
    b : value;
    s : size;
}


type infrule = [
  | AddSub of add_sub
  | AddCommutativeTgt of add_commutative_tgt
  | AddShift of add_shift
  | AddSignbit of add_signbit
  | AddOnebit of add_onebit
  | AddZextBool of add_zext_bool
  | AddConstNot of add_const_not
  | AddMask of add_mask
  | AddOrAnd of add_or_and
  | AddSelectZero of add_select_zero
  | AddSelectZero2 of add_select_zero2
  | AddDistSub of add_dist_sub
  | AddXorAnd of add_xor_and
  | AndDeMorgan of and_de_morgan
  | AndMone of and_mone
  | AndNot of and_not
  | AndOr of and_or
  | AndOrConst2 of and_or_const2
  | AndSame of and_same
  | AndTrueBool of and_true_bool
  | AndTrueBoolTgt of and_true_bool_tgt
  | AndUndef of and_undef
  | AndXorConst of and_xor_const
  | AndZero of and_zero
  | AndOrNot1 of and_or_not1
  | BitcastBitcast of bitcast_bitcast
  | BitcastDoubleI64 of bitcast_double_i64
  | BitcastLoad of bitcast_load
  | BitcastFpext of bitcast_fpext
  | BitcastFptosi of bitcast_fptosi
  | BitcastFptoui of bitcast_fptoui
  | BitcastFptrunc of bitcast_fptrunc
  | BitcastInttoptr of bitcast_inttoptr
  | BitcastPtrtoint of bitcast_ptrtoint
  | BitcastSext of bitcast_sext
  | BitcastSametype of bitcast_sametype
  | BitcastSitofp of bitcast_sitofp
  | BitcastTrunc of bitcast_trunc
  | BitcastUitofp of bitcast_uitofp
  | BitcastZext of bitcast_zext
  | Bitcastptr of bitcastptr
  | BopAssociative of bop_associative
  | BopCommutative of bop_commutative
  | BopCommutativeRev of bop_commutative_rev
  | BopCommutativeTgt of bop_commutative_tgt
  | BopCommutativeRevTgt of bop_commutative_rev_tgt
  | FbopCommutative of fbop_commutative
  | FbopCommutativeRev of fbop_commutative_rev
  | FbopCommutativeTgt of fbop_commutative_tgt
  | FbopCommutativeRevTgt of fbop_commutative_rev_tgt
  | BopDistributiveOverSelectinst of bop_distributive_over_selectinst
  | BopDistributiveOverSelectinst2 of bop_distributive_over_selectinst2
  | DiffblockUnique of diffblock_unique
  | DiffblockGlobalGlobal of diffblock_global_global
  | DiffblockGlobalUnique of diffblock_global_unique
  | DiffblockLessthan of diffblock_lessthan
  | DiffblockNoalias of diffblock_noalias
  | FaddCommutativeTgt of fadd_commutative_tgt
  | FbopDistributiveOverSelectinst of fbop_distributive_over_selectinst
  | FbopDistributiveOverSelectinst2 of fbop_distributive_over_selectinst2
  | FmulCommutativeTgt of fmul_commutative_tgt
  | FpextBitcast of fpext_bitcast
  | FpextFpext of fpext_fpext
  | FptosiBitcast of fptosi_bitcast
  | FptosiFpext of fptosi_fpext
  | FptouiBitcast of fptoui_bitcast
  | FptouiFpext of fptoui_fpext
  | FptruncBitcast of fptrunc_bitcast
  | FptruncFpext of fptrunc_fpext
  | Gepzero of gepzero
  | GepInboundsRemove of gep_inbounds_remove
  | GepInboundsAdd of gep_inbounds_add
  | IntroGhost of intro_ghost
  | IntroGhostSrc of intro_ghost_src
  | IntroEq of intro_eq
  | IntroEqTgt of intro_eq_tgt
  | InttoptrLoad of inttoptr_load
  | InttoptrBitcast of inttoptr_bitcast
  | InttoptrPtrtoint of inttoptr_ptrtoint
  | InttoptrZext of inttoptr_zext
  | LessthanUndef of lessthan_undef
  | LessthanUndefTgt of lessthan_undef_tgt
  | MulAddDistributive of mul_add_distributive
  | NegVal of neg_val
  | OrAnd of or_and
  | OrAndXor of or_and_xor
  | OrCommutativeTgt of or_commutative_tgt
  | OrFalse of or_false
  | OrFalseTgt of or_false_tgt
  | OrMone of or_mone
  | OrNot of or_not
  | OrOr of or_or
  | OrOr2 of or_or2
  | OrUndef of or_undef
  | OrSame of or_same
  | OrXor of or_xor
  | OrXor2 of or_xor2
  | OrXor3 of or_xor3
  | OrXor4 of or_xor4
  | OrZero of or_zero
  | PtrtointBitcast of ptrtoint_bitcast
  | PtrtointInttoptr of ptrtoint_inttoptr
  | PtrtointLoad of ptrtoint_load
  | PtrtointZero of ptrtoint_zero
  | MulBool of mul_bool
  | MulMone of mul_mone
  | MulNeg of mul_neg
  | MulShl of mul_shl
  | RemNeg of rem_neg
  | Substitute of substitute
  | SubstituteRev of substitute_rev
  | SubstituteTgt of substitute_tgt
  | SdivMone of sdiv_mone
  | SdivSubSrem of sdiv_sub_srem
  | SelectIcmpEq of select_icmp_eq
  | SelectIcmpEqXor1 of select_icmp_eq_xor1
  | SelectIcmpEqXor2 of select_icmp_eq_xor2
  | SelectIcmpNe of select_icmp_ne
  | SelectIcmpNeXor1 of select_icmp_ne_xor1
  | SelectIcmpNeXor2 of select_icmp_ne_xor2
  | SelectIcmpSgtConst of select_icmp_sgt_const
  | SelectIcmpSgtXor1 of select_icmp_sgt_xor1
  | SelectIcmpSgtXor2 of select_icmp_sgt_xor2
  | SelectIcmpSltXor1 of select_icmp_slt_xor1
  | SelectIcmpSltXor2 of select_icmp_slt_xor2
  | SelectIcmpSltConst of select_icmp_slt_const
  | SelectIcmpUgtConst of select_icmp_ugt_const
  | SelectIcmpUltConst of select_icmp_ult_const
  | SextBitcast of sext_bitcast
  | SextSext of sext_sext
  | SextTruncAshr of sext_trunc_ashr
  | SextZext of sext_zext
  | ShiftUndef1 of shift_undef1
  | ShiftUndef2 of shift_undef2
  | ShiftZero1 of shift_zero1
  | ShiftZero2 of shift_zero2
  | SitofpBitcast of sitofp_bitcast
  | SitofpSext of sitofp_sext
  | SitofpZext of sitofp_zext
  | SubAdd of sub_add
  | SubConstAdd of sub_const_add
  | SubConstNot of sub_const_not
  | SubMone of sub_mone
  | SubOnebit of sub_onebit
  | SubRemove of sub_remove
  | SubSdiv of sub_sdiv
  | SubShl of sub_shl
  | SubOrXor of sub_or_xor
  | SubSub of sub_sub
  | Transitivity of transitivity
  | TransitivityTgt of transitivity_tgt
  | TransitivityPointerLhs of transitivity_pointer_lhs
  | TransitivityPointerRhs of transitivity_pointer_rhs
  | TruncBitcast of trunc_bitcast
  | TruncOnebit of trunc_onebit
  | TruncPtrtoint of trunc_ptrtoint
  | TruncSext of trunc_sext
  | TruncTrunc of trunc_trunc
  | TruncZext of trunc_zext
  | UdivSubUrem of udiv_sub_urem
  | UdivZext of udiv_zext
  | UdivZextConst of udiv_zext_const
  | UitofpBitcast of uitofp_bitcast
  | UitofpZext of uitofp_zext
  | UremZext of urem_zext
  | UremZextConst of urem_zext_const
  | XorCommutativeTgt of xor_commutative_tgt
  | XorNot of xor_not
  | XorSame of xor_same
  | XorUndef of xor_undef
  | XorZero of xor_zero
  | ZextBitcast of zext_bitcast
  | ZextTruncAnd of zext_trunc_and
  | ZextTruncAndXor of zext_trunc_and_xor
  | ZextXor of zext_xor
  | ZextZext of zext_zext
  | IcmpInverse of icmp_inverse
  | IcmpInverseRhs of icmp_inverse_rhs
  | IcmpInverseTgt of icmp_inverse_tgt
  | IcmpInverseRhsTgt of icmp_inverse_rhs_tgt
  | IcmpSwapOperands of icmp_swap_operands
  | IcmpSwapOperandsRev of icmp_swap_operands_rev
  | IcmpSwapOperandsTgt of icmp_swap_operands_tgt
  | IcmpSwapOperandsRevTgt of icmp_swap_operands_rev_tgt
  | FcmpSwapOperands of fcmp_swap_operands
  | FcmpSwapOperandsRev of fcmp_swap_operands_rev
  | FcmpSwapOperandsTgt of fcmp_swap_operands_tgt
  | FcmpSwapOperandsRevTgt of fcmp_swap_operands_rev_tgt
  | ImpliesFalse of implies_false
  | IcmpEqAddAdd of icmp_eq_add_add
  | IcmpEqSrem of icmp_eq_srem
  | IcmpEqSub of icmp_eq_sub
  | IcmpEqSubSub of icmp_eq_sub_sub
  | IcmpEqSame of icmp_eq_same
  | IcmpEqSameTgt of icmp_eq_same_tgt
  | IcmpEqXorNot of icmp_eq_xor_not
  | IcmpEqXorXor of icmp_eq_xor_xor
  | IcmpNeAddAdd of icmp_ne_add_add
  | IcmpNeSrem of icmp_ne_srem
  | IcmpNeSub of icmp_ne_sub
  | IcmpNeSubSub of icmp_ne_sub_sub
  | IcmpNeqSame of icmp_neq_same
  | IcmpNeqSameTgt of icmp_neq_same_tgt
  | IcmpNeXor of icmp_ne_xor
  | IcmpNeXorXor of icmp_ne_xor_xor
  | IcmpSgeOrNot of icmp_sge_or_not
  | IcmpSgtAndNot of icmp_sgt_and_not
  | IcmpSleOrNot of icmp_sle_or_not
  | IcmpSltAndNot of icmp_slt_and_not
  | IcmpUgeOrNot of icmp_uge_or_not
  | IcmpUgtAndNot of icmp_ugt_and_not
  | IcmpUleOrNot of icmp_ule_or_not
  | IcmpUltAndNot of icmp_ult_and_not
  ] <ocaml repr="classic">

type return_code_type = [ACTUAL | ADMITTED | FAIL] <ocaml repr="classic">

type hint_command = [
  | Propagate of propagate
  | Infrule of (position * infrule)
  ] <ocaml repr="classic">

type cpp_debug_info = {
  file_name : string;
  line_number : int;
}

type auto_opt = [AUTO_GVN | AUTO_SROA | AUTO_LICM | AUTO_INSTCOMBINE | AUTO_DEFAULT] <ocaml repr="classic">

type postprop_opt = [ POSTPROP_GVN | POSTPROP_NONE ] <ocaml repr="classic">

type postprop_info = {
  opt : postprop_opt;
  itrnum : int;
}

type hints = {
  module_id : string;
  function_id : string;
  opt_name : string;
  ~description : string;
  return_code : return_code_type;
  ~auto_option <ocaml default="AUTO_DEFAULT"> : auto_opt;
  postprop_option : postprop_info;
  nop_positions: position list; (* insert after position *)

  commands : (hint_command * cpp_debug_info) list;
}