Require Import Axioms CoqlibC MapsC Errors.
Require Import AST Linking.
Require Archi.
newly added *
Require Export Ctypes Csyntax.
Require Import Errors.
Require Import Values.
Require Import sflib.
Require Import Skeleton ASTC.
Set Implicit Arguments.
Generalizable Variables F.
Definition fundef_of_fundef F (
f:
Ctypes.fundef F):
AST.fundef F :=
match f with
|
Internal f =>
AST.Internal f
|
External ef _ _ _ =>
AST.External ef
end.
Coercion fundef_of_fundef:
Ctypes.fundef >->
AST.fundef.
Definition globdef_of_globdef F V (
gd:
globdef (
Ctypes.fundef F)
V) :
globdef (
AST.fundef F)
V :=
match gd with
|
Gfun fd =>
Gfun (
fundef_of_fundef fd)
|
Gvar v =>
Gvar v
end.
Global Instance fundef_HasExternal {
F}:
HasExternal (
Ctypes.fundef F) :=
Build_HasExternal (
fun fd =>
is_external_fd (
fundef_of_fundef fd)).
Module CSk.
Definition of_program {
F} (
get_sg:
F ->
signature) (
prog:
Ctypes.program F):
Sk.t :=
mkprogram (
skdefs_of_gdefs (
get_sg) (
map (
update_snd (@
globdef_of_globdef F type))
prog.(
prog_defs)))
prog.(
prog_public)
prog.(
prog_main).
Lemma of_program_defs
F get_sg (
p:
Ctypes.program F):
(
of_program get_sg p).(
defs) =
p.(
defs).
Proof.
Let match_fundef F0 F1 (
get_sig:
F0 ->
F1) (
_:
unit):
Ctypes.fundef F0 ->
AST.fundef F1 ->
Prop :=
fun f0 f1 =>
match f0,
f1 with
|
Internal func0,
AST.Internal func1 =>
get_sig func0 =
func1
|
External ef0 _ _ _,
AST.External ef1 =>
external_function_eq ef0 ef1
|
_,
_ =>
false
end.
Definition wf_match_fundef CTX F1 F2 (
match_fundef:
CTX ->
Ctypes.fundef F1 ->
Ctypes.fundef F2 ->
Prop)
(
fn_sig1:
F1 ->
signature) (
fn_sig2:
F2 ->
signature):
Prop :=
forall
ctx f1 f2
(
MATCH:
match_fundef ctx f1 f2),
(<<
EXT:
exists ef targs tres cc,
f1 =
External ef targs tres cc /\
f2 =
External ef targs tres cc>>)
\/ (<<
INT:
exists fd1 fd2,
f1 =
Internal fd1 /\
f2 =
Internal fd2 /\ <<
SIG:
fn_sig1 fd1 =
fn_sig2 fd2>> >>).
Lemma match_program_eq
F1 F2 match_fundef match_varinfo fn_sig1 fn_sig2
`{
Linker (
Ctypes.fundef F1)}
(
p1:
Ctypes.program F1)
(
p2:
Ctypes.program F2)
(
MATCH:
match_program match_fundef match_varinfo p1 p2)
(
WF:
wf_match_fundef match_fundef fn_sig1 fn_sig2):
<<
EQ:
CSk.of_program fn_sig1 p1 =
CSk.of_program fn_sig2 p2>>.
Proof.
rr in MATCH.
des.
unfold of_program.
r.
f_equal;
ss.
revert MATCH.
generalize p1 at 1
as CTX.
i.
destruct p1,
p2;
ss.
clear -
MATCH WF.
ginduction prog_defs;
ii;
ss;
inv MATCH;
ss.
erewrite IHprog_defs;
eauto.
f_equal;
eauto.
inv H2.
destruct a,
b1;
ss.
clarify.
inv H1;
ss.
-
unfold update_snd.
exploit WF;
eauto.
i;
des;
clarify;
ss.
+
repeat f_equal.
exploit WF;
et.
-
inv H0.
ss.
Qed.
Lemma of_program_prog_defmap:
forall F (
p:
Ctypes.program F) (
get_sg:
F ->
signature),
<<
SIM:
forall id,
option_rel (@
Linking.match_globdef unit _ _ _ _ _
(@
match_fundef _ _ (
get_sg))
top2
tt)
(
p.(
prog_defmap) !
id) ((
of_program get_sg p).(
prog_defmap) !
id)>>.
Proof.
Local Opaque prog_defmap.
Lemma of_program_internals:
forall F get_sg (
p:
Ctypes.program F),
(
of_program get_sg p).(
internals) =
p.(
internals).
Proof.
Local Transparent prog_defmap.
End CSk.
Module CSkEnv.
Local Opaque prog_defs_names.
Local Opaque prog_defmap.
Lemma project_revive_precise
F skenv (
prog:
Ctypes.program F)
skenv_link get_sg
(
PROJ:
SkEnv.project_spec skenv_link prog.(
CSk.of_program get_sg)
skenv)
(
INCL:
SkEnv.includes skenv_link prog.(
CSk.of_program get_sg)):
<<
PRECISE:
SkEnv.genv_precise (
SkEnv.revive skenv prog)
prog>>.
Proof.
Lemma project_revive_no_external
F (
prog:
Ctypes.program F)
skenv_link get_sg blk gd
(
DEF:
Genv.find_def (
SkEnv.revive (
SkEnv.project skenv_link (
CSk.of_program get_sg prog))
prog)
blk =
Some gd)
(
EXTERNAL:
is_external gd)
(
INCL:
SkEnv.includes skenv_link (
CSk.of_program get_sg prog))
(
WF:
SkEnv.wf skenv_link):
False.
Proof.
Lemma senv_genv_compat
F (
skenv_link:
SkEnv.t)
fn_sig (
prog:
Ctypes.program F)
(
INCL:
SkEnv.includes skenv_link (
CSk.of_program fn_sig prog)):
senv_genv_compat skenv_link (
SkEnv.revive (
SkEnv.project skenv_link (
CSk.of_program fn_sig prog))
prog).
Proof.
End CSkEnv.
Lemma typ_of_type_list
t
:
map typ_of_type (
Ctypes.typelist_to_listtype t) =
typlist_of_typelist t
.
Proof.
ginduction t; ii; ss. rewrite IHt. ss.
Qed.