diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-13 12:01:32 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-13 12:01:32 +0100 |
| commit | 84dfe6960d60bb9a41acf33f33042b34f248677b (patch) | |
| tree | 4eb13f0aca3406b0676b9c9add0413b9f1e9de34 /backend/CSE3proof.v | |
| parent | b27ed35711b59b034dd3900dbca26ac190713cea (diff) | |
| download | compcert-kvx-84dfe6960d60bb9a41acf33f33042b34f248677b.tar.gz compcert-kvx-84dfe6960d60bb9a41acf33f33042b34f248677b.zip | |
begin adding invariants and inductiveness
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 26 |
1 files changed, 17 insertions, 9 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 855f8338..0a43a58d 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -242,7 +242,10 @@ Inductive match_stackframes: list stackframe -> list stackframe -> signature -> (FUN: transf_function f = OK tf) (WTF: type_function f = OK tenv) (WTRS: wt_regset tenv rs) - (WTRES: tenv res = proj_sig_res sg), + (WTRES: tenv res = proj_sig_res sg) + (invariants : PMap.t RB.t) + (hints : analysis_hints) + (IND: is_inductive_allstep (ctx:=(context_from_hints hints)) f tenv invariants), match_stackframes (Stackframe res f sp pc rs :: s) (Stackframe res tf sp pc rs :: ts) @@ -254,7 +257,10 @@ Inductive match_states: state -> state -> Prop := (STACKS: match_stackframes s ts (fn_sig tf)) (FUN: transf_function f = OK tf) (WTF: type_function f = OK tenv) - (WTRS: wt_regset tenv rs), + (WTRS: wt_regset tenv rs) + (invariants : PMap.t RB.t) + (hints : analysis_hints) + (IND: is_inductive_allstep (ctx:=(context_from_hints hints)) f tenv invariants), match_states (State s f sp pc rs m) (State ts tf sp pc rs m) | match_states_call: @@ -437,13 +443,15 @@ Proof. + rewrite params_preserved with (tf:=tf) (f:=f) by assumption. rewrite entrypoint_preserved with (tf:=tf) (f:=f) by assumption. econstructor; eauto. - apply type_function_correct in TENV. - inv TENV. - simpl in WTARGS. - rewrite sig_preserved2 with (f:=f) in WTARGS by assumption. - apply wt_init_regs. - rewrite <- wt_params in WTARGS. - assumption. + * apply type_function_correct in TENV. + inv TENV. + simpl in WTARGS. + rewrite sig_preserved2 with (f:=f) in WTARGS by assumption. + apply wt_init_regs. + rewrite <- wt_params in WTARGS. + assumption. + * apply checked_is_inductive_allstep. + apply transf_function_invariants_inductive with (tf:=tf); auto. - (* external *) simpl in FUN. inv FUN. |