From f9e4d91431334d88992e62a232a9e2ff2f6fcdc9 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 25 Oct 2021 23:23:46 +0200 Subject: cleaner symbolic semantic of load traps --- scheduling/BTL_SEtheory.v | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 033ed843..55afc19a 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -84,19 +84,17 @@ Fixpoint eval_sval ctx (sv: sval): option val := SOME args <- eval_list_sval ctx l IN eval_operation (cge ctx) (csp ctx) op args (cm0 ctx) | Sload sm trap chunk addr lsv _ => + SOME args <- eval_list_sval ctx lsv IN + SOME m <- eval_smem ctx sm IN match trap with | TRAP => - SOME args <- eval_list_sval ctx lsv IN SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN - SOME m <- eval_smem ctx sm IN Mem.loadv chunk m a | NOTRAP => - SOME args <- eval_list_sval ctx lsv IN - match (eval_addressing (cge ctx) (csp ctx) addr args) with + match eval_addressing (cge ctx) (csp ctx) addr args with | None => Some Vundef | Some a => - SOME m <- eval_smem ctx sm IN - match (Mem.loadv chunk m a) with + match Mem.loadv chunk m a with | None => Some Vundef | Some val => Some val end @@ -641,7 +639,7 @@ Proof. - simpl. destruct SIS as (PRE&MEM®). rewrite Regmap.gss; simpl; auto. erewrite eval_list_sval_inj; simpl; auto. - autodestruct; rewrite MEM, LOAD; auto. + rewrite MEM; simpl. autodestruct. rewrite LOAD; auto. Qed. Definition sexec_store chunk addr args src sis: sistate := @@ -1004,7 +1002,7 @@ Proof. eapply set_sreg_abort; eauto. simpl. destruct SIS as (PRE&MEM®). erewrite eval_list_sval_inj; simpl; auto. - intros; autodestruct; try_simplify_someHyps. + rewrite MEM; simpl; autodestruct; try_simplify_someHyps. Qed. Lemma set_smem_abort ctx sm sis rs m: @@ -1241,10 +1239,10 @@ Proof. (P1 := fun sm => eval_smem (bctx1 ctx) sm = eval_smem (bctx2 ctx) sm); simpl; auto. + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto. erewrite eval_operation_preserved; eauto. - + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto. - erewrite eval_addressing_preserved; eauto. - destruct (eval_addressing _ _ _ _); auto. - rewrite IHsv; auto. + + rewrite IHsv0; clear IHsv0. + autodestruct; intros. + erewrite IHsv; do 2 autodestruct; + erewrite eval_addressing_preserved; eauto. + rewrite IHsv; clear IHsv. destruct (eval_sval _ _); auto. rewrite IHsv0; auto. + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto. -- cgit