Module Main
Require Import Coqlib.
Require Import AST.
Require Import Maps.
Require Import Integers.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Behaviors.
Require Import Csyntax.
Require Import Csem.
Require Import Cstrategy.
Require Import RTL.
Require Import Asm.
Require Import Compiler.
Require Import GlobalBounds.
Require Import GlobalBounds_proof.
Require Import CountingSem_proof.
Require Import Errors.
Require Import DLib.
Require Import FullLoopbounds.
Open Scope error_monad_scope.
Definition headers :=
GlobalBounds.headers.
Definition full_bounds :=
FullLoopbounds.full_bounds.
Definition transf_c_program :=
Compiler.transf_c_program.
Definition transf_cminor_program :=
Compiler.transf_cminor_program.
Definition transf_rtl_program :=
Compiler.transf_rtl_program.
Definition rtl_bounds (
prog:
RTL.program) :
res (
ident->
option Z) :=
do f <-
check_one_single_func prog;
do bound <-
GlobalBounds.bound f;
do m0 <-
get_opt (
Genv.init_mem prog) "
init_mem error";
let annots :=
annots f in
OK (
fun id =>
bound_from_list bound (
PMap.get id annots)).
Theorem rtl_terminates_bound:
forall prog bound,
rtl_bounds prog =
OK bound ->
forall t r id b,
program_behaves (
RTL.semantics prog) (
Behaviors.Terminates t r) ->
bound id =
Some b ->
(
Z_of_nat (
count_annot id t) <=
b)%
Z.
Proof.
unfold rtl_bounds;
intros.
monadInv H.
unfold check_one_single_func in EQ.
monadInv EQ.
unfold DLib.get_opt in *.
repeat (
match goal with
id:(
match ?
x with |
Some _ =>
OK _ |
None =>
Error _ end) =
OK _ |-
_ =>
let T :=
fresh "
T"
in
case_eq x; [
intro;
intros T|
intros T];
rewrite T in id;
inv id
end).
destruct x3;
try (
inv EQ4;
fail).
monadInv EQ4.
destruct x3.
generalize (
ptree_forall_error_correct _ _ _ EQ).
clear EQ;
intros C1.
case_eq (
Memory.Mem.alloc x1 0 (
fn_stacksize x));
intros m1 b1 He.
destruct (
bound_correct x x0 EQ1)
as (
scp &
S1).
eapply rtl_terminates_bound;
eauto.
intros pc ins Hp;
generalize (
C1 _ _ Hp);
destruct ins;
auto;
congruence.
apply valid_annotation1.
apply valid_annotation2.
Qed.
Lemma RTL_determinate:
forall p,
determinate (
RTL.semantics p).
Proof.
intros p.
constructor.
>
intros.
inv H;
inv H0;
try match goal with
|
id1 : (
fn_code _) !
_ =
_,
id2 : (
fn_code _) !
_ =
_ |-
_ =>
rewrite id2 in id1;
inv id1
end;
try congruence;
(
split; [
try constructor|
intro;
try congruence]).
eapply external_call_match_traces;
eauto.
destruct external_call_determ with (1:=
H2) (2:=
H11).
destruct H1;
subst;
auto.
assert (
b0=
b)
by congruence;
subst;
auto.
eapply external_call_match_traces;
eauto.
destruct external_call_determ with (1:=
H1) (2:=
H7).
destruct H2;
subst;
auto.
>
red;
intros;
inv H;
simpl;
try omega.
eapply external_call_trace_length;
eauto.
eapply external_call_trace_length;
eauto.
>
intros.
inv H;
inv H0.
unfold ge,
ge0 in *.
f_equal;
try congruence.
>
intros.
inv H.
red;
intros;
red;
intros.
inv H;
congruence.
>
intros.
inv H;
inv H0.
congruence.
Qed.
Definition transf_c_program_with_bound (
p:
Csyntax.program) :
res (
Asm.program * (
ident ->
option Z)) :=
do rtl <-
transf_c_program_to_rtl p;
do bound <-
rtl_bounds rtl;
do asm <-
transf_rtl_program rtl;
OK (
asm,
bound).
Definition not_wrong_program (
p:
Csyntax.program) :
Prop :=
forall beh,
program_behaves (
Csem.semantics p)
beh ->
not_wrong beh.
Open Scope Z_scope.
Theorem 2 in the paper: transf_c_program_with_bound_correct.
It states the start-to-end correctness of bounds related to program
annotations.
Theorem transf_c_program_with_bound_correct:
(* Theorem 2 *)
forall p tp bound,
transf_c_program_with_bound p =
OK (
tp,
bound) ->
not_wrong_program p ->
(
forall beh,
program_behaves (
Asm.semantics tp)
beh ->
program_behaves (
Csem.semantics p)
beh)
/\
(
forall t r id b,
program_behaves (
Asm.semantics tp) (
Behaviors.Terminates t r) ->
bound id =
Some b ->
(
Z_of_nat (
count_annot id t) <=
b)%
Z).
Proof.