open Preamble open BitVectorTrie open Graphs open Order open Registers open FrontEndVal open Hide open ByteValues open GenMem open FrontEndMem open Division open Z open BitVectorZ open Pointers open Coqlib open Values open FrontEndOps open CostLabel open Proper open PositiveMap open Deqsets open ErrorMessages open PreIdentifiers open Errors open Extralib open Lists open Positive open Identifiers open Exp open Arithmetic open Vector open Div_and_mod open Util open FoldStuff open BitVector open Jmeq open Russell open List open Setoids open Monad open Option open Extranat open Bool open Relations open Nat open Integers open Types open AST open Hints_declaration open Core_notation open Pts open Logic open RTLabs_syntax open Extra_bool open Globalenvs open String open Sets open Listb open LabelledObjects open I8051 open BackEndOps open Joint open RTL open Deqsets_extra open State open Bind_new open BindLists open Blocks open TranslateUtils val size_of_sig_type : AST.typ -> Nat.nat val sign_of_sig_type : AST.typ -> AST.signedness type register_type = | Register_int of Registers.register | Register_ptr of Registers.register * Registers.register val register_type_rect_Type4 : (Registers.register -> 'a1) -> (Registers.register -> Registers.register -> 'a1) -> register_type -> 'a1 val register_type_rect_Type5 : (Registers.register -> 'a1) -> (Registers.register -> Registers.register -> 'a1) -> register_type -> 'a1 val register_type_rect_Type3 : (Registers.register -> 'a1) -> (Registers.register -> Registers.register -> 'a1) -> register_type -> 'a1 val register_type_rect_Type2 : (Registers.register -> 'a1) -> (Registers.register -> Registers.register -> 'a1) -> register_type -> 'a1 val register_type_rect_Type1 : (Registers.register -> 'a1) -> (Registers.register -> Registers.register -> 'a1) -> register_type -> 'a1 val register_type_rect_Type0 : (Registers.register -> 'a1) -> (Registers.register -> Registers.register -> 'a1) -> register_type -> 'a1 val register_type_inv_rect_Type4 : register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 val register_type_inv_rect_Type3 : register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 val register_type_inv_rect_Type2 : register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 val register_type_inv_rect_Type1 : register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 val register_type_inv_rect_Type0 : register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 val register_type_discr : register_type -> register_type -> __ val register_type_jmdiscr : register_type -> register_type -> __ type local_env = Registers.register List.list Identifiers.identifier_map val find_local_env : PreIdentifiers.identifier -> local_env -> Registers.register List.list val find_local_env_arg : Registers.register -> local_env -> Joint.psd_argument List.list val m_iter : Monad.monad -> ('a1 -> __) -> Nat.nat -> __ -> __ val fresh_registers : Joint.params -> AST.ident List.list -> Nat.nat -> Registers.register List.list Monad.smax_def__o__monad val map_list_local_env : Registers.register List.list Identifiers.identifier_map -> (Registers.register, AST.typ) Types.prod List.list -> Registers.register List.list val initialize_local_env : AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list -> local_env Monad.smax_def__o__monad val initialize_locals_params_ret : AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list -> (Registers.register, AST.typ) Types.prod Types.option -> local_env Monad.smax_def__o__monad val make_addr : 'a1 List.list -> ('a1, 'a1) Types.prod val find_and_addr : PreIdentifiers.identifier -> local_env -> (Registers.register, Registers.register) Types.prod val find_and_addr_arg : Registers.register -> local_env -> (Joint.psd_argument, Joint.psd_argument) Types.prod val rtl_args : Registers.register List.list -> local_env -> Joint.psd_argument List.list val vrsplit : Nat.nat -> Nat.nat -> 'a1 Vector.vector -> 'a1 Vector.vector List.list Types.sig0 val split_into_bytes : AST.intsize -> AST.bvint -> BitVector.byte List.list Types.sig0 val list_inject_All_aux : 'a1 List.list -> 'a1 Types.sig0 List.list val translate_op_aux : AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list -> Joint.psd_argument List.list -> Joint.psd_argument List.list -> Joint.joint_seq List.list val translate_op : AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list -> Joint.psd_argument List.list -> Joint.psd_argument List.list -> Joint.joint_seq List.list val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list val translate_op_asym_unsigned : AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list -> Joint.psd_argument List.list -> Joint.psd_argument List.list -> Joint.joint_seq List.list val zero_args : Nat.nat -> Joint.psd_argument List.list Types.sig0 val one_args : Nat.nat -> Joint.psd_argument List.list Types.sig0 val size_of_cst : AST.typ -> FrontEndOps.constant -> Nat.nat val translate_cst : AST.typ -> AST.ident List.list -> FrontEndOps.constant Types.sig0 -> Registers.register List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val translate_move : AST.ident List.list -> Registers.register List.list -> Joint.psd_argument List.list -> Joint.joint_seq List.list val sign_mask : AST.ident List.list -> Registers.register -> Joint.psd_argument -> Joint.joint_seq List.list val translate_cast_signed : AST.ident List.list -> Registers.register List.list -> Joint.psd_argument -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val translate_fill_with_zero : AST.ident List.list -> Registers.register List.list -> Joint.joint_seq List.list val last : 'a1 List.list -> 'a1 Types.option val translate_op_asym_signed : AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list -> Joint.psd_argument List.list -> Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val translate_cast : AST.ident List.list -> AST.signedness -> Registers.register List.list -> Registers.register List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val translate_notint : AST.ident List.list -> Registers.register List.list -> Registers.register List.list -> Joint.joint_seq List.list val translate_negint : AST.ident List.list -> Registers.register List.list -> Registers.register List.list -> Joint.joint_seq List.list val translate_notbool : AST.ident List.list -> Registers.register List.list -> Registers.register List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val translate_op1 : AST.ident List.list -> AST.typ -> AST.typ -> FrontEndOps.unary_operation -> Registers.register List.list -> Registers.register List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val translate_mul_i : AST.ident List.list -> Registers.register -> Registers.register -> Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list -> Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 -> Joint.joint_seq List.list -> Joint.joint_seq List.list val translate_mul : AST.ident List.list -> Registers.register List.list -> Joint.psd_argument List.list -> Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val translate_divumodu8 : AST.ident List.list -> Bool.bool -> Registers.register List.list -> Joint.psd_argument List.list -> Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val foldr2 : ('a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> 'a1 List.list -> 'a2 List.list -> 'a3 val translate_ne : AST.ident List.list -> Registers.register List.list -> Joint.psd_argument List.list -> Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val translate_toggle_bool : AST.ident List.list -> Registers.register List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val translate_lt_unsigned : AST.ident List.list -> Registers.register List.list -> Joint.psd_argument List.list -> Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val shift_signed : AST.ident List.list -> Registers.register -> Joint.psd_argument List.list -> (Joint.psd_argument List.list, Joint.joint_seq List.list) Types.prod Types.sig0 val translate_lt_signed : AST.ident List.list -> Registers.register List.list -> Joint.psd_argument List.list -> Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val translate_lt : Bool.bool -> AST.ident List.list -> Registers.register List.list -> Joint.psd_argument List.list -> Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val translate_cmp : Bool.bool -> AST.ident List.list -> Integers.comparison -> Registers.register List.list -> Joint.psd_argument List.list -> Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq) BindLists.bind_list val translate_op2 : AST.ident List.list -> AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation -> Registers.register List.list -> Joint.psd_argument List.list -> Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val translate_cond : AST.ident List.list -> Registers.register List.list -> Graphs.label -> Blocks.bind_step_block val translate_load : AST.ident List.list -> Joint.psd_argument List.list -> Registers.register List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val translate_store : AST.ident List.list -> Joint.psd_argument List.list -> Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new val ensure_bind_step_block : Joint.params -> AST.ident List.list -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new -> Blocks.bind_step_block val translate_statement : AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list -> local_env -> RTLabs_syntax.statement -> ((Blocks.bind_step_block, Blocks.bind_fin_block) Types.sum, __) Types.dPair val translate_internal : AST.ident List.list -> RTLabs_syntax.internal_function -> Joint.joint_closed_internal_function val rtlabs_to_rtl : CostLabel.costlabel -> RTLabs_syntax.rTLabs_program -> RTL.rtl_program