Require Import String.
Require Import Coqlib.
Require Import Errors.
Require Import Integers.
Require Import Floats.

Set Implicit Arguments.

Syntactic elements

Definition ident := positive.

Definition ident_eq := peq.


Inductive typ : Type :=
  | Tint (* 32-bit integers or pointers *)
  | Tfloat (* 64-bit double-precision floats *)
  | Tlong (* 64-bit integers *)
  | Tsingle (* 32-bit single-precision floats *)
  | Tany32 (* any 32-bit value *)
  | Tany64. (* any 64-bit value, i.e. any value *)

Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}.
Global Opaque typ_eq.

Definition opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}
                     := option_eq typ_eq.

Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2}
                     := list_eq_dec typ_eq.

Definition typesize (ty: typ) : Z :=
  match ty with
  | Tint => 4
  | Tfloat => 8
  | Tlong => 8
  | Tsingle => 4
  | Tany32 => 4
  | Tany64 => 8
  end.

Lemma typesize_pos: forall ty, typesize ty > 0.


Definition subtype (ty1 ty2: typ) : bool :=
  match ty1, ty2 with
  | Tint, Tint => true
  | Tlong, Tlong => true
  | Tfloat, Tfloat => true
  | Tsingle, Tsingle => true
  | (Tint | Tsingle | Tany32), Tany32 => true
  | _, Tany64 => true
  | _, _ => false
  end.

Fixpoint subtype_list (tyl1 tyl2: list typ) : bool :=
  match tyl1, tyl2 with
  | nil, nil => true
  | ty1::tys1, ty2::tys2 => subtype ty1 ty2 && subtype_list tys1 tys2
  | _, _ => false
  end.


Record calling_convention : Type := mkcallconv {
  cc_vararg: bool; (* variable-arity function *)
  cc_unproto: bool; (* old-style unprototyped function *)
  cc_structret: bool (* function returning a struct *)
}.

Definition cc_default :=
  {| cc_vararg := false; cc_unproto := false; cc_structret := false |}.

Record signature : Type := mksignature {
  sig_args: list typ;
  sig_res: option typ;
  sig_cc: calling_convention
}.

Definition proj_sig_res (s: signature) : typ :=
  match s.(sig_res) with
  | None => Tint
  | Some t => t
  end.

Definition signature_eq: forall (s1 s2: signature), {s1=s2} + {s1<>s2}.
Global Opaque signature_eq.

Definition signature_main :=
  {| sig_args := nil; sig_res := Some Tint; sig_cc := cc_default |}.


Inductive memory_chunk : Type :=
  | Mint8signed (* 8-bit signed integer *)
  | Mint8unsigned (* 8-bit unsigned integer *)
  | Mint16signed (* 16-bit signed integer *)
  | Mint16unsigned (* 16-bit unsigned integer *)
  | Mint32 (* 32-bit integer, or pointer *)
  | Mint64 (* 64-bit integer *)
  | Mfloat32 (* 32-bit single-precision float *)
  | Mfloat64 (* 64-bit double-precision float *)
  | Many32 (* any value that fits in 32 bits *)
  | Many64. (* any value *)

Definition chunk_eq: forall (c1 c2: memory_chunk), {c1=c2} + {c1<>c2}.
Global Opaque chunk_eq.


Definition type_of_chunk (c: memory_chunk) : typ :=
  match c with
  | Mint8signed => Tint
  | Mint8unsigned => Tint
  | Mint16signed => Tint
  | Mint16unsigned => Tint
  | Mint32 => Tint
  | Mint64 => Tlong
  | Mfloat32 => Tsingle
  | Mfloat64 => Tfloat
  | Many32 => Tany32
  | Many64 => Tany64
  end.


Definition chunk_of_type (ty: typ) :=
  match ty with
  | Tint => Mint32
  | Tfloat => Mfloat64
  | Tlong => Mint64
  | Tsingle => Mfloat32
  | Tany32 => Many32
  | Tany64 => Many64
  end.


Inductive init_data: Type :=
  | Init_int8: int -> init_data
  | Init_int16: int -> init_data
  | Init_int32: int -> init_data
  | Init_int64: int64 -> init_data
  | Init_float32: float32 -> init_data
  | Init_float64: float -> init_data
  | Init_space: Z -> init_data
  | Init_addrof: ident -> int -> init_data. (* address of symbol + offset *)


Record globvar (V: Type) : Type := mkglobvar {
  gvar_info: V; (* language-dependent info, e.g. a type *)
  gvar_init: list init_data; (* initialization data *)
  gvar_readonly: bool; (* read-only variable? (const) *)
  gvar_volatile: bool (* volatile variable? *)
}.


Inductive globdef (F V: Type) : Type :=
  | Gfun (f: F)
  | Gvar (v: globvar V).

Implicit Arguments Gfun [F V].
Implicit Arguments Gvar [F V].

Record program (F V: Type) : Type := mkprogram {
  prog_defs: list (ident * globdef F V);
  prog_public: list ident;
  prog_main: ident
}.

Definition prog_defs_names (F V: Type) (p: program F V) : list ident :=
  List.map fst p.(prog_defs).

Generic transformations over programs

Section TRANSF_PROGRAM.

Variable A B V: Type.
Variable transf: A -> B.

Definition transform_program_globdef (idg: ident * globdef A V) : ident * globdef B V :=
  match idg with
  | (id, Gfun f) => (id, Gfun (transf f))
  | (id, Gvar v) => (id, Gvar v)
  end.

Definition transform_program (p: program A V) : program B V :=
  mkprogram
    (List.map transform_program_globdef p.(prog_defs))
    p.(prog_public)
    p.(prog_main).

Lemma transform_program_function:
  forall p i tf,
  In (i, Gfun tf) (transform_program p).(prog_defs) ->
  exists f, In (i, Gfun f) p.(prog_defs) /\ transf f = tf.

End TRANSF_PROGRAM.


Section TRANSF_PROGRAM_IDENT.

Variable A B V: Type.
Variable transf: ident -> A -> B.

Definition transform_program_globdef_ident (idg: ident * globdef A V) : ident * globdef B V :=
  match idg with
  | (id, Gfun f) => (id, Gfun (transf id f))
  | (id, Gvar v) => (id, Gvar v)
  end.

Definition transform_program_ident (p: program A V): program B V :=
  mkprogram
    (List.map transform_program_globdef_ident p.(prog_defs))
    p.(prog_public)
    p.(prog_main).

Lemma tranforma_program_function_ident:
  forall p i tf,
  In (i, Gfun tf) (transform_program_ident p).(prog_defs) ->
  exists f, In (i, Gfun f) p.(prog_defs) /\ transf i f = tf.

End TRANSF_PROGRAM_IDENT.


Local Open Scope error_monad_scope.

Section TRANSF_PROGRAM_GEN.

Variables A B V W: Type.
Variable transf_fun: A -> res B.
Variable transf_fun_ident: ident -> A -> res B.
Variable transf_var: V -> res W.
Variable transf_var_ident: ident -> V -> res W.

Definition transf_globvar (g: globvar V) : res (globvar W) :=
  do info' <- transf_var g.(gvar_info);
  OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)).

Definition transf_globvar_ident (i: ident) (g: globvar V) : res (globvar W) :=
  do info' <- transf_var_ident i g.(gvar_info);
  OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)).

Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) :=
  match l with
  | nil => OK nil
  | (id, Gfun f) :: l' =>
      match transf_fun f with
      | Error msg => Error (MSG "In function " :: CTX id :: MSG ": " :: msg)
      | OK tf =>
          do tl' <- transf_globdefs l'; OK ((id, Gfun tf) :: tl')
      end
  | (id, Gvar v) :: l' =>
      match transf_globvar v with
      | Error msg => Error (MSG "In variable " :: CTX id :: MSG ": " :: msg)
      | OK tv =>
          do tl' <- transf_globdefs l'; OK ((id, Gvar tv) :: tl')
      end
  end.

Fixpoint transf_globdefs_ident (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) :=
  match l with
  | nil => OK nil
  | (id, Gfun f) :: l' =>
    match transf_fun_ident id f with
      | Error msg => Error (MSG "In function " :: CTX id :: MSG ": " :: msg)
      | OK tf =>
        do tl' <- transf_globdefs_ident l'; OK ((id, Gfun tf) :: tl')
    end
  | (id, Gvar v) :: l' =>
    match transf_globvar_ident id v with
      | Error msg => Error (MSG "In variable " :: CTX id :: MSG ": " :: msg)
      | OK tv =>
        do tl' <- transf_globdefs_ident l'; OK ((id, Gvar tv) :: tl')
    end
  end.

Definition transform_partial_program2 (p: program A V) : res (program B W) :=
  do gl' <- transf_globdefs p.(prog_defs);
  OK (mkprogram gl' p.(prog_public) p.(prog_main)).

Definition transform_partial_ident_program2 (p: program A V) : res (program B W) :=
  do gl' <- transf_globdefs_ident p.(prog_defs);
  OK (mkprogram gl' p.(prog_public) p.(prog_main)).

Lemma transform_partial_program2_function:
  forall p tp i tf,
  transform_partial_program2 p = OK tp ->
  In (i, Gfun tf) tp.(prog_defs) ->
  exists f, In (i, Gfun f) p.(prog_defs) /\ transf_fun f = OK tf.

Lemma transform_partial_ident_program2_function:
  forall p tp i tf,
  transform_partial_ident_program2 p = OK tp ->
  In (i, Gfun tf) tp.(prog_defs) ->
  exists f, In (i, Gfun f) p.(prog_defs) /\ transf_fun_ident i f = OK tf.

Lemma transform_partial_program2_variable:
  forall p tp i tv,
  transform_partial_program2 p = OK tp ->
  In (i, Gvar tv) tp.(prog_defs) ->
  exists v,
     In (i, Gvar(mkglobvar v tv.(gvar_init) tv.(gvar_readonly) tv.(gvar_volatile))) p.(prog_defs)
  /\ transf_var v = OK tv.(gvar_info).


Lemma transform_partial_ident_program2_variable:
  forall p tp i tv,
  transform_partial_ident_program2 p = OK tp ->
  In (i, Gvar tv) tp.(prog_defs) ->
  exists v,
     In (i, Gvar(mkglobvar v tv.(gvar_init) tv.(gvar_readonly) tv.(gvar_volatile))) p.(prog_defs)
  /\ transf_var_ident i v = OK tv.(gvar_info).

Lemma transform_partial_program2_succeeds:
  forall p tp i g,
  transform_partial_program2 p = OK tp ->
  In (i, g) p.(prog_defs) ->
  match g with
  | Gfun fd => exists tfd, transf_fun fd = OK tfd
  | Gvar gv => exists tv, transf_var gv.(gvar_info) = OK tv
  end.

Lemma transform_partial_ident_program2_succeeds:
  forall p tp i g,
  transform_partial_ident_program2 p = OK tp ->
  In (i, g) p.(prog_defs) ->
  match g with
  | Gfun fd => exists tfd, transf_fun_ident i fd = OK tfd
  | Gvar gv => exists tv, transf_var_ident i gv.(gvar_info) = OK tv
  end.

Lemma transform_partial_program2_main:
  forall p tp,
  transform_partial_program2 p = OK tp ->
  tp.(prog_main) = p.(prog_main).

Lemma transform_partial_ident_program2_main:
  forall p tp,
  transform_partial_ident_program2 p = OK tp ->
  tp.(prog_main) = p.(prog_main).

Lemma transform_partial_program2_public:
  forall p tp,
  transform_partial_program2 p = OK tp ->
  tp.(prog_public) = p.(prog_public).

Lemma transform_partial_ident_program2_public:
  forall p tp,
  transform_partial_ident_program2 p = OK tp ->
  tp.(prog_public) = p.(prog_public).


Section AUGMENT.

Variable new_globs: list(ident * globdef B W).
Variable new_main: ident.

Definition transform_partial_augment_program (p: program A V) : res (program B W) :=
  do gl' <- transf_globdefs p.(prog_defs);
  OK(mkprogram (gl' ++ new_globs) p.(prog_public) new_main).

Lemma transform_partial_augment_program_main:
  forall p tp,
  transform_partial_augment_program p = OK tp ->
  tp.(prog_main) = new_main.

Definition transform_partial_augment_ident_program (p: program A V) : res (program B W) :=
  do gl' <- transf_globdefs_ident p.(prog_defs);
  OK(mkprogram (gl' ++ new_globs) p.(prog_public) new_main).

Lemma transform_partial_augment_ident_program_main:
  forall p tp,
  transform_partial_augment_ident_program p = OK tp ->
  tp.(prog_main) = new_main.

End AUGMENT.

Remark transform_partial_program2_augment:
  forall p,
  transform_partial_program2 p =
  transform_partial_augment_program nil p.(prog_main) p.

Remark transform_partial_ident_program2_augment:
  forall p,
  transform_partial_ident_program2 p =
  transform_partial_augment_ident_program nil p.(prog_main) p.

End TRANSF_PROGRAM_GEN.


Section TRANSF_PARTIAL_PROGRAM.

Variable A B V: Type.
Variable transf_partial: A -> res B.
Variable transf_partial_ident: ident -> A -> res B.

Definition transform_partial_program (p: program A V) : res (program B V) :=
  transform_partial_program2 transf_partial (fun v => OK v) p.

Definition transform_partial_ident_program (p: program A V) : res (program B V) :=
  transform_partial_ident_program2 transf_partial_ident (fun _ v => OK v) p.

Lemma transform_partial_program_main:
  forall p tp,
  transform_partial_program p = OK tp ->
  tp.(prog_main) = p.(prog_main).

Lemma transform_partial_ident_program_main:
  forall p tp,
  transform_partial_ident_program p = OK tp ->
  tp.(prog_main) = p.(prog_main).

Lemma transform_partial_program_public:
  forall p tp,
  transform_partial_program p = OK tp ->
  tp.(prog_public) = p.(prog_public).

Lemma transform_partial_ident_program_public:
  forall p tp,
  transform_partial_ident_program p = OK tp ->
  tp.(prog_public) = p.(prog_public).

Lemma transform_partial_program_function:
  forall p tp i tf,
  transform_partial_program p = OK tp ->
  In (i, Gfun tf) tp.(prog_defs) ->
  exists f, In (i, Gfun f) p.(prog_defs) /\ transf_partial f = OK tf.

Lemma transform_partial_ident_program_function:
  forall p tp i tf,
  transform_partial_ident_program p = OK tp ->
  In (i, Gfun tf) tp.(prog_defs) ->
  exists f, In (i, Gfun f) p.(prog_defs) /\ transf_partial_ident i f = OK tf.

Lemma transform_partial_program_succeeds:
  forall p tp i fd,
  transform_partial_program p = OK tp ->
  In (i, Gfun fd) p.(prog_defs) ->
  exists tfd, transf_partial fd = OK tfd.

Lemma transform_partial_ident_program_succeeds:
  forall p tp i fd,
  transform_partial_ident_program p = OK tp ->
  In (i, Gfun fd) p.(prog_defs) ->
  exists tfd, transf_partial_ident i fd = OK tfd.

End TRANSF_PARTIAL_PROGRAM.

Lemma transform_program_partial_program:
  forall (A B V: Type) (transf: A -> B) (p: program A V),
  transform_partial_program (fun f => OK(transf f)) p = OK(transform_program transf p).

Lemma transform_program_partial_ident_program:
  forall (A B V: Type) (transf: ident -> A -> B) (p: program A V),
  transform_partial_ident_program (fun id f => OK(transf id f)) p = OK(transform_program_ident transf p).


Section MATCH_PROGRAM.

Variable A B V W: Type.
Variable match_fundef: A -> B -> Prop.
Variable match_varinfo: V -> W -> Prop.

Inductive match_globdef: ident * globdef A V -> ident * globdef B W -> Prop :=
  | match_glob_fun: forall id f1 f2,
      match_fundef f1 f2 ->
      match_globdef (id, Gfun f1) (id, Gfun f2)
  | match_glob_var: forall id init ro vo info1 info2,
      match_varinfo info1 info2 ->
      match_globdef (id, Gvar (mkglobvar info1 init ro vo)) (id, Gvar (mkglobvar info2 init ro vo)).

Definition match_program (new_globs : list (ident * globdef B W))
                         (new_main : ident)
                         (p1: program A V) (p2: program B W) : Prop :=
  (exists tglob, list_forall2 match_globdef p1.(prog_defs) tglob /\
                 p2.(prog_defs) = tglob ++ new_globs) /\
  p2.(prog_main) = new_main /\
  p2.(prog_public) = p1.(prog_public).

End MATCH_PROGRAM.

Lemma transform_partial_augment_program_match:
  forall (A B V W: Type)
         (transf_fun: A -> res B)
         (transf_var: V -> res W)
         (p: program A V)
         (new_globs : list (ident * globdef B W))
         (new_main : ident)
         (tp: program B W),
  transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK tp ->
  match_program
    (fun fd tfd => transf_fun fd = OK tfd)
    (fun info tinfo => transf_var info = OK tinfo)
    new_globs new_main
    p tp.

External functions

Inductive external_function : Type :=
  | EF_external (name: string) (sg: signature)
  | EF_builtin (name: string) (sg: signature)
  | EF_vload (chunk: memory_chunk)
  | EF_vstore (chunk: memory_chunk)
  | EF_malloc
  | EF_free
  | EF_memcpy (sz: Z) (al: Z)
  | EF_annot (text: string) (targs: list typ)
  | EF_annot_val (text: string) (targ: typ)
  | EF_inline_asm (text: string) (sg: signature) (clobbers: list string)
  | EF_debug (kind: positive) (text: ident) (targs: list typ).


Definition ef_sig (ef: external_function): signature :=
  match ef with
  | EF_external name sg => sg
  | EF_builtin name sg => sg
  | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default
  | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default
  | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default
  | EF_free => mksignature (Tint :: nil) None cc_default
  | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default
  | EF_annot text targs => mksignature targs None cc_default
  | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default
  | EF_inline_asm text sg clob => sg
  | EF_debug kind text targs => mksignature targs None cc_default
  end.


Definition ef_inline (ef: external_function) : bool :=
  match ef with
  | EF_external name sg => false
  | EF_builtin name sg => true
  | EF_vload chunk => true
  | EF_vstore chunk => true
  | EF_malloc => false
  | EF_free => false
  | EF_memcpy sz al => true
  | EF_annot text targs => true
  | EF_annot_val text targ => true
  | EF_inline_asm text sg clob => true
  | EF_debug kind text targs => true
  end.


Definition ef_reloads (ef: external_function) : bool :=
  match ef with
  | EF_annot text targs => false
  | EF_debug kind text targs => false
  | _ => true
  end.


Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}.
Global Opaque external_function_eq.


Inductive fundef (F: Type): Type :=
  | Internal: F -> fundef F
  | External: external_function -> fundef F.

Implicit Arguments External [F].

Section TRANSF_FUNDEF.

Variable A B: Type.
Variable transf: A -> B.

Definition transf_fundef (fd: fundef A): fundef B :=
  match fd with
  | Internal f => Internal (transf f)
  | External ef => External ef
  end.

End TRANSF_FUNDEF.

Section TRANSF_PARTIAL_FUNDEF.

Variable A B: Type.
Variable transf_partial: A -> res B.

Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
  match fd with
  | Internal f => do f' <- transf_partial f; OK (Internal f')
  | External ef => OK (External ef)
  end.

End TRANSF_PARTIAL_FUNDEF.

Arguments and results to builtin functions

Set Contextual Implicit.

Inductive builtin_arg (A: Type) : Type :=
  | BA (x: A)
  | BA_int (n: int)
  | BA_long (n: int64)
  | BA_float (f: float)
  | BA_single (f: float32)
  | BA_loadstack (chunk: memory_chunk) (ofs: int)
  | BA_addrstack (ofs: int)
  | BA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: int)
  | BA_addrglobal (id: ident) (ofs: int)
  | BA_splitlong (hi lo: builtin_arg A).

Inductive builtin_res (A: Type) : Type :=
  | BR (x: A)
  | BR_none
  | BR_splitlong (hi lo: builtin_res A).

Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident :=
  match a with
  | BA_loadglobal chunk id ofs => id :: nil
  | BA_addrglobal id ofs => id :: nil
  | BA_splitlong hi lo => globals_of_builtin_arg hi ++ globals_of_builtin_arg lo
  | _ => nil
  end.

Definition globals_of_builtin_args (A: Type) (al: list (builtin_arg A)) : list ident :=
  List.fold_right (fun a l => globals_of_builtin_arg a ++ l) nil al.

Fixpoint params_of_builtin_arg (A: Type) (a: builtin_arg A) : list A :=
  match a with
  | BA x => x :: nil
  | BA_splitlong hi lo => params_of_builtin_arg hi ++ params_of_builtin_arg lo
  | _ => nil
  end.

Definition params_of_builtin_args (A: Type) (al: list (builtin_arg A)) : list A :=
  List.fold_right (fun a l => params_of_builtin_arg a ++ l) nil al.

Fixpoint params_of_builtin_res (A: Type) (a: builtin_res A) : list A :=
  match a with
  | BR x => x :: nil
  | BR_none => nil
  | BR_splitlong hi lo => params_of_builtin_res hi ++ params_of_builtin_res lo
  end.

Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_arg B :=
  match a with
  | BA x => BA (f x)
  | BA_int n => BA_int n
  | BA_long n => BA_long n
  | BA_float n => BA_float n
  | BA_single n => BA_single n
  | BA_loadstack chunk ofs => BA_loadstack chunk ofs
  | BA_addrstack ofs => BA_addrstack ofs
  | BA_loadglobal chunk id ofs => BA_loadglobal chunk id ofs
  | BA_addrglobal id ofs => BA_addrglobal id ofs
  | BA_splitlong hi lo =>
      BA_splitlong (map_builtin_arg f hi) (map_builtin_arg f lo)
  end.

Fixpoint map_builtin_res (A B: Type) (f: A -> B) (a: builtin_res A) : builtin_res B :=
  match a with
  | BR x => BR (f x)
  | BR_none => BR_none
  | BR_splitlong hi lo =>
      BR_splitlong (map_builtin_res f hi) (map_builtin_res f lo)
  end.


Inductive builtin_arg_constraint : Type :=
  | OK_default
  | OK_const
  | OK_addrstack
  | OK_addrglobal
  | OK_addrany
  | OK_all.

Definition builtin_arg_ok
       (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) :=
  match ba, c with
  | (BA _ | BA_splitlong _ _), _ => true
  | (BA_int _ | BA_long _ | BA_float _ | BA_single _), OK_const => true
  | BA_addrstack _, (OK_addrstack | OK_addrany) => true
  | BA_addrglobal _ _, (OK_addrglobal | OK_addrany) => true
  | _, OK_all => true
  | _, _ => false
  end.