diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-02 14:58:35 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-02 15:03:05 +0200 |
| commit | 79cca6a66cbad09f298e0d3b69974c47a8327fc0 (patch) | |
| tree | e20a83c9772ecb9ec8708d50dd8e45d4dba78667 /scheduling/BTL_SEtheory.v | |
| parent | 37c8b2a474bb07890f21db0535b5886bec4e4e6d (diff) | |
| download | compcert-kvx-79cca6a66cbad09f298e0d3b69974c47a8327fc0.tar.gz compcert-kvx-79cca6a66cbad09f298e0d3b69974c47a8327fc0.zip | |
minor renaming
Diffstat (limited to 'scheduling/BTL_SEtheory.v')
| -rw-r--r-- | scheduling/BTL_SEtheory.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index c437846e..7f00e46f 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -470,7 +470,7 @@ Definition sexec_final_sfv (i: final) (sis: sistate): sfval := Local Hint Constructors sem_sfval: core. -Lemma sexec_final_svf_correct ctx stk i sis t rs m s: +Lemma sexec_final_sfv_correct ctx stk i sis t rs m s: sem_sistate ctx sis rs m -> final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs m i t s -> sem_sfval ctx stk (sexec_final_sfv i sis) rs m t s. @@ -493,7 +493,7 @@ Qed. Local Hint Constructors final_step: core. Local Hint Resolve seval_builtin_args_exact: core. -Lemma sexec_final_svf_exact ctx stk i sis t rs m s: +Lemma sexec_final_sfv_exact ctx stk i sis t rs m s: sem_sistate ctx sis rs m -> sem_sfval ctx stk (sexec_final_sfv i sis) rs m t s -> final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs m i t s. @@ -677,8 +677,8 @@ Proof. econstructor; simpl; intuition eauto || congruence. Qed. -Definition poly_str {A} (tr: function -> list exit -> option reg -> A) f (svf: sfval): A := - match svf with +Definition poly_str {A} (tr: function -> list exit -> option reg -> A) f (sfv: sfval): A := + match sfv with | Sgoto pc => tr f [pc] None | Scall _ _ _ res pc => tr f [pc] (Some res) | Stailcall _ _ args => tr f [] None @@ -707,8 +707,8 @@ Inductive sstate := (* outcome of a symbolic execution path *) Record soutcome := sout { - so_sis: sistate; - so_svf: sfval; + _sis: sistate; + _sfv: sfval; }. Fixpoint run_sem_isstate ctx (st:sstate): option soutcome := @@ -717,7 +717,7 @@ Fixpoint run_sem_isstate ctx (st:sstate): option soutcome := | Scond cond args sm ifso ifnot => SOME b <- seval_condition ctx cond args sm IN run_sem_isstate ctx (if b then ifso else ifnot) - | _ => None + | Sabort => None end. (* transition (t,s) produced by a sstate in initial context ctx *) @@ -794,7 +794,7 @@ Fixpoint sexec_rec f ib sis (k: sistate -> sstate): sstate := Definition sexec f ib := sexec_rec f ib sis_init (fun _ => Sabort). Local Hint Constructors sem_sstate: core. -Local Hint Resolve sexec_op_correct sexec_final_svf_correct tr_sis_regs_correct_aux tr_sis_regs_correct +Local Hint Resolve sexec_op_correct sexec_final_sfv_correct tr_sis_regs_correct_aux tr_sis_regs_correct sexec_load_TRAP_correct sexec_store_correct sis_init_correct: core. Lemma sexec_rec_correct ctx stk t s ib rs m rs1 m1 ofin @@ -992,7 +992,7 @@ Proof. intros; rewrite REG; autodestruct; try_simplify_someHyps. Qed. -Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort sexec_final_svf_exact: core. +Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort sexec_final_sfv_exact: core. Lemma sexec_rec_exact ctx stk ib t s1: forall sis k (SEXEC: sem_sstate ctx stk t s1 (sexec_rec (cf ctx) ib sis k)) |