From af2c82cfd7f2318fcd81da2ea4cf3fd695db3b40 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 28 Apr 2021 18:14:53 +0200 Subject: start the new "BTL" IR. --- scheduling/BTL.v | 575 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 575 insertions(+) create mode 100644 scheduling/BTL.v (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v new file mode 100644 index 00000000..8bdafb89 --- /dev/null +++ b/scheduling/BTL.v @@ -0,0 +1,575 @@ +(** The BTL intermediate language: abstract syntax and semantics. + + BTL stands for "Block Transfer Language". + + Informally, a block is a piece of "loop-free" code, with a single entry-point, + hence, such that transformation preserving locally the semantics of each block, + preserve also globally the semantics of the function. + + a BTL function is a CFG where each node is such a block, represented by structured code. + + BTL gives a structured view of RTL code. + It is dedicated to optimizations validated by "symbolic simulation" over blocks. + + +*) + +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import RTL Op Registers OptionMonad. + +(** * Abstract syntax *) + +Definition exit := node. (* we may generalize this with register renamings at exit, + like in "phi" nodes of SSA-form *) + +(** final instructions (that stops block execution) *) +Inductive final: Type := + | Bgoto (succ:exit) (** No operation -- just branch to [succ]. *) + | Breturn (res: option reg) + (** terminates the execution of the current function. It returns the value of the given + register, or [Vundef] if none is given. *) + | Bcall (sig: signature) (fn: reg + ident) (args:list reg) (dest:reg) (succ:exit) + (** invokes the function determined by [fn] (either a function pointer found in a register or a + function name), giving it the values of registers [args] as arguments. + It stores the return value in [dest] and branches to [succ]. *) + | Btailcall (sig:signature) (fn: reg + ident) (args: list reg) + (** performs a function invocation in tail-call position + (the current function terminates after the call, returning the result of the callee) + *) + | Bbuiltin (ef:external_function) (args:list (builtin_arg reg)) (dest:builtin_res reg) (succ:exit) + (** calls the built-in function identified by [ef], giving it the values of [args] as arguments. + It stores the return value in [dest] and branches to [succ]. *) + | Bjumptable (arg:reg) (tbl:list exit) + (** [Bjumptable arg tbl] transitions to the node that is the [n]-th + element of the list [tbl], where [n] is the unsigned integer value of register [arg]. *) + . + +(* instruction block *) +Inductive iblock: Type := +(* final instructions that stops block execution *) + | BF (fi: final) +(* basic instructions that continues block execution, except when aborting *) + | Bnop (* nop instruction *) + | Bop (op:operation) (args:list reg) (dest:reg) + (** performs the arithmetic operation [op] over the values of registers [args], stores the result in [dest] *) + | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg) + (** loads a [chunk] quantity from the address determined by the addressing mode [addr] + and the values of the [args] registers, stores the quantity just read into [dest]. + If trap=NOTRAP, then failures lead to a default value written to [dest]. *) + | Bstore (chunk:memory_chunk) (addr:addressing) (args:list reg) (src:reg) + (** stores the value of register [src] in the [chunk] quantity at the + the address determined by the addressing mode [addr] and the + values of the [args] registers. *) +(* composed instructions *) + | Bseq (b1 b2: iblock) + (** starts by running [b1] and stops here if execution of [b1] has reached a final instruction or aborted + or continue with [b2] otherwise *) + | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock) (info:option bool) + (** evaluates the boolean condition [cond] over the values of registers [args]. + If the condition is true, it continues on [ifso]. + If the condition is false, it continues on [ifnot]. + [info] is a ghost field there to provide information relative to branch prediction. *) + . +Coercion BF: final >-> iblock. + + +(** NB: - a RTL [(Inop pc)] ending a branch of block is encoded by [(Bseq Bnop (Bgoto pc))]. + - a RTL [(Inop pc)] in the middle of a branch is simply encoded by [Bnop]. + - the same trick appears for all "basic" instructions and [Icond]. +*) + + + +Record iblock_info := { + entry: iblock; + input_regs: Regset.t (* extra liveness information ignored by BTL semantics *) +}. + +Definition code: Type := PTree.t iblock_info. + +Record function: Type := mkfunction { + fn_sig: signature; + fn_params: list reg; + fn_stacksize: Z; + fn_code: code; + fn_entrypoint: node +}. + +(** A function description comprises a control-flow graph (CFG) [fn_code] + (a partial finite mapping from nodes to instructions). As in Cminor, + [fn_sig] is the function signature and [fn_stacksize] the number of bytes + for its stack-allocated activation record. [fn_params] is the list + of registers that are bound to the values of arguments at call time. + [fn_entrypoint] is the node of the first instruction of the function + in the CFG. *) + +Definition fundef := AST.fundef function. + +Definition program := AST.program fundef unit. + +Definition funsig (fd: fundef) := + match fd with + | Internal f => fn_sig f + | External ef => ef_sig ef + end. + +(** * Operational semantics *) + +Definition genv := Genv.t fundef unit. + +(** The dynamic semantics of BTL is similar to RTL, + except that the step of one instruction is generalized into the run of one [iblock]. +*) + +Inductive stackframe : Type := + | Stackframe: + forall (res: reg) (**r where to store the result *) + (f: function) (**r calling function *) + (sp: val) (**r stack pointer in calling function *) + (succ: exit) (**r program point in calling function *) + (rs: regset), (**r register state in calling function *) + stackframe. + +Inductive state : Type := + | State: + forall (stack: list stackframe) (**r call stack *) + (f: function) (**r current function *) + (sp: val) (**r stack pointer *) + (pc: node) (**r current program point in [c] *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) + state + | Callstate: + forall (stack: list stackframe) (**r call stack *) + (f: fundef) (**r function to call *) + (args: list val) (**r arguments to the call *) + (m: mem), (**r memory state *) + state + | Returnstate: + forall (stack: list stackframe) (**r call stack *) + (v: val) (**r return value for the call *) + (m: mem), (**r memory state *) + state. + +(** outcome of a block execution *) +Record outcome := { + _rs: regset; + _m: mem; + _fin: option final +}. + +Section RELSEM. + +Variable ge: genv. + +Definition find_function (ros: reg + ident) (rs: regset) : option fundef := + match ros with + | inl r => Genv.find_funct ge rs#r + | inr symb => + match Genv.find_symbol ge symb with + | None => None + | Some b => Genv.find_funct_ptr ge b + end + end. + +Local Open Scope option_monad_scope. + +(** internal big-step execution of one iblock *) +Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop := + | exec_final rs m fin: iblock_istep sp rs m (BF fin) rs m (Some fin) + | exec_nop rs m: iblock_istep sp rs m Bnop rs m None + | exec_op rs m op args res v + (EVAL: eval_operation ge sp op rs##args m = Some v) + : iblock_istep sp rs m (Bop op args res) (rs#res <- v) m None + | exec_load_TRAP rs m chunk addr args dst a v + (EVAL: eval_addressing ge sp addr rs##args = Some a) + (LOAD: Mem.loadv chunk m a = Some v) + : iblock_istep sp rs m (Bload TRAP chunk addr args dst) (rs#dst <- v) m None + | exec_store rs m chunk addr args src a m' + (EVAL: eval_addressing ge sp addr rs##args = Some a) + (STORE: Mem.storev chunk m a rs#src = Some m') + : iblock_istep sp rs m (Bstore chunk addr args src) rs m' None + | exec_seq_stop rs m b1 b2 rs' m' fin + (EXEC: iblock_istep sp rs m b1 rs' m' (Some fin)) + : iblock_istep sp rs m (Bseq b1 b2) rs' m' (Some fin) + | exec_seq_continue rs m b1 b2 rs1 m1 rs' m' ofin + (EXEC1: iblock_istep sp rs m b1 rs1 m1 None) + (EXEC2: iblock_istep sp rs1 m1 b2 rs' m' ofin) + : iblock_istep sp rs m (Bseq b1 b2) rs' m' ofin + | exec_cond rs m cond args ifso ifnot i b rs' m' ofin + (EVAL: eval_condition cond rs##args m = Some b) + (EXEC: iblock_istep sp rs m (if b then ifso else ifnot) rs' m' ofin) + : iblock_istep sp rs m (Bcond cond args ifso ifnot i) rs' m' ofin + . +Local Hint Constructors iblock_istep: core. + +(** A functional variant of [iblock_istep_run] of [iblock_istep]. +Lemma [iblock_istep_run_equiv] below provides a proof that "relation" [iblock_istep] is a "partial function". +*) +Fixpoint iblock_istep_run sp ib rs m: option outcome := + match ib with + | BF fin => + Some {| _rs := rs; _m := m; _fin := Some fin |} + (* basic instructions *) + | Bnop => + Some {| _rs := rs; _m:= m; _fin := None |} + | Bop op args res => + SOME v <- eval_operation ge sp op rs##args m IN + Some {| _rs := rs#res <- v; _m:= m; _fin := None |} + | Bload TRAP chunk addr args dst => + SOME a <- eval_addressing ge sp addr rs##args IN + SOME v <- Mem.loadv chunk m a IN + Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} + | Bload NOTRAP chunk addr args dst => + None (* TODO *) + | Bstore chunk addr args src => + SOME a <- eval_addressing ge sp addr rs##args IN + SOME m' <- Mem.storev chunk m a rs#src IN + Some {| _rs := rs; _m:= m'; _fin := None |} + (* composed instructions *) + | Bseq b1 b2 => + SOME out1 <- iblock_istep_run sp b1 rs m IN + match out1.(_fin) with + | None => iblock_istep_run sp b2 out1.(_rs) out1.(_m) + | _ => Some out1 (* stop execution on the 1st final instruction *) + end + | Bcond cond args ifso ifnot _ => + SOME b <- eval_condition cond rs##args m IN + iblock_istep_run sp (if b then ifso else ifnot) rs m + end. + +Lemma iblock_istep_run_equiv sp rs m ib rs' m' ofin: + iblock_istep sp rs m ib rs' m' ofin <-> iblock_istep_run sp ib rs m = Some {| _rs := rs'; _m:= m'; _fin := ofin |}. +Proof. + constructor. + - induction 1; simpl; try autodestruct; try_simplify_someHyps. + - generalize rs m rs' m' ofin; clear rs m rs' m' ofin. + induction ib; simpl; repeat (try autodestruct; try_simplify_someHyps). + destruct o; try_simplify_someHyps; subst; eauto. +Qed. + +Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := + | exec_Bgoto pc: + final_step stack f sp rs m (Bgoto pc) E0 + (State stack f sp pc rs m) + | exec_Breturn or stk m': + sp = (Vptr stk Ptrofs.zero) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + final_step stack f sp rs m (Breturn or) + E0 (Returnstate stack (regmap_optget or Vundef rs) m') + | exec_Bcall sig ros args res pc' fd: + find_function ros rs = Some fd -> + funsig fd = sig -> + final_step stack f sp rs m (Bcall sig ros args res pc') + E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m) + | exec_Btailcall sig ros args stk m' fd: + find_function ros rs = Some fd -> + funsig fd = sig -> + sp = (Vptr stk Ptrofs.zero) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + final_step stack f sp rs m (Btailcall sig ros args) + E0 (Callstate stack fd rs##args m') + | exec_Bbuiltin ef args res pc' vargs t vres m': + eval_builtin_args ge (fun r => rs#r) sp m args vargs -> + external_call ef ge vargs m t vres m' -> + final_step stack f sp rs m (Bbuiltin ef args res pc') + t (State stack f sp pc' (regmap_setres res vres rs) m') + | exec_Bjumptable arg tbl n pc': + rs#arg = Vint n -> + list_nth_z tbl (Int.unsigned n) = Some pc' -> + final_step stack f sp rs m (Bjumptable arg tbl) + E0 (State stack f sp pc' rs m) +. + +(** big-step execution of one iblock *) +Definition iblock_step stack f sp rs m ib t s: Prop := + exists rs' m' fin, iblock_istep sp rs m ib rs' m' (Some fin) /\ final_step stack f sp rs' m' fin t s. + +(** The transitions are presented as an inductive predicate + [step ge st1 t st2], where [ge] is the global environment, + [st1] the initial state, [st2] the final state, and [t] the trace + of system calls performed during this transition. *) + +Inductive step: state -> trace -> state -> Prop := + | exec_iblock stack ib f sp pc rs m t s: + (fn_code f)!pc = Some ib -> + iblock_step stack f sp rs m ib.(entry) t s -> + step (State stack f sp pc rs m) t s + | exec_function_internal stack f args m m' stk: + Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> + step (Callstate stack (Internal f) args m) + E0 (State stack + f + (Vptr stk Ptrofs.zero) + f.(fn_entrypoint) + (init_regs args f.(fn_params)) + m') + | exec_function_external stack ef args res t m m': + external_call ef ge args m t res m' -> + step (Callstate stack (External ef) args m) + t (Returnstate stack res m') + | exec_return stack res f sp pc rs vres m: + step (Returnstate (Stackframe res f sp pc rs :: stack) vres m) + E0 (State stack f sp pc (rs#res <- vres) m) +. + +End RELSEM. + +(** Execution of whole programs are described as sequences of transitions + from an initial state to a final state. An initial state is a [Callstate] + corresponding to the invocation of the ``main'' function of the program + without arguments and with an empty call stack. *) + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b f m0, + let ge := Genv.globalenv p in + Genv.init_mem p = Some m0 -> + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + funsig f = signature_main -> + initial_state p (Callstate nil f nil m0). + +(** A final state is a [Returnstate] with an empty call stack. *) + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall r m, + final_state (Returnstate nil (Vint r) m) r. + +(** The small-step semantics for a program. *) + +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). + + +(** Matching BTL and RTL code + +We should be able to define a single verifier able to prove a bisimulation between BTL and RTL code. + +NB 1: the proof of BTL -> RTL (plus simulation) should be much easier than RTL -> BTL (star simulation). + +NB 2: our scheme allows the BTL to duplicate some RTL code. +- in other words: RTL -> BTL allows tail duplication, loop unrolling, etc. Exactly like "Duplicate" on RTL. +- BTL -> RTL allows to "undo" some duplications (e.g. remove duplications that have not enabled interesting optimizations) ! + +Hence, in a sense, our verifier imitates the approach of Duplicate, where [dupmap] maps the BTL nodes to the RTL nodes. + +The [match_*] definitions gives a "relational" specification of the verifier... +*) + +Require Import Errors. + +Inductive match_final_inst (dupmap: PTree.t node): final -> instruction -> Prop := +(* TODO: it may be simplify the oracle for BTL -> RTL, but may makes the verifier more complex ? + | mfi_goto pc pc': + dupmap!pc = (Some pc') -> match_final_inst dupmap (Bgoto pc) (Inop pc') +*) + | mfi_return or: match_final_inst dupmap (Breturn or) (Ireturn or) + | mfi_call pc pc' s ri lr r: + dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc) (Icall s ri lr r pc') + | mfi_tailcall s ri lr: + match_final_inst dupmap (Btailcall s ri lr) (Itailcall s ri lr) + | mfi_builtin pc pc' ef la br: + dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc) (Ibuiltin ef la br pc') + | mfi_jumptable ln ln' r: + list_forall2 (fun pc pc' => (dupmap!pc = (Some pc'))) ln ln' -> + match_final_inst dupmap (Bjumptable r ln) (Ijumptable r ln') +. + +Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop := + | ijo_None_left o: is_join_opt None o o + | ijo_None_right o: is_join_opt o None o + | ijo_Some x: is_join_opt (Some x) (Some x) (Some x) + . + +(* [match_iblock dupmap cfg isfst pc ib opc] means that [ib] match a block in a RTL code starting at [pc], with: + - [isfst] (in "input") indicates that no step in the surrounding block has been executed before entering [pc] + - if [opc] (in "ouput") is [None], this means that all branches of the block ends on a final instruction + - if [opc] is [Some pc'], this means that all branches of the block that do not exit, join on [pc']. +*) +Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> iblock -> (option node) -> Prop := + | mib_BF isfst fi pc i: + cfg!pc = Some i -> + match_final_inst dupmap fi i -> + match_iblock dupmap cfg isfst pc (BF fi) None + | mib_nop isfst pc pc': + cfg!pc = Some (Inop pc') -> + match_iblock dupmap cfg isfst pc Bnop (Some pc') + | mib_op isfst pc pc' op lr r: + cfg!pc = Some (Iop op lr r pc') -> + match_iblock dupmap cfg isfst pc (Bop op lr r) (Some pc') + | mib_load isfst pc pc' tm m a lr r: + cfg!pc = Some (Iload tm m a lr r pc') -> + match_iblock dupmap cfg isfst pc (Bload tm m a lr r) (Some pc') + | mib_store isfst pc pc' m a lr r: + cfg!pc = Some (Istore m a lr r pc') -> + match_iblock dupmap cfg isfst pc (Bstore m a lr r) (Some pc') + | mib_exit pc pc': + dupmap!pc = (Some pc') -> + match_iblock dupmap cfg false pc' (Bgoto pc) None + (* NB: on RTL side, we exit the block by a "basic" instruction (or Icond). + Thus some step should have been executed before [pc'] in the RTL code *) + | mib_seq_Some isfst b1 b2 pc1 pc2 opc: + match_iblock dupmap cfg isfst pc1 b1 (Some pc2) -> + match_iblock dupmap cfg false pc2 b2 opc -> + match_iblock dupmap cfg isfst pc1 (Bseq b1 b2) opc +(* | mib_seq_None isfst b1 b2 pc: + match_iblock dupmap cfg isfst pc b1 None -> + match_iblock dupmap cfg isfst (Bseq b1 b2) pc None + (* TODO: here [b2] is dead code ! Is this case really useful ? + The oracle could remove this dead code. + And the verifier could fail if there is such dead code! + *) +*) + | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i i': + cfg!pc = Some (Icond c lr pcso pcnot i') -> + match_iblock dupmap cfg false pcso bso opc1 -> + match_iblock dupmap cfg false pcnot bnot opc2 -> + is_join_opt opc1 opc2 opc -> + match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot i) opc + . + +(* Partial copy of Duplicate and Duplicateproof. *) + +Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop := + forall pc pc', dupmap!pc = Some pc' -> + exists ib, cfg!pc = Some ib /\ match_iblock dupmap cfg' true pc' ib.(entry) None. + +Record match_function dupmap f f': Prop := { + dupmap_correct: match_cfg dupmap (fn_code f) (RTL.fn_code f'); + dupmap_entrypoint: dupmap!(fn_entrypoint f) = Some (RTL.fn_entrypoint f'); + preserv_fnsig: fn_sig f = RTL.fn_sig f'; + preserv_fnparams: fn_params f = RTL.fn_params f'; + preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f' +}. + +Inductive match_fundef: fundef -> RTL.fundef -> Prop := + | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f') + | match_External ef: match_fundef (External ef) (External ef). + +Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop := + | match_stackframe_intro + dupmap res f sp pc rs f' pc' + (TRANSF: match_function dupmap f f') + (DUPLIC: dupmap!pc' = Some pc) + : match_stackframes (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). + +Inductive match_states: state -> RTL.state -> Prop := + | match_states_intro + dupmap st f sp pc rs m st' f' pc' + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_function dupmap f f') + (DUPLIC: dupmap!pc' = Some pc) + : match_states (State st f sp pc rs m) (RTL.State st' f' sp pc' rs m) + | match_states_call + st st' f f' args m + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_fundef f f') + : match_states (Callstate st f args m) (RTL.Callstate st' f' args m) + | match_states_return + st st' v m + (STACKS: list_forall2 match_stackframes st st') + : match_states (Returnstate st v m) (RTL.Returnstate st' v m) + . + +(** Shared verifier between RTL -> BTL and BTL -> RTL *) + +Local Open Scope error_monad_scope. + +Definition verify_is_copy dupmap n n' := + match dupmap!n with + | None => Error(msg "verify_is_copy None") + | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end + end. + +Fixpoint verify_is_copy_list dupmap ln ln' := + match ln with + | n::ln => match ln' with + | n'::ln' => do _ <- verify_is_copy dupmap n n'; + verify_is_copy_list dupmap ln ln' + | nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end + | nil => match ln' with + | n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'") + | nil => OK tt end + end. + +Lemma verify_is_copy_correct dupmap n n' tt: + verify_is_copy dupmap n n' = OK tt -> + dupmap ! n = Some n'. +Proof. + unfold verify_is_copy; repeat autodestruct. + intros NP H; destruct (_ ! n) eqn:REVM; [|inversion H]. + eapply Pos.compare_eq in NP. congruence. +Qed. +Local Hint Resolve verify_is_copy_correct: core. + +Lemma verify_is_copy_list_correct dupmap ln: forall ln' tt, + verify_is_copy_list dupmap ln ln' = OK tt -> + list_forall2 (fun n n' => dupmap ! n = Some n') ln ln'. +Proof. + induction ln. + - intros. destruct ln'; monadInv H. constructor. + - intros. destruct ln'; monadInv H. constructor; eauto. +Qed. + +(* TODO: deuxième étape (après BTLtoRTLproof.plus_simulation) *) +Parameter verify_block: PTree.t node -> RTL.code -> bool -> node -> iblock -> res (option node). + +(* This property expresses that "relation" [match_iblock] is a partial function (see also [iblock_istep_run_equiv] above) *) +Lemma verify_block_correct: forall dupmap cfg isfst pc ib fin, + verify_block dupmap cfg isfst pc ib = (OK fin) -> match_iblock dupmap cfg isfst pc ib fin. +Admitted. +Local Hint Resolve verify_block_correct: core. + +Fixpoint verify_blocks dupmap (cfg: code) (cfg':RTL.code) l: res unit := + match l with + | nil => OK tt + | (pc, pc')::l => + match cfg!pc with + | Some ib => do o <- verify_block dupmap cfg' true pc' ib.(entry); + match o with + | None => verify_blocks dupmap cfg cfg' l + | _ => Error(msg "verify_blocks.end") + end + | _ => Error(msg "verify_blocks.entry") + end + end. + +Definition verify_cfg dupmap (cfg: code) (cfg':RTL.code): res unit := + verify_blocks dupmap cfg cfg' (PTree.elements dupmap). + +Lemma verify_cfg_correct dupmap cfg cfg' tt: + verify_cfg dupmap cfg cfg' = OK tt -> + match_cfg dupmap cfg cfg'. +Proof. + unfold verify_cfg. + intros X pc pc' H; generalize X; clear X. + exploit PTree.elements_correct; eauto. + generalize tt pc pc' H; clear tt pc pc' H. + generalize (PTree.elements dupmap). + induction l as [|[pc1 pc1']l]; simpl. + - tauto. + - intros pc pc' DUP u H. + unfold bind. + repeat autodestruct. + intros; subst. + destruct H as [H|H]; eauto. + inversion H; subst. + eexists; split; eauto. +Qed. + +Definition verify_function dupmap f f' : res unit := + do _ <- verify_is_copy dupmap (fn_entrypoint f) (RTL.fn_entrypoint f'); + verify_cfg dupmap (fn_code f) (RTL.fn_code f'). + +Lemma verify_function_correct dupmap f f' tt: + verify_function dupmap f f' = OK tt -> + fn_sig f = RTL.fn_sig f' -> + fn_params f = RTL.fn_params f' -> + fn_stacksize f = RTL.fn_stacksize f' -> + match_function dupmap f f'. +Proof. + unfold verify_function; intro VERIF. monadInv VERIF. + constructor; eauto. + eapply verify_cfg_correct; eauto. +Qed. -- cgit From 989e85b700161867c2f80df55c2dfaaaa5fe82b4 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 30 Apr 2021 16:52:21 +0200 Subject: BTLtoRTL: proof for internal/external/return states --- scheduling/BTL.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 8bdafb89..8529010c 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -451,7 +451,7 @@ Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop := | match_stackframe_intro dupmap res f sp pc rs f' pc' (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc' = Some pc) + (DUPLIC: dupmap!pc = Some pc') : match_stackframes (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). Inductive match_states: state -> RTL.state -> Prop := @@ -459,7 +459,7 @@ Inductive match_states: state -> RTL.state -> Prop := dupmap st f sp pc rs m st' f' pc' (STACKS: list_forall2 match_stackframes st st') (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc' = Some pc) + (DUPLIC: dupmap!pc = Some pc') : match_states (State st f sp pc rs m) (RTL.State st' f' sp pc' rs m) | match_states_call st st' f f' args m -- cgit From 3751a5570441faed6147f0d7e80dffbb2342d258 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Sat, 1 May 2021 17:11:48 +0200 Subject: debroussaillage et precisions... --- scheduling/BTL.v | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 8529010c..28941e01 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -292,26 +292,26 @@ Definition iblock_step stack f sp rs m ib t s: Prop := of system calls performed during this transition. *) Inductive step: state -> trace -> state -> Prop := - | exec_iblock stack ib f sp pc rs m t s: - (fn_code f)!pc = Some ib -> - iblock_step stack f sp rs m ib.(entry) t s -> - step (State stack f sp pc rs m) t s - | exec_function_internal stack f args m m' stk: - Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> - step (Callstate stack (Internal f) args m) - E0 (State stack + | exec_iblock stack ib f sp pc rs m t s + (PC: (fn_code f)!pc = Some ib) + (STEP: iblock_step stack f sp rs m ib.(entry) t s) + :step (State stack f sp pc rs m) t s + | exec_function_internal stack f args m m' stk + (ALLOC: Mem.alloc m 0 f.(fn_stacksize) = (m', stk)) + :step (Callstate stack (Internal f) args m) + E0 (State stack f (Vptr stk Ptrofs.zero) f.(fn_entrypoint) (init_regs args f.(fn_params)) m') - | exec_function_external stack ef args res t m m': - external_call ef ge args m t res m' -> - step (Callstate stack (External ef) args m) - t (Returnstate stack res m') - | exec_return stack res f sp pc rs vres m: - step (Returnstate (Stackframe res f sp pc rs :: stack) vres m) - E0 (State stack f sp pc (rs#res <- vres) m) + | exec_function_external stack ef args res t m m' + (EXTCALL: external_call ef ge args m t res m') + :step (Callstate stack (External ef) args m) + t (Returnstate stack res m') + | exec_return stack res f sp pc rs vres m + :step (Returnstate (Stackframe res f sp pc rs :: stack) vres m) + E0 (State stack f sp pc (rs#res <- vres) m) . End RELSEM. -- cgit From e9f8fa5f0635f3c1af489bcf084d38f89ea58b13 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 5 May 2021 14:03:04 +0200 Subject: advance in cfg checker --- scheduling/BTL.v | 139 ++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 138 insertions(+), 1 deletion(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 28941e01..82a54061 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -513,11 +513,148 @@ Proof. Qed. (* TODO: deuxième étape (après BTLtoRTLproof.plus_simulation) *) -Parameter verify_block: PTree.t node -> RTL.code -> bool -> node -> iblock -> res (option node). +Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) := + match ib with + | BF fi => + match fi with + | Bgoto pc => + match dupmap!pc with + | Some _ => OK None + | None => Error (msg "verify_block: incorrect dupmap Bgoto") + end + | _ => + match cfg!pc with + | Some i => Error (msg "TODO") (* TODO *) + | None => Error (msg "verify_block: incorrect cfg BF") + end + end + | Bnop => + match cfg!pc with + | Some (Inop pc') => OK (Some pc') + | _ => Error (msg "verify_block: incorrect cfg Bnop") + end + | Bop op lr r => + match cfg!pc with + | Some (Iop op' lr' r' pc') => + if (eq_operation op op') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then + OK (Some pc') + else Error (msg "verify_block: different r in Bop") + else Error (msg "verify_block: different lr in Bop") + else Error (msg "verify_block: different operations in Bop") + | _ => Error (msg "verify_block: incorrect cfg Bop") + end + | Bload tm m a lr r => + match cfg!pc with + | Some (Iload tm' m' a' lr' r' pc') => + if (trapping_mode_eq tm tm') then + if (chunk_eq m m') then + if (eq_addressing a a') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then + OK (Some pc') + else Error (msg "verify_block: different r in Bload") + else Error (msg "verify_block: different lr in Bload") + else Error (msg "verify_block: different addressing in Bload") + else Error (msg "verify_block: different mchunk in Bload") + else Error (msg "verify_block: different trapping_mode in Bload") + | _ => Error (msg "verify_block: incorrect cfg Bload") + end + | Bstore m a lr r => + match cfg!pc with + | Some (Istore m' a' lr' r' pc') => + if (chunk_eq m m') then + if (eq_addressing a a') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then OK (Some pc') + else Error (msg "verify_block: different r in Bstore") + else Error (msg "verify_block: different lr in Bstore") + else Error (msg "verify_block: different addressing in Bstore") + else Error (msg "verify_block: different mchunk in Bstore") + | _ => Error (msg "verify_block: incorrect cfg Bstore") + end + | Bseq b1 b2 => + do opc <- verify_block dupmap cfg isfst pc b1; + match opc with + | Some pc' => + verify_block dupmap cfg false pc' b2 + | None => Error (msg "verify_block: None next pc in Bseq (deadcode)") + end + | Bcond c lr bso bnot i => + match cfg!pc with + | Some (Icond c' lr' pcso pcnot i') => + if (list_eq_dec Pos.eq_dec lr lr') then + if (eq_condition c c') then + do opc1 <- verify_block dupmap cfg false pcso bso; + do opc2 <- verify_block dupmap cfg false pcnot bnot; + match opc1, opc2 with + | None, o => OK o + | o, None => OK o + | Some x, Some x' => + if Pos.eq_dec x x' then OK (Some x) + else Error (msg "verify_block: is_join_opt incorrect for Bcond") + end + else Error (msg "verify_block: incompatible conditions in Bcond") + else Error (msg "verify_block: different lr in Bcond") + | _ => Error (msg "verify_block: incorrect cfg Bcond") + end + end. (* This property expresses that "relation" [match_iblock] is a partial function (see also [iblock_istep_run_equiv] above) *) Lemma verify_block_correct: forall dupmap cfg isfst pc ib fin, verify_block dupmap cfg isfst pc ib = (OK fin) -> match_iblock dupmap cfg isfst pc ib fin. +Proof. + induction ib; intros; + try (unfold verify_block in H; destruct (cfg!pc) eqn:EQCFG; [ idtac | discriminate; fail ]). + - admit. + - (* Bnop *) + destruct i; inv H. + constructor; assumption. + - (* Bop *) + destruct i; try discriminate. + destruct (eq_operation _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. inv H. + constructor; assumption. + - (* Bload *) + destruct i; try discriminate. + destruct (trapping_mode_eq _ _); try discriminate. + destruct (chunk_eq _ _); try discriminate. + destruct (eq_addressing _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. inv H. + constructor; assumption. + - (* Bstore *) + destruct i; try discriminate. + destruct (chunk_eq _ _); try discriminate. + destruct (eq_addressing _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. inv H. + constructor; assumption. + - (* Bseq *) + monadInv H. + destruct x; try discriminate. + eapply mib_seq_Some. + eapply IHib1; eauto. admit. + (*eapply IHib2; eauto.*) + (*destruct (cfg!pc) eqn:ECFG; try discriminate.*) + (*destruct i; try discriminate.*) + - (* Bcond *) + destruct i; try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (eq_condition _ _); try discriminate. + fold (verify_block dupmap cfg false n ib1) in H. + fold (verify_block dupmap cfg false n0 ib2) in H. + monadInv H. + destruct x, x0; try destruct (Pos.eq_dec _ _); try discriminate. + + inv EQ2. eapply mib_cond; eauto. + admit. + admit. + admit. + + admit. + + admit. + + admit. Admitted. Local Hint Resolve verify_block_correct: core. -- cgit From 7473fed7c8e1b2fdef276b7aa754fb00792d47ca Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 5 May 2021 19:59:47 +0200 Subject: finish verify_block and proof --- scheduling/BTL.v | 144 +++++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 123 insertions(+), 21 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 82a54061..7bc091ef 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -512,20 +512,91 @@ Proof. - intros. destruct ln'; monadInv H. constructor; eauto. Qed. +(* TODO Copied from duplicate, should we import ? *) +Lemma product_eq {A B: Type} : + (forall (a b: A), {a=b} + {a<>b}) -> + (forall (c d: B), {c=d} + {c<>d}) -> + forall (x y: A+B), {x=y} + {x<>y}. +Proof. + intros H H'. intros. decide equality. +Qed. + +(* TODO Copied from duplicate, should we import ? *) +(** FIXME Ideally i would like to put this in AST.v but i get an "illegal application" + * error when doing so *) +Remark builtin_arg_eq_pos: forall (a b: builtin_arg positive), {a=b} + {a<>b}. +Proof. + intros. + apply (builtin_arg_eq Pos.eq_dec). +Defined. +Global Opaque builtin_arg_eq_pos. + +(* TODO Copied from duplicate, should we import ? *) +Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}. +Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed. +Global Opaque builtin_res_eq_pos. + (* TODO: deuxième étape (après BTLtoRTLproof.plus_simulation) *) Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) := match ib with | BF fi => match fi with - | Bgoto pc => - match dupmap!pc with - | Some _ => OK None - | None => Error (msg "verify_block: incorrect dupmap Bgoto") + | Bgoto pc1 => + do u <- verify_is_copy dupmap pc1 pc; + if negb isfst then + OK None + else Error (msg "verify_block: isfst is true Bgoto") + | Breturn or => + match cfg!pc with + | Some (Ireturn or') => + if option_eq Pos.eq_dec or or' then OK None + else Error (msg "verify_block: different opt reg in Breturn") + | _ => Error (msg "verify_block: incorrect cfg Breturn") end - | _ => + | Bcall s ri lr r pc1 => match cfg!pc with - | Some i => Error (msg "TODO") (* TODO *) - | None => Error (msg "verify_block: incorrect cfg BF") + | Some (Icall s' ri' lr' r' pc2) => + do u <- verify_is_copy dupmap pc1 pc2; + if (signature_eq s s') then + if (product_eq Pos.eq_dec ident_eq ri ri') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then OK None + else Error (msg "verify_block: different r r' in Bcall") + else Error (msg "verify_block: different lr in Bcall") + else Error (msg "verify_block: different ri in Bcall") + else Error (msg "verify_block: different signatures in Bcall") + | _ => Error (msg "verify_block: incorrect cfg Bcall") + end + | Btailcall s ri lr => + match cfg!pc with + | Some (Itailcall s' ri' lr') => + if (signature_eq s s') then + if (product_eq Pos.eq_dec ident_eq ri ri') then + if (list_eq_dec Pos.eq_dec lr lr') then OK None + else Error (msg "verify_block: different lr in Btailcall") + else Error (msg "verify_block: different ri in Btailcall") + else Error (msg "verify_block: different signatures in Btailcall") + | _ => Error (msg "verify_block: incorrect cfg Btailcall") + end + | Bbuiltin ef la br pc1 => + match cfg!pc with + | Some (Ibuiltin ef' la' br' pc2) => + do u <- verify_is_copy dupmap pc1 pc2; + if (external_function_eq ef ef') then + if (list_eq_dec builtin_arg_eq_pos la la') then + if (builtin_res_eq_pos br br') then OK None + else Error (msg "verify_block: different brr in Bbuiltin") + else Error (msg "verify_block: different lbar in Bbuiltin") + else Error (msg "verify_block: different ef in Bbuiltin") + | _ => Error (msg "verify_block: incorrect cfg Bbuiltin") + end + | Bjumptable r ln => + match cfg!pc with + | Some (Ijumptable r' ln') => + do u <- verify_is_copy_list dupmap ln ln'; + if (Pos.eq_dec r r') then OK None + else Error (msg "verify_block: different r in Bjumptable") + | _ => Error (msg "verify_block: incorrect cfg Bjumptable") end end | Bnop => @@ -602,12 +673,51 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) end. (* This property expresses that "relation" [match_iblock] is a partial function (see also [iblock_istep_run_equiv] above) *) -Lemma verify_block_correct: forall dupmap cfg isfst pc ib fin, +Lemma verify_block_correct dupmap cfg ib: forall pc isfst fin, verify_block dupmap cfg isfst pc ib = (OK fin) -> match_iblock dupmap cfg isfst pc ib fin. Proof. induction ib; intros; try (unfold verify_block in H; destruct (cfg!pc) eqn:EQCFG; [ idtac | discriminate; fail ]). - - admit. + - (* BF *) + destruct fi; unfold verify_block in H. + + (* Bgoto *) + monadInv H. + destruct (isfst); simpl in EQ0; inv EQ0. + eapply verify_is_copy_correct in EQ. + constructor; assumption. + + (* Breturn *) + destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. + destruct (option_eq _ _ _); try discriminate. inv H. + eapply mib_BF; eauto. constructor. + + (* Bcall *) + destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. + monadInv H. + eapply verify_is_copy_correct in EQ. + destruct (signature_eq _ _); try discriminate. + destruct (product_eq _ _ _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. subst. + inv EQ0. eapply mib_BF; eauto. constructor; assumption. + + (* Btailcall *) + destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. + destruct (signature_eq _ _); try discriminate. + destruct (product_eq _ _ _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. subst. + inv H. eapply mib_BF; eauto. constructor. + + (* Bbuiltin *) + destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. + monadInv H. + eapply verify_is_copy_correct in EQ. + destruct (external_function_eq _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (builtin_res_eq_pos _ _); try discriminate. subst. + inv EQ0. eapply mib_BF; eauto. constructor; assumption. + + (* Bjumptable *) + destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. + monadInv H. + eapply verify_is_copy_list_correct in EQ. + destruct (Pos.eq_dec _ _); try discriminate. subst. + inv EQ0. eapply mib_BF; eauto. constructor; assumption. - (* Bnop *) destruct i; inv H. constructor; assumption. @@ -636,10 +746,8 @@ Proof. monadInv H. destruct x; try discriminate. eapply mib_seq_Some. - eapply IHib1; eauto. admit. - (*eapply IHib2; eauto.*) - (*destruct (cfg!pc) eqn:ECFG; try discriminate.*) - (*destruct i; try discriminate.*) + eapply IHib1; eauto. + eapply IHib2; eauto. - (* Bcond *) destruct i; try discriminate. destruct (list_eq_dec _ _ _); try discriminate. @@ -648,14 +756,8 @@ Proof. fold (verify_block dupmap cfg false n0 ib2) in H. monadInv H. destruct x, x0; try destruct (Pos.eq_dec _ _); try discriminate. - + inv EQ2. eapply mib_cond; eauto. - admit. - admit. - admit. - + admit. - + admit. - + admit. -Admitted. + all: inv EQ2; eapply mib_cond; eauto; econstructor. +Qed. Local Hint Resolve verify_block_correct: core. Fixpoint verify_blocks dupmap (cfg: code) (cfg':RTL.code) l: res unit := -- cgit From c7bc74b1860f30df678bf384a32cd9c6eb113beb Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 6 May 2021 09:07:07 +0200 Subject: start RTL -> BTL --- scheduling/BTL.v | 119 ++++++++++++++++++++++++++++++++----------------------- 1 file changed, 70 insertions(+), 49 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 7bc091ef..fb67d150 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -342,6 +342,8 @@ Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). +(** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) + (** Matching BTL and RTL code We should be able to define a single verifier able to prove a bisimulation between BTL and RTL code. @@ -429,49 +431,10 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot i) opc . -(* Partial copy of Duplicate and Duplicateproof. *) - Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop := forall pc pc', dupmap!pc = Some pc' -> exists ib, cfg!pc = Some ib /\ match_iblock dupmap cfg' true pc' ib.(entry) None. -Record match_function dupmap f f': Prop := { - dupmap_correct: match_cfg dupmap (fn_code f) (RTL.fn_code f'); - dupmap_entrypoint: dupmap!(fn_entrypoint f) = Some (RTL.fn_entrypoint f'); - preserv_fnsig: fn_sig f = RTL.fn_sig f'; - preserv_fnparams: fn_params f = RTL.fn_params f'; - preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f' -}. - -Inductive match_fundef: fundef -> RTL.fundef -> Prop := - | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f') - | match_External ef: match_fundef (External ef) (External ef). - -Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop := - | match_stackframe_intro - dupmap res f sp pc rs f' pc' - (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc = Some pc') - : match_stackframes (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). - -Inductive match_states: state -> RTL.state -> Prop := - | match_states_intro - dupmap st f sp pc rs m st' f' pc' - (STACKS: list_forall2 match_stackframes st st') - (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc = Some pc') - : match_states (State st f sp pc rs m) (RTL.State st' f' sp pc' rs m) - | match_states_call - st st' f f' args m - (STACKS: list_forall2 match_stackframes st st') - (TRANSF: match_fundef f f') - : match_states (Callstate st f args m) (RTL.Callstate st' f' args m) - | match_states_return - st st' v m - (STACKS: list_forall2 match_stackframes st st') - : match_states (Returnstate st v m) (RTL.Returnstate st' v m) - . - (** Shared verifier between RTL -> BTL and BTL -> RTL *) Local Open Scope error_monad_scope. @@ -536,7 +499,6 @@ Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}. Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed. Global Opaque builtin_res_eq_pos. -(* TODO: deuxième étape (après BTLtoRTLproof.plus_simulation) *) Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) := match ib with | BF fi => @@ -801,14 +763,73 @@ Definition verify_function dupmap f f' : res unit := do _ <- verify_is_copy dupmap (fn_entrypoint f) (RTL.fn_entrypoint f'); verify_cfg dupmap (fn_code f) (RTL.fn_code f'). -Lemma verify_function_correct dupmap f f' tt: - verify_function dupmap f f' = OK tt -> - fn_sig f = RTL.fn_sig f' -> - fn_params f = RTL.fn_params f' -> - fn_stacksize f = RTL.fn_stacksize f' -> - match_function dupmap f f'. +Definition is_seq (ib: iblock): bool := + match ib with + | Bseq _ _ => true + | _ => false + end. + +Definition is_atom (ib: iblock): bool := + match ib with + | Bseq _ _ | Bcond _ _ _ _ _ => false + | _ => true + end. + + +Inductive is_right_assoc: iblock -> Prop := + | ira_Bseq ib1 ib2: + is_seq ib1 = false -> + is_right_assoc ib1 -> + is_right_assoc ib2 -> + is_right_assoc (Bseq ib1 ib2) + | ira_Bcond cond args ib1 ib2 i: + is_right_assoc ib1 -> + is_right_assoc ib2 -> + is_right_assoc (Bcond cond args ib1 ib2 i) + | ira_others ib: + is_atom ib = true -> + is_right_assoc ib + . +Local Hint Constructors is_right_assoc: core. + +Fixpoint right_assoc (ib: iblock): iblock := + match ib with + | Bseq ib1 ib2 => rec_rotate ib1 (right_assoc ib2) + | Bcond cond args ib1 ib2 i => + Bcond cond args (right_assoc ib1) (right_assoc ib2) i + | ib => ib + end +with rec_rotate (ib: iblock) rem: iblock := + match ib with + | Bseq ib1 ib2 => + rec_rotate ib1 (rec_rotate ib2 rem) + | Bcond cond args ib1 ib2 i => + Bseq (Bcond cond args (right_assoc ib1) (right_assoc ib2) i) rem + | ib => Bseq ib rem +end. + +Lemma right_assoc_rec_rotate_correct ib: + is_right_assoc (right_assoc ib) + /\ (forall rem, is_right_assoc rem -> is_right_assoc (rec_rotate ib rem)). Proof. - unfold verify_function; intro VERIF. monadInv VERIF. - constructor; eauto. - eapply verify_cfg_correct; eauto. + induction ib; simpl; intuition. Qed. + +Lemma right_assoc_correct ib: + is_right_assoc (right_assoc ib). +Proof. + destruct (right_assoc_rec_rotate_correct ib); auto. +Qed. + +Definition right_assoc_code (cfg: code): code := + (PTree.map (fun _ ib => {| entry:=right_assoc ib.(entry); input_regs := ib.(input_regs) |}) cfg). + +Lemma right_assoc_code_correct cfg pc ib : + (right_assoc_code cfg)!pc=Some ib -> is_right_assoc (ib.(entry)). +Proof. + unfold right_assoc_code. + rewrite PTree.gmap. + destruct (cfg!pc); simpl; intros; try_simplify_someHyps. + apply right_assoc_correct; auto. +Qed. + -- cgit From 1d32156c5bc43f966abe2c12c317a27e092355c4 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 7 May 2021 17:30:43 +0200 Subject: idea of a new scheme to define the semantics of LOAD NOTRAP --- scheduling/BTL.v | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index fb67d150..8ccab024 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -175,6 +175,23 @@ Definition find_function (ros: reg + ident) (rs: regset) : option fundef := Local Open Scope option_monad_scope. +(* (* TODO: a new (hopefully simpler) scheme to support "NOTRAP" wrt current scheme of RTL *) + +Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop := + | has_loaded_normal a trap + (EVAL: eval_addressing ge sp addr rs##args = Some a) + (LOAD: Mem.loadv chunk m a = Some v) + : has_loaded sp rs m chunk addr args v trap + | has_loaded_default + (LOAD: forall a, eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = None) + (DEFAULT: v = default_notrap_load_value chunk) + : has_loaded sp rs m chunk addr args v NOTRAP + . + +(* TODO: move this scheme in "Memory" module if this scheme is useful ! *) + +*) + (** internal big-step execution of one iblock *) Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop := | exec_final rs m fin: iblock_istep sp rs m (BF fin) rs m (Some fin) @@ -186,6 +203,11 @@ Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option fi (EVAL: eval_addressing ge sp addr rs##args = Some a) (LOAD: Mem.loadv chunk m a = Some v) : iblock_istep sp rs m (Bload TRAP chunk addr args dst) (rs#dst <- v) m None +(* TODO: replace [exec_load_TRAP] above by this one. See "new scheme" for "NOTRAP" above + | exec_load rs m trap chunk addr args dst v + (LOAD: has_loaded sp rs m chunk addr args v trap) + : iblock_istep sp rs m (Bload trap chunk addr args dst) (rs#dst <- v) m None +*) | exec_store rs m chunk addr args src a m' (EVAL: eval_addressing ge sp addr rs##args = Some a) (STORE: Mem.storev chunk m a rs#src = Some m') -- cgit From 08b39b2025951a9655939c1377f6e53b346c6821 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 7 May 2021 19:58:02 +0200 Subject: Some advance in proof and NOTRAP loads fix --- scheduling/BTL.v | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index fb67d150..c8dfa0af 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -400,9 +400,9 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i | mib_op isfst pc pc' op lr r: cfg!pc = Some (Iop op lr r pc') -> match_iblock dupmap cfg isfst pc (Bop op lr r) (Some pc') - | mib_load isfst pc pc' tm m a lr r: - cfg!pc = Some (Iload tm m a lr r pc') -> - match_iblock dupmap cfg isfst pc (Bload tm m a lr r) (Some pc') + | mib_load isfst pc pc' m a lr r: + cfg!pc = Some (Iload TRAP m a lr r pc') -> + match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r) (Some pc') | mib_store isfst pc pc' m a lr r: cfg!pc = Some (Istore m a lr r pc') -> match_iblock dupmap cfg isfst pc (Bstore m a lr r) (Some pc') @@ -581,7 +581,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) | Bload tm m a lr r => match cfg!pc with | Some (Iload tm' m' a' lr' r' pc') => - if (trapping_mode_eq tm tm') then + if (trapping_mode_eq tm TRAP && trapping_mode_eq tm' TRAP) then if (chunk_eq m m') then if (eq_addressing a a') then if (list_eq_dec Pos.eq_dec lr lr') then @@ -591,7 +591,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "verify_block: different lr in Bload") else Error (msg "verify_block: different addressing in Bload") else Error (msg "verify_block: different mchunk in Bload") - else Error (msg "verify_block: different trapping_mode in Bload") + else Error (msg "verify_block: NOTRAP trapping_mode unsupported in Bload") | _ => Error (msg "verify_block: incorrect cfg Bload") end | Bstore m a lr r => @@ -691,7 +691,8 @@ Proof. constructor; assumption. - (* Bload *) destruct i; try discriminate. - destruct (trapping_mode_eq _ _); try discriminate. + do 2 (destruct (trapping_mode_eq _ _); try discriminate). + simpl in H. destruct (chunk_eq _ _); try discriminate. destruct (eq_addressing _ _); try discriminate. destruct (list_eq_dec _ _ _); try discriminate. -- cgit From a1cde0686dfb40595423f40ccc40e18de3539e52 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Sat, 8 May 2021 07:31:05 +0200 Subject: idee pour simplifier la preuve: restreindre le "right_assoc" en "expand" ! --- scheduling/BTL.v | 66 +++++++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 61 insertions(+), 5 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 8ccab024..7f3d327b 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -785,11 +785,6 @@ Definition verify_function dupmap f f' : res unit := do _ <- verify_is_copy dupmap (fn_entrypoint f) (RTL.fn_entrypoint f'); verify_cfg dupmap (fn_code f) (RTL.fn_code f'). -Definition is_seq (ib: iblock): bool := - match ib with - | Bseq _ _ => true - | _ => false - end. Definition is_atom (ib: iblock): bool := match ib with @@ -797,6 +792,67 @@ Definition is_atom (ib: iblock): bool := | _ => true end. +Inductive is_expand: iblock -> Prop := + | exp_Bseq ib1 ib2: + is_atom ib1 = true -> + is_expand ib2 -> + is_expand (Bseq ib1 ib2) + | exp_Bcond cond args ib1 ib2 i: + is_expand ib1 -> + is_expand ib2 -> + is_expand (Bcond cond args ib1 ib2 i) + | exp_others ib: + is_atom ib = true -> + is_expand ib + . +Local Hint Constructors is_expand: core. + +Fixpoint expand (ib: iblock) (k: option iblock): iblock := + match ib with + | Bseq ib1 ib2 => expand ib1 (Some (expand ib2 k)) + | Bcond cond args ib1 ib2 i => + Bcond cond args (expand ib1 k) (expand ib2 k) i + | ib => + match k with + | None => ib + | Some rem => Bseq ib rem + end + end. + +Lemma expand_correct ib: forall k, + (match k with Some rem => is_expand rem | None => True end) + -> is_expand (expand ib k). +Proof. + induction ib; simpl; intros; try autodestruct; auto. +Qed. + +Lemma expand_None_correct ib: + is_expand (expand ib None). +Proof. + apply expand_correct; simpl; auto. +Qed. + +Definition expand_code (cfg: code): code := + (PTree.map (fun _ ib => {| entry:=expand ib.(entry) None; input_regs := ib.(input_regs) |}) cfg). + +Lemma expand_code_correct cfg pc ib : + (expand_code cfg)!pc=Some ib -> is_expand (ib.(entry)). +Proof. + unfold expand_code. + rewrite PTree.gmap. + destruct (cfg!pc); simpl; intros; try_simplify_someHyps. + apply expand_None_correct; auto. +Qed. + + +(* TODO: eliminer toute la suite quand "right_assoc" sera remplace par "expand" *) + +Definition is_seq (ib: iblock): bool := + match ib with + | Bseq _ _ => true + | _ => false + end. + Inductive is_right_assoc: iblock -> Prop := | ira_Bseq ib1 ib2: -- cgit From 895470548b89f00111d1f98ae52d217b9fd15643 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 10 May 2021 12:22:34 +0200 Subject: Some more proof cases, comments and cleanup --- scheduling/BTL.v | 69 +------------------------------------------------------- 1 file changed, 1 insertion(+), 68 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index d7ffa118..a87f674b 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -793,6 +793,7 @@ Definition is_atom (ib: iblock): bool := | _ => true end. +(** Is expand property to only support atomic instructions on the left part of a Bseq *) Inductive is_expand: iblock -> Prop := | exp_Bseq ib1 ib2: is_atom ib1 = true -> @@ -844,71 +845,3 @@ Proof. destruct (cfg!pc); simpl; intros; try_simplify_someHyps. apply expand_None_correct; auto. Qed. - - -(* TODO: eliminer toute la suite quand "right_assoc" sera remplace par "expand" *) - -Definition is_seq (ib: iblock): bool := - match ib with - | Bseq _ _ => true - | _ => false - end. - - -Inductive is_right_assoc: iblock -> Prop := - | ira_Bseq ib1 ib2: - is_seq ib1 = false -> - is_right_assoc ib1 -> - is_right_assoc ib2 -> - is_right_assoc (Bseq ib1 ib2) - | ira_Bcond cond args ib1 ib2 i: - is_right_assoc ib1 -> - is_right_assoc ib2 -> - is_right_assoc (Bcond cond args ib1 ib2 i) - | ira_others ib: - is_atom ib = true -> - is_right_assoc ib - . -Local Hint Constructors is_right_assoc: core. - -Fixpoint right_assoc (ib: iblock): iblock := - match ib with - | Bseq ib1 ib2 => rec_rotate ib1 (right_assoc ib2) - | Bcond cond args ib1 ib2 i => - Bcond cond args (right_assoc ib1) (right_assoc ib2) i - | ib => ib - end -with rec_rotate (ib: iblock) rem: iblock := - match ib with - | Bseq ib1 ib2 => - rec_rotate ib1 (rec_rotate ib2 rem) - | Bcond cond args ib1 ib2 i => - Bseq (Bcond cond args (right_assoc ib1) (right_assoc ib2) i) rem - | ib => Bseq ib rem -end. - -Lemma right_assoc_rec_rotate_correct ib: - is_right_assoc (right_assoc ib) - /\ (forall rem, is_right_assoc rem -> is_right_assoc (rec_rotate ib rem)). -Proof. - induction ib; simpl; intuition. -Qed. - -Lemma right_assoc_correct ib: - is_right_assoc (right_assoc ib). -Proof. - destruct (right_assoc_rec_rotate_correct ib); auto. -Qed. - -Definition right_assoc_code (cfg: code): code := - (PTree.map (fun _ ib => {| entry:=right_assoc ib.(entry); input_regs := ib.(input_regs) |}) cfg). - -Lemma right_assoc_code_correct cfg pc ib : - (right_assoc_code cfg)!pc=Some ib -> is_right_assoc (ib.(entry)). -Proof. - unfold right_assoc_code. - rewrite PTree.gmap. - destruct (cfg!pc); simpl; intros; try_simplify_someHyps. - apply right_assoc_correct; auto. -Qed. - -- cgit From e3613e0614ccc93c1013f7c39b58cffb6c21a76c Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 10 May 2021 17:49:29 +0200 Subject: new strong_state predicate and lemma --- scheduling/BTL.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index a87f674b..bc0f0815 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -786,6 +786,11 @@ Definition verify_function dupmap f f' : res unit := do _ <- verify_is_copy dupmap (fn_entrypoint f) (RTL.fn_entrypoint f'); verify_cfg dupmap (fn_code f) (RTL.fn_code f'). +Definition is_goto (ib: iblock): bool := + match ib with + | Bgoto _ => true + | _ => false + end. Definition is_atom (ib: iblock): bool := match ib with -- cgit From 95b6814a1cff386150a7573cb30e9cb68a18052c Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 10 May 2021 20:07:29 +0200 Subject: prove sexec_exact --- scheduling/BTL.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index a87f674b..476e71a7 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -153,7 +153,7 @@ Inductive state : Type := state. (** outcome of a block execution *) -Record outcome := { +Record outcome := out { _rs: regset; _m: mem; _fin: option final -- cgit From 99e735af1f7726da2903409758bee202cf47c6a4 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 17 May 2021 16:02:57 +0200 Subject: Lemmas on ISTEP --- scheduling/BTL.v | 1 + 1 file changed, 1 insertion(+) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 064297f1..d55a0415 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -819,6 +819,7 @@ Fixpoint expand (ib: iblock) (k: option iblock): iblock := | Bseq ib1 ib2 => expand ib1 (Some (expand ib2 k)) | Bcond cond args ib1 ib2 i => Bcond cond args (expand ib1 k) (expand ib2 k) i + | BF fin => fin | ib => match k with | None => ib -- cgit From ee558407e59c6794daad70aab2e1e7794535367e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 17 May 2021 19:12:46 +0200 Subject: finishing RTLtoBTL --- scheduling/BTL.v | 18 ------------------ 1 file changed, 18 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index d55a0415..10a000a8 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -833,21 +833,3 @@ Lemma expand_correct ib: forall k, Proof. induction ib; simpl; intros; try autodestruct; auto. Qed. - -Lemma expand_None_correct ib: - is_expand (expand ib None). -Proof. - apply expand_correct; simpl; auto. -Qed. - -Definition expand_code (cfg: code): code := - (PTree.map (fun _ ib => {| entry:=expand ib.(entry) None; input_regs := ib.(input_regs) |}) cfg). - -Lemma expand_code_correct cfg pc ib : - (expand_code cfg)!pc=Some ib -> is_expand (ib.(entry)). -Proof. - unfold expand_code. - rewrite PTree.gmap. - destruct (cfg!pc); simpl; intros; try_simplify_someHyps. - apply expand_None_correct; auto. -Qed. -- cgit From bf443e2f2bf38c30c9b68020c7c43cd7b3e10549 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 17 May 2021 23:19:16 +0200 Subject: preparing compiler passes and ml oracles --- scheduling/BTL.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 10a000a8..9fdf39be 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -463,8 +463,8 @@ Local Open Scope error_monad_scope. Definition verify_is_copy dupmap n n' := match dupmap!n with - | None => Error(msg "verify_is_copy None") - | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end + | None => Error(msg "BTL.verify_is_copy None") + | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "BTL.verify_is_copy invalid map") end end. Fixpoint verify_is_copy_list dupmap ln ln' := @@ -472,9 +472,9 @@ Fixpoint verify_is_copy_list dupmap ln ln' := | n::ln => match ln' with | n'::ln' => do _ <- verify_is_copy dupmap n n'; verify_is_copy_list dupmap ln ln' - | nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end + | nil => Error (msg "BTL.verify_is_copy_list: ln' bigger than ln") end | nil => match ln' with - | n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'") + | n :: ln' => Error (msg "BTL.verify_is_copy_list: ln bigger than ln'") | nil => OK tt end end. -- cgit From c27d87ffe33242840964dd9bd67090409eea79a5 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 18 May 2021 16:55:56 +0200 Subject: oracle simplification, BTL printer, and error msg spec --- scheduling/BTL.v | 82 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 41 insertions(+), 41 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 9fdf39be..3daa40c4 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -529,13 +529,13 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) do u <- verify_is_copy dupmap pc1 pc; if negb isfst then OK None - else Error (msg "verify_block: isfst is true Bgoto") + else Error (msg "BTL.verify_block: isfst is true Bgoto") | Breturn or => match cfg!pc with | Some (Ireturn or') => if option_eq Pos.eq_dec or or' then OK None - else Error (msg "verify_block: different opt reg in Breturn") - | _ => Error (msg "verify_block: incorrect cfg Breturn") + else Error (msg "BTL.verify_block: different opt reg in Breturn") + | _ => Error (msg "BTL.verify_block: incorrect cfg Breturn") end | Bcall s ri lr r pc1 => match cfg!pc with @@ -545,11 +545,11 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (product_eq Pos.eq_dec ident_eq ri ri') then if (list_eq_dec Pos.eq_dec lr lr') then if (Pos.eq_dec r r') then OK None - else Error (msg "verify_block: different r r' in Bcall") - else Error (msg "verify_block: different lr in Bcall") - else Error (msg "verify_block: different ri in Bcall") - else Error (msg "verify_block: different signatures in Bcall") - | _ => Error (msg "verify_block: incorrect cfg Bcall") + else Error (msg "BTL.verify_block: different r r' in Bcall") + else Error (msg "BTL.verify_block: different lr in Bcall") + else Error (msg "BTL.verify_block: different ri in Bcall") + else Error (msg "BTL.verify_block: different signatures in Bcall") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bcall") end | Btailcall s ri lr => match cfg!pc with @@ -557,10 +557,10 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (signature_eq s s') then if (product_eq Pos.eq_dec ident_eq ri ri') then if (list_eq_dec Pos.eq_dec lr lr') then OK None - else Error (msg "verify_block: different lr in Btailcall") - else Error (msg "verify_block: different ri in Btailcall") - else Error (msg "verify_block: different signatures in Btailcall") - | _ => Error (msg "verify_block: incorrect cfg Btailcall") + else Error (msg "BTL.verify_block: different lr in Btailcall") + else Error (msg "BTL.verify_block: different ri in Btailcall") + else Error (msg "BTL.verify_block: different signatures in Btailcall") + | _ => Error (msg "BTL.verify_block: incorrect cfg Btailcall") end | Bbuiltin ef la br pc1 => match cfg!pc with @@ -569,24 +569,24 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (external_function_eq ef ef') then if (list_eq_dec builtin_arg_eq_pos la la') then if (builtin_res_eq_pos br br') then OK None - else Error (msg "verify_block: different brr in Bbuiltin") - else Error (msg "verify_block: different lbar in Bbuiltin") - else Error (msg "verify_block: different ef in Bbuiltin") - | _ => Error (msg "verify_block: incorrect cfg Bbuiltin") + else Error (msg "BTL.verify_block: different brr in Bbuiltin") + else Error (msg "BTL.verify_block: different lbar in Bbuiltin") + else Error (msg "BTL.verify_block: different ef in Bbuiltin") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bbuiltin") end | Bjumptable r ln => match cfg!pc with | Some (Ijumptable r' ln') => do u <- verify_is_copy_list dupmap ln ln'; if (Pos.eq_dec r r') then OK None - else Error (msg "verify_block: different r in Bjumptable") - | _ => Error (msg "verify_block: incorrect cfg Bjumptable") + else Error (msg "BTL.verify_block: different r in Bjumptable") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bjumptable") end end | Bnop => match cfg!pc with | Some (Inop pc') => OK (Some pc') - | _ => Error (msg "verify_block: incorrect cfg Bnop") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop") end | Bop op lr r => match cfg!pc with @@ -595,10 +595,10 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (list_eq_dec Pos.eq_dec lr lr') then if (Pos.eq_dec r r') then OK (Some pc') - else Error (msg "verify_block: different r in Bop") - else Error (msg "verify_block: different lr in Bop") - else Error (msg "verify_block: different operations in Bop") - | _ => Error (msg "verify_block: incorrect cfg Bop") + else Error (msg "BTL.verify_block: different r in Bop") + else Error (msg "BTL.verify_block: different lr in Bop") + else Error (msg "BTL.verify_block: different operations in Bop") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bop") end | Bload tm m a lr r => match cfg!pc with @@ -609,12 +609,12 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (list_eq_dec Pos.eq_dec lr lr') then if (Pos.eq_dec r r') then OK (Some pc') - else Error (msg "verify_block: different r in Bload") - else Error (msg "verify_block: different lr in Bload") - else Error (msg "verify_block: different addressing in Bload") - else Error (msg "verify_block: different mchunk in Bload") - else Error (msg "verify_block: NOTRAP trapping_mode unsupported in Bload") - | _ => Error (msg "verify_block: incorrect cfg Bload") + else Error (msg "BTL.verify_block: different r in Bload") + else Error (msg "BTL.verify_block: different lr in Bload") + else Error (msg "BTL.verify_block: different addressing in Bload") + else Error (msg "BTL.verify_block: different mchunk in Bload") + else Error (msg "BTL.verify_block: NOTRAP trapping_mode unsupported in Bload") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bload") end | Bstore m a lr r => match cfg!pc with @@ -623,18 +623,18 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (eq_addressing a a') then if (list_eq_dec Pos.eq_dec lr lr') then if (Pos.eq_dec r r') then OK (Some pc') - else Error (msg "verify_block: different r in Bstore") - else Error (msg "verify_block: different lr in Bstore") - else Error (msg "verify_block: different addressing in Bstore") - else Error (msg "verify_block: different mchunk in Bstore") - | _ => Error (msg "verify_block: incorrect cfg Bstore") + else Error (msg "BTL.verify_block: different r in Bstore") + else Error (msg "BTL.verify_block: different lr in Bstore") + else Error (msg "BTL.verify_block: different addressing in Bstore") + else Error (msg "BTL.verify_block: different mchunk in Bstore") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bstore") end | Bseq b1 b2 => do opc <- verify_block dupmap cfg isfst pc b1; match opc with | Some pc' => verify_block dupmap cfg false pc' b2 - | None => Error (msg "verify_block: None next pc in Bseq (deadcode)") + | None => Error (msg "BTL.verify_block: None next pc in Bseq (deadcode)") end | Bcond c lr bso bnot i => match cfg!pc with @@ -648,11 +648,11 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) | o, None => OK o | Some x, Some x' => if Pos.eq_dec x x' then OK (Some x) - else Error (msg "verify_block: is_join_opt incorrect for Bcond") + else Error (msg "BTL.verify_block: is_join_opt incorrect for Bcond") end - else Error (msg "verify_block: incompatible conditions in Bcond") - else Error (msg "verify_block: different lr in Bcond") - | _ => Error (msg "verify_block: incorrect cfg Bcond") + else Error (msg "BTL.verify_block: incompatible conditions in Bcond") + else Error (msg "BTL.verify_block: different lr in Bcond") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bcond") end end. @@ -753,9 +753,9 @@ Fixpoint verify_blocks dupmap (cfg: code) (cfg':RTL.code) l: res unit := | Some ib => do o <- verify_block dupmap cfg' true pc' ib.(entry); match o with | None => verify_blocks dupmap cfg cfg' l - | _ => Error(msg "verify_blocks.end") + | _ => Error(msg "BTL.verify_blocks.end") end - | _ => Error(msg "verify_blocks.entry") + | _ => Error(msg "BTL.verify_blocks.entry") end end. -- cgit From 9f252d9055ad16f9433caaf41f6490e45424e88a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 19 May 2021 15:53:02 +0200 Subject: Adding a BTL record to help oracles --- scheduling/BTL.v | 143 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 74 insertions(+), 69 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 3daa40c4..44c25b75 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -23,24 +23,29 @@ Require Import RTL Op Registers OptionMonad. Definition exit := node. (* we may generalize this with register renamings at exit, like in "phi" nodes of SSA-form *) +(* node_info is a ghost record to provide and transfert information through oracles *) +Record node_info := { + _pos: node +}. + (** final instructions (that stops block execution) *) Inductive final: Type := | Bgoto (succ:exit) (** No operation -- just branch to [succ]. *) - | Breturn (res: option reg) + | Breturn (res: option reg) (ni: node_info) (** terminates the execution of the current function. It returns the value of the given register, or [Vundef] if none is given. *) - | Bcall (sig: signature) (fn: reg + ident) (args:list reg) (dest:reg) (succ:exit) + | Bcall (sig: signature) (fn: reg + ident) (args:list reg) (dest:reg) (succ:exit) (ni: node_info) (** invokes the function determined by [fn] (either a function pointer found in a register or a function name), giving it the values of registers [args] as arguments. It stores the return value in [dest] and branches to [succ]. *) - | Btailcall (sig:signature) (fn: reg + ident) (args: list reg) + | Btailcall (sig:signature) (fn: reg + ident) (args: list reg) (ni: node_info) (** performs a function invocation in tail-call position (the current function terminates after the call, returning the result of the callee) *) - | Bbuiltin (ef:external_function) (args:list (builtin_arg reg)) (dest:builtin_res reg) (succ:exit) + | Bbuiltin (ef:external_function) (args:list (builtin_arg reg)) (dest:builtin_res reg) (succ:exit) (ni: node_info) (** calls the built-in function identified by [ef], giving it the values of [args] as arguments. It stores the return value in [dest] and branches to [succ]. *) - | Bjumptable (arg:reg) (tbl:list exit) + | Bjumptable (arg:reg) (tbl:list exit) (ni: node_info) (** [Bjumptable arg tbl] transitions to the node that is the [n]-th element of the list [tbl], where [n] is the unsigned integer value of register [arg]. *) . @@ -50,14 +55,14 @@ Inductive iblock: Type := (* final instructions that stops block execution *) | BF (fi: final) (* basic instructions that continues block execution, except when aborting *) - | Bnop (* nop instruction *) - | Bop (op:operation) (args:list reg) (dest:reg) + | Bnop (ni: node_info) (* nop instruction *) + | Bop (op:operation) (args:list reg) (dest:reg) (ni: node_info) (** performs the arithmetic operation [op] over the values of registers [args], stores the result in [dest] *) - | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg) + | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg) (ni: node_info) (** loads a [chunk] quantity from the address determined by the addressing mode [addr] and the values of the [args] registers, stores the quantity just read into [dest]. If trap=NOTRAP, then failures lead to a default value written to [dest]. *) - | Bstore (chunk:memory_chunk) (addr:addressing) (args:list reg) (src:reg) + | Bstore (chunk:memory_chunk) (addr:addressing) (args:list reg) (src:reg) (ni: node_info) (** stores the value of register [src] in the [chunk] quantity at the the address determined by the addressing mode [addr] and the values of the [args] registers. *) @@ -65,7 +70,7 @@ Inductive iblock: Type := | Bseq (b1 b2: iblock) (** starts by running [b1] and stops here if execution of [b1] has reached a final instruction or aborted or continue with [b2] otherwise *) - | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock) (info:option bool) + | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock) (info:option bool) (ni: node_info) (** evaluates the boolean condition [cond] over the values of registers [args]. If the condition is true, it continues on [ifso]. If the condition is false, it continues on [ifnot]. @@ -195,23 +200,23 @@ Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop := (** internal big-step execution of one iblock *) Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop := | exec_final rs m fin: iblock_istep sp rs m (BF fin) rs m (Some fin) - | exec_nop rs m: iblock_istep sp rs m Bnop rs m None - | exec_op rs m op args res v + | exec_nop rs m ni: iblock_istep sp rs m (Bnop ni) rs m None + | exec_op rs m op args res v ni (EVAL: eval_operation ge sp op rs##args m = Some v) - : iblock_istep sp rs m (Bop op args res) (rs#res <- v) m None - | exec_load_TRAP rs m chunk addr args dst a v + : iblock_istep sp rs m (Bop op args res ni) (rs#res <- v) m None + | exec_load_TRAP rs m chunk addr args dst a v ni (EVAL: eval_addressing ge sp addr rs##args = Some a) (LOAD: Mem.loadv chunk m a = Some v) - : iblock_istep sp rs m (Bload TRAP chunk addr args dst) (rs#dst <- v) m None + : iblock_istep sp rs m (Bload TRAP chunk addr args dst ni) (rs#dst <- v) m None (* TODO: replace [exec_load_TRAP] above by this one. See "new scheme" for "NOTRAP" above | exec_load rs m trap chunk addr args dst v (LOAD: has_loaded sp rs m chunk addr args v trap) : iblock_istep sp rs m (Bload trap chunk addr args dst) (rs#dst <- v) m None *) - | exec_store rs m chunk addr args src a m' + | exec_store rs m chunk addr args src a m' ni (EVAL: eval_addressing ge sp addr rs##args = Some a) (STORE: Mem.storev chunk m a rs#src = Some m') - : iblock_istep sp rs m (Bstore chunk addr args src) rs m' None + : iblock_istep sp rs m (Bstore chunk addr args src ni) rs m' None | exec_seq_stop rs m b1 b2 rs' m' fin (EXEC: iblock_istep sp rs m b1 rs' m' (Some fin)) : iblock_istep sp rs m (Bseq b1 b2) rs' m' (Some fin) @@ -219,10 +224,10 @@ Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option fi (EXEC1: iblock_istep sp rs m b1 rs1 m1 None) (EXEC2: iblock_istep sp rs1 m1 b2 rs' m' ofin) : iblock_istep sp rs m (Bseq b1 b2) rs' m' ofin - | exec_cond rs m cond args ifso ifnot i b rs' m' ofin + | exec_cond rs m cond args ifso ifnot i b rs' m' ofin ni (EVAL: eval_condition cond rs##args m = Some b) (EXEC: iblock_istep sp rs m (if b then ifso else ifnot) rs' m' ofin) - : iblock_istep sp rs m (Bcond cond args ifso ifnot i) rs' m' ofin + : iblock_istep sp rs m (Bcond cond args ifso ifnot i ni) rs' m' ofin . Local Hint Constructors iblock_istep: core. @@ -234,18 +239,18 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome := | BF fin => Some {| _rs := rs; _m := m; _fin := Some fin |} (* basic instructions *) - | Bnop => + | Bnop _ => Some {| _rs := rs; _m:= m; _fin := None |} - | Bop op args res => + | Bop op args res _ => SOME v <- eval_operation ge sp op rs##args m IN Some {| _rs := rs#res <- v; _m:= m; _fin := None |} - | Bload TRAP chunk addr args dst => + | Bload TRAP chunk addr args dst _ => SOME a <- eval_addressing ge sp addr rs##args IN SOME v <- Mem.loadv chunk m a IN Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} - | Bload NOTRAP chunk addr args dst => + | Bload NOTRAP chunk addr args dst _ => None (* TODO *) - | Bstore chunk addr args src => + | Bstore chunk addr args src _ => SOME a <- eval_addressing ge sp addr rs##args IN SOME m' <- Mem.storev chunk m a rs#src IN Some {| _rs := rs; _m:= m'; _fin := None |} @@ -256,7 +261,7 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome := | None => iblock_istep_run sp b2 out1.(_rs) out1.(_m) | _ => Some out1 (* stop execution on the 1st final instruction *) end - | Bcond cond args ifso ifnot _ => + | Bcond cond args ifso ifnot _ _ => SOME b <- eval_condition cond rs##args m IN iblock_istep_run sp (if b then ifso else ifnot) rs m end. @@ -275,32 +280,32 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := | exec_Bgoto pc: final_step stack f sp rs m (Bgoto pc) E0 (State stack f sp pc rs m) - | exec_Breturn or stk m': + | exec_Breturn or stk m' ni: sp = (Vptr stk Ptrofs.zero) -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - final_step stack f sp rs m (Breturn or) + final_step stack f sp rs m (Breturn or ni) E0 (Returnstate stack (regmap_optget or Vundef rs) m') - | exec_Bcall sig ros args res pc' fd: + | exec_Bcall sig ros args res pc' fd ni: find_function ros rs = Some fd -> funsig fd = sig -> - final_step stack f sp rs m (Bcall sig ros args res pc') + final_step stack f sp rs m (Bcall sig ros args res pc' ni) E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m) - | exec_Btailcall sig ros args stk m' fd: + | exec_Btailcall sig ros args stk m' fd ni: find_function ros rs = Some fd -> funsig fd = sig -> sp = (Vptr stk Ptrofs.zero) -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - final_step stack f sp rs m (Btailcall sig ros args) + final_step stack f sp rs m (Btailcall sig ros args ni) E0 (Callstate stack fd rs##args m') - | exec_Bbuiltin ef args res pc' vargs t vres m': + | exec_Bbuiltin ef args res pc' vargs t vres m' ni: eval_builtin_args ge (fun r => rs#r) sp m args vargs -> external_call ef ge vargs m t vres m' -> - final_step stack f sp rs m (Bbuiltin ef args res pc') + final_step stack f sp rs m (Bbuiltin ef args res pc' ni) t (State stack f sp pc' (regmap_setres res vres rs) m') - | exec_Bjumptable arg tbl n pc': + | exec_Bjumptable arg tbl n pc' ni: rs#arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some pc' -> - final_step stack f sp rs m (Bjumptable arg tbl) + final_step stack f sp rs m (Bjumptable arg tbl ni) E0 (State stack f sp pc' rs m) . @@ -388,16 +393,16 @@ Inductive match_final_inst (dupmap: PTree.t node): final -> instruction -> Prop | mfi_goto pc pc': dupmap!pc = (Some pc') -> match_final_inst dupmap (Bgoto pc) (Inop pc') *) - | mfi_return or: match_final_inst dupmap (Breturn or) (Ireturn or) - | mfi_call pc pc' s ri lr r: - dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc) (Icall s ri lr r pc') - | mfi_tailcall s ri lr: - match_final_inst dupmap (Btailcall s ri lr) (Itailcall s ri lr) - | mfi_builtin pc pc' ef la br: - dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc) (Ibuiltin ef la br pc') - | mfi_jumptable ln ln' r: + | mfi_return or ni: match_final_inst dupmap (Breturn or ni) (Ireturn or) + | mfi_call pc pc' s ri lr r ni: + dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc ni) (Icall s ri lr r pc') + | mfi_tailcall s ri lr ni: + match_final_inst dupmap (Btailcall s ri lr ni) (Itailcall s ri lr) + | mfi_builtin pc pc' ef la br ni: + dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc ni) (Ibuiltin ef la br pc') + | mfi_jumptable ln ln' r ni: list_forall2 (fun pc pc' => (dupmap!pc = (Some pc'))) ln ln' -> - match_final_inst dupmap (Bjumptable r ln) (Ijumptable r ln') + match_final_inst dupmap (Bjumptable r ln ni) (Ijumptable r ln') . Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop := @@ -416,18 +421,18 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i cfg!pc = Some i -> match_final_inst dupmap fi i -> match_iblock dupmap cfg isfst pc (BF fi) None - | mib_nop isfst pc pc': + | mib_nop isfst pc pc' ni: cfg!pc = Some (Inop pc') -> - match_iblock dupmap cfg isfst pc Bnop (Some pc') - | mib_op isfst pc pc' op lr r: + match_iblock dupmap cfg isfst pc (Bnop ni) (Some pc') + | mib_op isfst pc pc' op lr r ni: cfg!pc = Some (Iop op lr r pc') -> - match_iblock dupmap cfg isfst pc (Bop op lr r) (Some pc') - | mib_load isfst pc pc' m a lr r: + match_iblock dupmap cfg isfst pc (Bop op lr r ni) (Some pc') + | mib_load isfst pc pc' m a lr r ni: cfg!pc = Some (Iload TRAP m a lr r pc') -> - match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r) (Some pc') - | mib_store isfst pc pc' m a lr r: + match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r ni) (Some pc') + | mib_store isfst pc pc' m a lr r ni: cfg!pc = Some (Istore m a lr r pc') -> - match_iblock dupmap cfg isfst pc (Bstore m a lr r) (Some pc') + match_iblock dupmap cfg isfst pc (Bstore m a lr r ni) (Some pc') | mib_exit pc pc': dupmap!pc = (Some pc') -> match_iblock dupmap cfg false pc' (Bgoto pc) None @@ -445,12 +450,12 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i And the verifier could fail if there is such dead code! *) *) - | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i i': + | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i i' ni: cfg!pc = Some (Icond c lr pcso pcnot i') -> match_iblock dupmap cfg false pcso bso opc1 -> match_iblock dupmap cfg false pcnot bnot opc2 -> is_join_opt opc1 opc2 opc -> - match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot i) opc + match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot i ni) opc . Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop := @@ -530,14 +535,14 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if negb isfst then OK None else Error (msg "BTL.verify_block: isfst is true Bgoto") - | Breturn or => + | Breturn or _ => match cfg!pc with | Some (Ireturn or') => if option_eq Pos.eq_dec or or' then OK None else Error (msg "BTL.verify_block: different opt reg in Breturn") | _ => Error (msg "BTL.verify_block: incorrect cfg Breturn") end - | Bcall s ri lr r pc1 => + | Bcall s ri lr r pc1 _ => match cfg!pc with | Some (Icall s' ri' lr' r' pc2) => do u <- verify_is_copy dupmap pc1 pc2; @@ -551,7 +556,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "BTL.verify_block: different signatures in Bcall") | _ => Error (msg "BTL.verify_block: incorrect cfg Bcall") end - | Btailcall s ri lr => + | Btailcall s ri lr _ => match cfg!pc with | Some (Itailcall s' ri' lr') => if (signature_eq s s') then @@ -562,7 +567,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "BTL.verify_block: different signatures in Btailcall") | _ => Error (msg "BTL.verify_block: incorrect cfg Btailcall") end - | Bbuiltin ef la br pc1 => + | Bbuiltin ef la br pc1 _ => match cfg!pc with | Some (Ibuiltin ef' la' br' pc2) => do u <- verify_is_copy dupmap pc1 pc2; @@ -574,7 +579,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "BTL.verify_block: different ef in Bbuiltin") | _ => Error (msg "BTL.verify_block: incorrect cfg Bbuiltin") end - | Bjumptable r ln => + | Bjumptable r ln _ => match cfg!pc with | Some (Ijumptable r' ln') => do u <- verify_is_copy_list dupmap ln ln'; @@ -583,12 +588,12 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) | _ => Error (msg "BTL.verify_block: incorrect cfg Bjumptable") end end - | Bnop => + | Bnop _ => match cfg!pc with | Some (Inop pc') => OK (Some pc') | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop") end - | Bop op lr r => + | Bop op lr r _ => match cfg!pc with | Some (Iop op' lr' r' pc') => if (eq_operation op op') then @@ -600,7 +605,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "BTL.verify_block: different operations in Bop") | _ => Error (msg "BTL.verify_block: incorrect cfg Bop") end - | Bload tm m a lr r => + | Bload tm m a lr r _ => match cfg!pc with | Some (Iload tm' m' a' lr' r' pc') => if (trapping_mode_eq tm TRAP && trapping_mode_eq tm' TRAP) then @@ -616,7 +621,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "BTL.verify_block: NOTRAP trapping_mode unsupported in Bload") | _ => Error (msg "BTL.verify_block: incorrect cfg Bload") end - | Bstore m a lr r => + | Bstore m a lr r _ => match cfg!pc with | Some (Istore m' a' lr' r' pc') => if (chunk_eq m m') then @@ -636,7 +641,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) verify_block dupmap cfg false pc' b2 | None => Error (msg "BTL.verify_block: None next pc in Bseq (deadcode)") end - | Bcond c lr bso bnot i => + | Bcond c lr bso bnot i _ => match cfg!pc with | Some (Icond c' lr' pcso pcnot i') => if (list_eq_dec Pos.eq_dec lr lr') then @@ -794,7 +799,7 @@ Definition is_goto (ib: iblock): bool := Definition is_atom (ib: iblock): bool := match ib with - | Bseq _ _ | Bcond _ _ _ _ _ => false + | Bseq _ _ | Bcond _ _ _ _ _ _ => false | _ => true end. @@ -804,10 +809,10 @@ Inductive is_expand: iblock -> Prop := is_atom ib1 = true -> is_expand ib2 -> is_expand (Bseq ib1 ib2) - | exp_Bcond cond args ib1 ib2 i: + | exp_Bcond cond args ib1 ib2 i ni: is_expand ib1 -> is_expand ib2 -> - is_expand (Bcond cond args ib1 ib2 i) + is_expand (Bcond cond args ib1 ib2 i ni) | exp_others ib: is_atom ib = true -> is_expand ib @@ -817,8 +822,8 @@ Local Hint Constructors is_expand: core. Fixpoint expand (ib: iblock) (k: option iblock): iblock := match ib with | Bseq ib1 ib2 => expand ib1 (Some (expand ib2 k)) - | Bcond cond args ib1 ib2 i => - Bcond cond args (expand ib1 k) (expand ib2 k) i + | Bcond cond args ib1 ib2 i ni => + Bcond cond args (expand ib1 k) (expand ib2 k) i ni | BF fin => fin | ib => match k with -- cgit From 2408dd1aecf8d8c3bfd3b24a65f7f57cf602cb10 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 20 May 2021 11:58:40 +0200 Subject: Changing to an opaq record in BTL info, this is a broken commit --- scheduling/BTL.v | 158 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 81 insertions(+), 77 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 44c25b75..ca727f82 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -23,29 +23,32 @@ Require Import RTL Op Registers OptionMonad. Definition exit := node. (* we may generalize this with register renamings at exit, like in "phi" nodes of SSA-form *) -(* node_info is a ghost record to provide and transfert information through oracles *) -Record node_info := { - _pos: node -}. +(* inst_info is a ghost record to provide instruction information through oracles *) +Parameter inst_info: Set. +Extract Constant inst_info => "BTLaux.inst_info". + +(* block_info is a ghost record to provide block information through oracles *) +Parameter block_info: Set. +Extract Constant block_info => "BTLaux.block_info". (** final instructions (that stops block execution) *) Inductive final: Type := | Bgoto (succ:exit) (** No operation -- just branch to [succ]. *) - | Breturn (res: option reg) (ni: node_info) + | Breturn (res: option reg) (** terminates the execution of the current function. It returns the value of the given register, or [Vundef] if none is given. *) - | Bcall (sig: signature) (fn: reg + ident) (args:list reg) (dest:reg) (succ:exit) (ni: node_info) + | Bcall (sig: signature) (fn: reg + ident) (args:list reg) (dest:reg) (succ:exit) (** invokes the function determined by [fn] (either a function pointer found in a register or a function name), giving it the values of registers [args] as arguments. It stores the return value in [dest] and branches to [succ]. *) - | Btailcall (sig:signature) (fn: reg + ident) (args: list reg) (ni: node_info) + | Btailcall (sig:signature) (fn: reg + ident) (args: list reg) (** performs a function invocation in tail-call position (the current function terminates after the call, returning the result of the callee) *) - | Bbuiltin (ef:external_function) (args:list (builtin_arg reg)) (dest:builtin_res reg) (succ:exit) (ni: node_info) + | Bbuiltin (ef:external_function) (args:list (builtin_arg reg)) (dest:builtin_res reg) (succ:exit) (** calls the built-in function identified by [ef], giving it the values of [args] as arguments. It stores the return value in [dest] and branches to [succ]. *) - | Bjumptable (arg:reg) (tbl:list exit) (ni: node_info) + | Bjumptable (arg:reg) (tbl:list exit) (** [Bjumptable arg tbl] transitions to the node that is the [n]-th element of the list [tbl], where [n] is the unsigned integer value of register [arg]. *) . @@ -53,16 +56,16 @@ Inductive final: Type := (* instruction block *) Inductive iblock: Type := (* final instructions that stops block execution *) - | BF (fi: final) + | BF (fi: final) (iinfo: inst_info) (* basic instructions that continues block execution, except when aborting *) - | Bnop (ni: node_info) (* nop instruction *) - | Bop (op:operation) (args:list reg) (dest:reg) (ni: node_info) + | Bnop (iinfo: inst_info) (* nop instruction *) + | Bop (op:operation) (args:list reg) (dest:reg) (iinfo: inst_info) (** performs the arithmetic operation [op] over the values of registers [args], stores the result in [dest] *) - | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg) (ni: node_info) + | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg) (iinfo: inst_info) (** loads a [chunk] quantity from the address determined by the addressing mode [addr] and the values of the [args] registers, stores the quantity just read into [dest]. If trap=NOTRAP, then failures lead to a default value written to [dest]. *) - | Bstore (chunk:memory_chunk) (addr:addressing) (args:list reg) (src:reg) (ni: node_info) + | Bstore (chunk:memory_chunk) (addr:addressing) (args:list reg) (src:reg) (iinfo: inst_info) (** stores the value of register [src] in the [chunk] quantity at the the address determined by the addressing mode [addr] and the values of the [args] registers. *) @@ -70,13 +73,13 @@ Inductive iblock: Type := | Bseq (b1 b2: iblock) (** starts by running [b1] and stops here if execution of [b1] has reached a final instruction or aborted or continue with [b2] otherwise *) - | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock) (info:option bool) (ni: node_info) + | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock) (iinfo: inst_info) (** evaluates the boolean condition [cond] over the values of registers [args]. If the condition is true, it continues on [ifso]. If the condition is false, it continues on [ifnot]. [info] is a ghost field there to provide information relative to branch prediction. *) . -Coercion BF: final >-> iblock. +Coercion BF: final >-> Funclass. (** NB: - a RTL [(Inop pc)] ending a branch of block is encoded by [(Bseq Bnop (Bgoto pc))]. @@ -88,7 +91,8 @@ Coercion BF: final >-> iblock. Record iblock_info := { entry: iblock; - input_regs: Regset.t (* extra liveness information ignored by BTL semantics *) + input_regs: Regset.t; (* extra liveness information ignored by BTL semantics *) + binfo: block_info (* Ghost field used in oracles *) }. Definition code: Type := PTree.t iblock_info. @@ -199,24 +203,24 @@ Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop := (** internal big-step execution of one iblock *) Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop := - | exec_final rs m fin: iblock_istep sp rs m (BF fin) rs m (Some fin) - | exec_nop rs m ni: iblock_istep sp rs m (Bnop ni) rs m None - | exec_op rs m op args res v ni + | exec_final rs m fin iinfo: iblock_istep sp rs m (BF fin iinfo) rs m (Some fin) + | exec_nop rs m iinfo: iblock_istep sp rs m (Bnop iinfo) rs m None + | exec_op rs m op args res v iinfo (EVAL: eval_operation ge sp op rs##args m = Some v) - : iblock_istep sp rs m (Bop op args res ni) (rs#res <- v) m None - | exec_load_TRAP rs m chunk addr args dst a v ni + : iblock_istep sp rs m (Bop op args res iinfo) (rs#res <- v) m None + | exec_load_TRAP rs m chunk addr args dst a v iinfo (EVAL: eval_addressing ge sp addr rs##args = Some a) (LOAD: Mem.loadv chunk m a = Some v) - : iblock_istep sp rs m (Bload TRAP chunk addr args dst ni) (rs#dst <- v) m None + : iblock_istep sp rs m (Bload TRAP chunk addr args dst iinfo) (rs#dst <- v) m None (* TODO: replace [exec_load_TRAP] above by this one. See "new scheme" for "NOTRAP" above | exec_load rs m trap chunk addr args dst v (LOAD: has_loaded sp rs m chunk addr args v trap) : iblock_istep sp rs m (Bload trap chunk addr args dst) (rs#dst <- v) m None *) - | exec_store rs m chunk addr args src a m' ni + | exec_store rs m chunk addr args src a m' iinfo (EVAL: eval_addressing ge sp addr rs##args = Some a) (STORE: Mem.storev chunk m a rs#src = Some m') - : iblock_istep sp rs m (Bstore chunk addr args src ni) rs m' None + : iblock_istep sp rs m (Bstore chunk addr args src iinfo) rs m' None | exec_seq_stop rs m b1 b2 rs' m' fin (EXEC: iblock_istep sp rs m b1 rs' m' (Some fin)) : iblock_istep sp rs m (Bseq b1 b2) rs' m' (Some fin) @@ -224,10 +228,10 @@ Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option fi (EXEC1: iblock_istep sp rs m b1 rs1 m1 None) (EXEC2: iblock_istep sp rs1 m1 b2 rs' m' ofin) : iblock_istep sp rs m (Bseq b1 b2) rs' m' ofin - | exec_cond rs m cond args ifso ifnot i b rs' m' ofin ni + | exec_cond rs m cond args ifso ifnot b rs' m' ofin iinfo (EVAL: eval_condition cond rs##args m = Some b) (EXEC: iblock_istep sp rs m (if b then ifso else ifnot) rs' m' ofin) - : iblock_istep sp rs m (Bcond cond args ifso ifnot i ni) rs' m' ofin + : iblock_istep sp rs m (Bcond cond args ifso ifnot iinfo) rs' m' ofin . Local Hint Constructors iblock_istep: core. @@ -236,7 +240,7 @@ Lemma [iblock_istep_run_equiv] below provides a proof that "relation" [iblock_is *) Fixpoint iblock_istep_run sp ib rs m: option outcome := match ib with - | BF fin => + | BF fin _ => Some {| _rs := rs; _m := m; _fin := Some fin |} (* basic instructions *) | Bnop _ => @@ -261,7 +265,7 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome := | None => iblock_istep_run sp b2 out1.(_rs) out1.(_m) | _ => Some out1 (* stop execution on the 1st final instruction *) end - | Bcond cond args ifso ifnot _ _ => + | Bcond cond args ifso ifnot _ => SOME b <- eval_condition cond rs##args m IN iblock_istep_run sp (if b then ifso else ifnot) rs m end. @@ -280,32 +284,32 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := | exec_Bgoto pc: final_step stack f sp rs m (Bgoto pc) E0 (State stack f sp pc rs m) - | exec_Breturn or stk m' ni: + | exec_Breturn or stk m': sp = (Vptr stk Ptrofs.zero) -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - final_step stack f sp rs m (Breturn or ni) + final_step stack f sp rs m (Breturn or) E0 (Returnstate stack (regmap_optget or Vundef rs) m') - | exec_Bcall sig ros args res pc' fd ni: + | exec_Bcall sig ros args res pc' fd: find_function ros rs = Some fd -> funsig fd = sig -> - final_step stack f sp rs m (Bcall sig ros args res pc' ni) + final_step stack f sp rs m (Bcall sig ros args res pc') E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m) - | exec_Btailcall sig ros args stk m' fd ni: + | exec_Btailcall sig ros args stk m' fd: find_function ros rs = Some fd -> funsig fd = sig -> sp = (Vptr stk Ptrofs.zero) -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - final_step stack f sp rs m (Btailcall sig ros args ni) + final_step stack f sp rs m (Btailcall sig ros args) E0 (Callstate stack fd rs##args m') - | exec_Bbuiltin ef args res pc' vargs t vres m' ni: + | exec_Bbuiltin ef args res pc' vargs t vres m': eval_builtin_args ge (fun r => rs#r) sp m args vargs -> external_call ef ge vargs m t vres m' -> - final_step stack f sp rs m (Bbuiltin ef args res pc' ni) + final_step stack f sp rs m (Bbuiltin ef args res pc') t (State stack f sp pc' (regmap_setres res vres rs) m') - | exec_Bjumptable arg tbl n pc' ni: + | exec_Bjumptable arg tbl n pc': rs#arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some pc' -> - final_step stack f sp rs m (Bjumptable arg tbl ni) + final_step stack f sp rs m (Bjumptable arg tbl) E0 (State stack f sp pc' rs m) . @@ -393,16 +397,16 @@ Inductive match_final_inst (dupmap: PTree.t node): final -> instruction -> Prop | mfi_goto pc pc': dupmap!pc = (Some pc') -> match_final_inst dupmap (Bgoto pc) (Inop pc') *) - | mfi_return or ni: match_final_inst dupmap (Breturn or ni) (Ireturn or) - | mfi_call pc pc' s ri lr r ni: - dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc ni) (Icall s ri lr r pc') - | mfi_tailcall s ri lr ni: - match_final_inst dupmap (Btailcall s ri lr ni) (Itailcall s ri lr) - | mfi_builtin pc pc' ef la br ni: - dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc ni) (Ibuiltin ef la br pc') - | mfi_jumptable ln ln' r ni: + | mfi_return or: match_final_inst dupmap (Breturn or) (Ireturn or) + | mfi_call pc pc' s ri lr r: + dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc) (Icall s ri lr r pc') + | mfi_tailcall s ri lr: + match_final_inst dupmap (Btailcall s ri lr) (Itailcall s ri lr) + | mfi_builtin pc pc' ef la br: + dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc) (Ibuiltin ef la br pc') + | mfi_jumptable ln ln' r: list_forall2 (fun pc pc' => (dupmap!pc = (Some pc'))) ln ln' -> - match_final_inst dupmap (Bjumptable r ln ni) (Ijumptable r ln') + match_final_inst dupmap (Bjumptable r ln) (Ijumptable r ln') . Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop := @@ -417,25 +421,25 @@ Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop := - if [opc] is [Some pc'], this means that all branches of the block that do not exit, join on [pc']. *) Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> iblock -> (option node) -> Prop := - | mib_BF isfst fi pc i: + | mib_BF isfst fi pc i iinfo: cfg!pc = Some i -> match_final_inst dupmap fi i -> - match_iblock dupmap cfg isfst pc (BF fi) None - | mib_nop isfst pc pc' ni: + match_iblock dupmap cfg isfst pc (BF fi iinfo) None + | mib_nop isfst pc pc' iinfo: cfg!pc = Some (Inop pc') -> - match_iblock dupmap cfg isfst pc (Bnop ni) (Some pc') - | mib_op isfst pc pc' op lr r ni: + match_iblock dupmap cfg isfst pc (Bnop iinfo) (Some pc') + | mib_op isfst pc pc' op lr r iinfo: cfg!pc = Some (Iop op lr r pc') -> - match_iblock dupmap cfg isfst pc (Bop op lr r ni) (Some pc') - | mib_load isfst pc pc' m a lr r ni: + match_iblock dupmap cfg isfst pc (Bop op lr r iinfo) (Some pc') + | mib_load isfst pc pc' m a lr r iinfo: cfg!pc = Some (Iload TRAP m a lr r pc') -> - match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r ni) (Some pc') - | mib_store isfst pc pc' m a lr r ni: + match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r iinfo) (Some pc') + | mib_store isfst pc pc' m a lr r iinfo: cfg!pc = Some (Istore m a lr r pc') -> - match_iblock dupmap cfg isfst pc (Bstore m a lr r ni) (Some pc') - | mib_exit pc pc': + match_iblock dupmap cfg isfst pc (Bstore m a lr r iinfo) (Some pc') + | mib_exit pc pc' iinfo: dupmap!pc = (Some pc') -> - match_iblock dupmap cfg false pc' (Bgoto pc) None + match_iblock dupmap cfg false pc' (BF (Bgoto pc) iinfo) None (* NB: on RTL side, we exit the block by a "basic" instruction (or Icond). Thus some step should have been executed before [pc'] in the RTL code *) | mib_seq_Some isfst b1 b2 pc1 pc2 opc: @@ -450,12 +454,12 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i And the verifier could fail if there is such dead code! *) *) - | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i i' ni: - cfg!pc = Some (Icond c lr pcso pcnot i') -> + | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i iinfo: + cfg!pc = Some (Icond c lr pcso pcnot i) -> match_iblock dupmap cfg false pcso bso opc1 -> match_iblock dupmap cfg false pcnot bnot opc2 -> is_join_opt opc1 opc2 opc -> - match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot i ni) opc + match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot iinfo) opc . Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop := @@ -528,21 +532,21 @@ Global Opaque builtin_res_eq_pos. Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) := match ib with - | BF fi => + | BF fi _ => match fi with | Bgoto pc1 => do u <- verify_is_copy dupmap pc1 pc; if negb isfst then OK None else Error (msg "BTL.verify_block: isfst is true Bgoto") - | Breturn or _ => + | Breturn or => match cfg!pc with | Some (Ireturn or') => if option_eq Pos.eq_dec or or' then OK None else Error (msg "BTL.verify_block: different opt reg in Breturn") | _ => Error (msg "BTL.verify_block: incorrect cfg Breturn") end - | Bcall s ri lr r pc1 _ => + | Bcall s ri lr r pc1 => match cfg!pc with | Some (Icall s' ri' lr' r' pc2) => do u <- verify_is_copy dupmap pc1 pc2; @@ -556,7 +560,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "BTL.verify_block: different signatures in Bcall") | _ => Error (msg "BTL.verify_block: incorrect cfg Bcall") end - | Btailcall s ri lr _ => + | Btailcall s ri lr => match cfg!pc with | Some (Itailcall s' ri' lr') => if (signature_eq s s') then @@ -567,7 +571,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "BTL.verify_block: different signatures in Btailcall") | _ => Error (msg "BTL.verify_block: incorrect cfg Btailcall") end - | Bbuiltin ef la br pc1 _ => + | Bbuiltin ef la br pc1 => match cfg!pc with | Some (Ibuiltin ef' la' br' pc2) => do u <- verify_is_copy dupmap pc1 pc2; @@ -579,7 +583,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "BTL.verify_block: different ef in Bbuiltin") | _ => Error (msg "BTL.verify_block: incorrect cfg Bbuiltin") end - | Bjumptable r ln _ => + | Bjumptable r ln => match cfg!pc with | Some (Ijumptable r' ln') => do u <- verify_is_copy_list dupmap ln ln'; @@ -641,7 +645,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) verify_block dupmap cfg false pc' b2 | None => Error (msg "BTL.verify_block: None next pc in Bseq (deadcode)") end - | Bcond c lr bso bnot i _ => + | Bcond c lr bso bnot _ => match cfg!pc with | Some (Icond c' lr' pcso pcnot i') => if (list_eq_dec Pos.eq_dec lr lr') then @@ -793,13 +797,13 @@ Definition verify_function dupmap f f' : res unit := Definition is_goto (ib: iblock): bool := match ib with - | Bgoto _ => true + | BF (Bgoto _) _ => true | _ => false end. Definition is_atom (ib: iblock): bool := match ib with - | Bseq _ _ | Bcond _ _ _ _ _ _ => false + | Bseq _ _ | Bcond _ _ _ _ _ => false | _ => true end. @@ -809,10 +813,10 @@ Inductive is_expand: iblock -> Prop := is_atom ib1 = true -> is_expand ib2 -> is_expand (Bseq ib1 ib2) - | exp_Bcond cond args ib1 ib2 i ni: + | exp_Bcond cond args ib1 ib2 iinfo: is_expand ib1 -> is_expand ib2 -> - is_expand (Bcond cond args ib1 ib2 i ni) + is_expand (Bcond cond args ib1 ib2 iinfo) | exp_others ib: is_atom ib = true -> is_expand ib @@ -822,9 +826,9 @@ Local Hint Constructors is_expand: core. Fixpoint expand (ib: iblock) (k: option iblock): iblock := match ib with | Bseq ib1 ib2 => expand ib1 (Some (expand ib2 k)) - | Bcond cond args ib1 ib2 i ni => - Bcond cond args (expand ib1 k) (expand ib2 k) i ni - | BF fin => fin + | Bcond cond args ib1 ib2 iinfo => + Bcond cond args (expand ib1 k) (expand ib2 k) iinfo + | BF fin iinfo => BF fin iinfo | ib => match k with | None => ib -- cgit From d858606e8400e6aab627f4aac5ec33ce9c2c80fe Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 20 May 2021 18:34:46 +0200 Subject: defines fsem (aka functional semantics) of BTL --- scheduling/BTL.v | 81 +++++++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 74 insertions(+), 7 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 10a000a8..cb60fed1 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -83,7 +83,7 @@ Coercion BF: final >-> iblock. Record iblock_info := { entry: iblock; - input_regs: Regset.t (* extra liveness information ignored by BTL semantics *) + input_regs: Regset.t (* extra liveness information for BTL functional semantics *) }. Definition code: Type := PTree.t iblock_info. @@ -161,6 +161,9 @@ Record outcome := out { Section RELSEM. +(* final_step is parametrized by a function to transfer regset on each exit *) +Variable tr_exit: function -> exit -> regset -> regset. + Variable ge: genv. Definition find_function (ros: reg + ident) (rs: regset) : option fundef := @@ -274,7 +277,7 @@ Qed. Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := | exec_Bgoto pc: final_step stack f sp rs m (Bgoto pc) E0 - (State stack f sp pc rs m) + (State stack f sp pc (tr_exit f pc rs) m) | exec_Breturn or stk m': sp = (Vptr stk Ptrofs.zero) -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> @@ -284,7 +287,7 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := find_function ros rs = Some fd -> funsig fd = sig -> final_step stack f sp rs m (Bcall sig ros args res pc') - E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m) + E0 (Callstate (Stackframe res f sp pc' (tr_exit f pc' rs) :: stack) fd rs##args m) | exec_Btailcall sig ros args stk m' fd: find_function ros rs = Some fd -> funsig fd = sig -> @@ -296,12 +299,12 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := eval_builtin_args ge (fun r => rs#r) sp m args vargs -> external_call ef ge vargs m t vres m' -> final_step stack f sp rs m (Bbuiltin ef args res pc') - t (State stack f sp pc' (regmap_setres res vres rs) m') + t (State stack f sp pc' (tr_exit f pc' (regmap_setres res vres rs)) m') | exec_Bjumptable arg tbl n pc': rs#arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some pc' -> final_step stack f sp rs m (Bjumptable arg tbl) - E0 (State stack f sp pc' rs m) + E0 (State stack f sp pc' (tr_exit f pc' rs) m) . (** big-step execution of one iblock *) @@ -358,11 +361,75 @@ Inductive final_state: state -> int -> Prop := | final_state_intro: forall r m, final_state (Returnstate nil (Vint r) m) r. -(** The small-step semantics for a program. *) +(** The basic small-step semantics for a BTL program. *) + +(* tid = transfer_identity *) +Definition tid (_:function) (_:exit) (rs:regset) := rs. Definition semantics (p: program) := - Semantics step (initial_state p) final_state (Genv.globalenv p). + Semantics (step tid) (initial_state p) final_state (Genv.globalenv p). + +(** The "functional" small-step semantics for a BTL program. + at each exit, we only transfer register in "input_regs" (i.e. "alive" registers). +*) + +Definition transfer_regs (inputs: list reg) (rs: regset): regset := + init_regs (rs##inputs) inputs. + +Lemma transfer_regs_inputs inputs rs r: + List.In r inputs -> (transfer_regs inputs rs)#r = rs#r. +Proof. + unfold transfer_regs; induction inputs; simpl; intuition subst. + - rewrite Regmap.gss; auto. + - destruct (Pos.eq_dec a r). + + subst; rewrite Regmap.gss; auto. + + rewrite Regmap.gso; auto. +Qed. + +Lemma transfer_regs_dead inputs rs r: + ~List.In r inputs -> (transfer_regs inputs rs)#r = Vundef. +Proof. + unfold transfer_regs; induction inputs; simpl; intuition subst. + - rewrite Regmap.gi; auto. + - rewrite Regmap.gso; auto. +Qed. + +Definition inputs_exit (f:function) (pc: exit) : Regset.t := + match f.(fn_code)!pc with + | None => Regset.empty + | Some ib => ib.(input_regs) + end. + +Definition tr_inputs (f:function) (pc: exit): regset -> regset + := transfer_regs (Regset.elements (inputs_exit f pc)). + +(* TODO: move this elsewhere *) +Lemma SetoidList_InA_eq_equiv A (l: list A): forall x, + SetoidList.InA (fun x y => x = y) x l <-> List.In x l. +Proof. + intros x; split. + - induction 1; simpl; eauto. + - induction l; simpl; intuition. +Qed. + +Lemma tr_inputs_exit f pc rs r: + Regset.In r (inputs_exit f pc) -> (tr_inputs f pc rs)#r = rs#r. +Proof. + intros; eapply transfer_regs_inputs. + rewrite <- SetoidList_InA_eq_equiv. + eapply Regset.elements_1; eauto. +Qed. + +Lemma tr_inputs_dead f pc rs r: + ~(Regset.In r (inputs_exit f pc)) -> (tr_inputs f pc rs)#r = Vundef. +Proof. + intros X; eapply transfer_regs_dead; intuition eauto. + eapply X. eapply Regset.elements_2. + rewrite -> SetoidList_InA_eq_equiv; eauto. +Qed. +Definition fsem (p: program) := + Semantics (step tr_inputs) (initial_state p) final_state (Genv.globalenv p). (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) -- cgit From 25a4620c95aaa6b017443da29fcf3d033a44a86f Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 21 May 2021 15:59:31 +0200 Subject: improve fsem --- scheduling/BTL.v | 45 ++++++++++++++++++++++++++++++--------------- 1 file changed, 30 insertions(+), 15 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index cb60fed1..fb6d5cea 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -161,8 +161,16 @@ Record outcome := out { Section RELSEM. -(* final_step is parametrized by a function to transfer regset on each exit *) -Variable tr_exit: function -> exit -> regset -> regset. +(** [step] (and in particular [final_step]) is parametrized by function [tr_exit] to transfer registers on each iblock exit. + + In particular, [tr_exit f pc or rs] computes from [rs] the [rs'] on which the execution from iblock [pc] in [f] will start. + + Here, [or] is an optional register that will be assigned after exiting the iblock, but before entering in [pc]: e.g. the register set by a function call + before entering in return address. + +*) + +Variable tr_exit: function -> exit -> option reg -> regset -> regset. Variable ge: genv. @@ -277,7 +285,7 @@ Qed. Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := | exec_Bgoto pc: final_step stack f sp rs m (Bgoto pc) E0 - (State stack f sp pc (tr_exit f pc rs) m) + (State stack f sp pc (tr_exit f pc None rs) m) | exec_Breturn or stk m': sp = (Vptr stk Ptrofs.zero) -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> @@ -287,7 +295,7 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := find_function ros rs = Some fd -> funsig fd = sig -> final_step stack f sp rs m (Bcall sig ros args res pc') - E0 (Callstate (Stackframe res f sp pc' (tr_exit f pc' rs) :: stack) fd rs##args m) + E0 (Callstate (Stackframe res f sp pc' (tr_exit f pc' (Some res) rs) :: stack) fd rs##args m) | exec_Btailcall sig ros args stk m' fd: find_function ros rs = Some fd -> funsig fd = sig -> @@ -299,12 +307,15 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := eval_builtin_args ge (fun r => rs#r) sp m args vargs -> external_call ef ge vargs m t vres m' -> final_step stack f sp rs m (Bbuiltin ef args res pc') - t (State stack f sp pc' (tr_exit f pc' (regmap_setres res vres rs)) m') + (* TODO: not clear that this is the better choice ! + we coud also do something like [regmap_setres res vres (tr_exit f pc' (reg_builtin_res res) rs)] + *) + t (State stack f sp pc' (tr_exit f pc' None (regmap_setres res vres rs)) m') | exec_Bjumptable arg tbl n pc': rs#arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some pc' -> final_step stack f sp rs m (Bjumptable arg tbl) - E0 (State stack f sp pc' (tr_exit f pc' rs) m) + E0 (State stack f sp pc' (tr_exit f pc' None rs) m) . (** big-step execution of one iblock *) @@ -364,7 +375,7 @@ Inductive final_state: state -> int -> Prop := (** The basic small-step semantics for a BTL program. *) (* tid = transfer_identity *) -Definition tid (_:function) (_:exit) (rs:regset) := rs. +Definition tid (_:function) (_:exit) (_: option reg) (rs:regset) := rs. Definition semantics (p: program) := Semantics (step tid) (initial_state p) final_state (Genv.globalenv p). @@ -394,14 +405,18 @@ Proof. - rewrite Regmap.gso; auto. Qed. -Definition inputs_exit (f:function) (pc: exit) : Regset.t := +Definition inputs_exit (f:function) (pc: exit) (or:option reg): Regset.t := match f.(fn_code)!pc with | None => Regset.empty - | Some ib => ib.(input_regs) + | Some ib => + match or with + | Some r => Regset.remove r ib.(input_regs) + | None => ib.(input_regs) + end end. -Definition tr_inputs (f:function) (pc: exit): regset -> regset - := transfer_regs (Regset.elements (inputs_exit f pc)). +Definition tr_inputs (f:function) (pc: exit) (or:option reg): regset -> regset + := transfer_regs (Regset.elements (inputs_exit f pc or)). (* TODO: move this elsewhere *) Lemma SetoidList_InA_eq_equiv A (l: list A): forall x, @@ -412,16 +427,16 @@ Proof. - induction l; simpl; intuition. Qed. -Lemma tr_inputs_exit f pc rs r: - Regset.In r (inputs_exit f pc) -> (tr_inputs f pc rs)#r = rs#r. +Lemma tr_inputs_exit f pc or rs r: + Regset.In r (inputs_exit f pc or) -> (tr_inputs f pc or rs)#r = rs#r. Proof. intros; eapply transfer_regs_inputs. rewrite <- SetoidList_InA_eq_equiv. eapply Regset.elements_1; eauto. Qed. -Lemma tr_inputs_dead f pc rs r: - ~(Regset.In r (inputs_exit f pc)) -> (tr_inputs f pc rs)#r = Vundef. +Lemma tr_inputs_dead f pc or rs r: + ~(Regset.In r (inputs_exit f pc or)) -> (tr_inputs f pc or rs)#r = Vundef. Proof. intros X; eapply transfer_regs_dead; intuition eauto. eapply X. eapply Regset.elements_2. -- cgit From 3e6844222d39b8a76bf0af20b9cbb0dfa2e35b5a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 21 May 2021 21:18:59 +0200 Subject: Now supporting Bnop insertion in conditions --- scheduling/BTL.v | 66 +++++++++++++++++++++++++++++++++++++------------------- 1 file changed, 44 insertions(+), 22 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index ca727f82..05391c58 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -58,7 +58,7 @@ Inductive iblock: Type := (* final instructions that stops block execution *) | BF (fi: final) (iinfo: inst_info) (* basic instructions that continues block execution, except when aborting *) - | Bnop (iinfo: inst_info) (* nop instruction *) + | Bnop (oiinfo: option inst_info) (* nop instruction *) | Bop (op:operation) (args:list reg) (dest:reg) (iinfo: inst_info) (** performs the arithmetic operation [op] over the values of registers [args], stores the result in [dest] *) | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg) (iinfo: inst_info) @@ -204,7 +204,7 @@ Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop := (** internal big-step execution of one iblock *) Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop := | exec_final rs m fin iinfo: iblock_istep sp rs m (BF fin iinfo) rs m (Some fin) - | exec_nop rs m iinfo: iblock_istep sp rs m (Bnop iinfo) rs m None +| exec_nop rs m oiinfo: iblock_istep sp rs m (Bnop oiinfo) rs m None | exec_op rs m op args res v iinfo (EVAL: eval_operation ge sp op rs##args m = Some v) : iblock_istep sp rs m (Bop op args res iinfo) (rs#res <- v) m None @@ -425,9 +425,11 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i cfg!pc = Some i -> match_final_inst dupmap fi i -> match_iblock dupmap cfg isfst pc (BF fi iinfo) None - | mib_nop isfst pc pc' iinfo: + | mib_nop_on_rtl isfst pc pc' iinfo: cfg!pc = Some (Inop pc') -> - match_iblock dupmap cfg isfst pc (Bnop iinfo) (Some pc') + match_iblock dupmap cfg isfst pc (Bnop (Some iinfo)) (Some pc') + | mib_nop_skip pc: + match_iblock dupmap cfg false pc (Bnop None) (Some pc) | mib_op isfst pc pc' op lr r iinfo: cfg!pc = Some (Iop op lr r pc') -> match_iblock dupmap cfg isfst pc (Bop op lr r iinfo) (Some pc') @@ -592,10 +594,16 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) | _ => Error (msg "BTL.verify_block: incorrect cfg Bjumptable") end end - | Bnop _ => - match cfg!pc with - | Some (Inop pc') => OK (Some pc') - | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop") + | Bnop oiinfo => + match oiinfo with + | Some _ => + match cfg!pc with + | Some (Inop pc') => OK (Some pc') + | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop") + end + | None => + if negb isfst then OK (Some pc) + else Error (msg "BTL.verify_block: isfst is true Bnop (on_rtl is false)") end | Bop op lr r _ => match cfg!pc with @@ -712,8 +720,11 @@ Proof. destruct (Pos.eq_dec _ _); try discriminate. subst. inv EQ0. eapply mib_BF; eauto. constructor; assumption. - (* Bnop *) - destruct i; inv H. - constructor; assumption. + destruct oiinfo; simpl in *. + + destruct (cfg!pc) eqn:EQCFG; try discriminate. + destruct i0; inv H. constructor; assumption. + + destruct isfst; try discriminate. inv H. + constructor; assumption. - (* Bop *) destruct i; try discriminate. destruct (eq_operation _ _); try discriminate. @@ -803,10 +814,16 @@ Definition is_goto (ib: iblock): bool := Definition is_atom (ib: iblock): bool := match ib with - | Bseq _ _ | Bcond _ _ _ _ _ => false + | Bseq _ _ | Bcond _ _ _ _ _ | Bnop None => false | _ => true end. +Definition Bnop_dec k: { k=Bnop None} + { k<>(Bnop None) }. +Proof. + destruct k; simpl; try destruct oiinfo; + intuition congruence. +Defined. + (** Is expand property to only support atomic instructions on the left part of a Bseq *) Inductive is_expand: iblock -> Prop := | exp_Bseq ib1 ib2: @@ -814,8 +831,8 @@ Inductive is_expand: iblock -> Prop := is_expand ib2 -> is_expand (Bseq ib1 ib2) | exp_Bcond cond args ib1 ib2 iinfo: - is_expand ib1 -> - is_expand ib2 -> + is_expand ib1 \/ ib1 = Bnop None -> + is_expand ib2 \/ ib2 = Bnop None -> is_expand (Bcond cond args ib1 ib2 iinfo) | exp_others ib: is_atom ib = true -> @@ -823,22 +840,27 @@ Inductive is_expand: iblock -> Prop := . Local Hint Constructors is_expand: core. -Fixpoint expand (ib: iblock) (k: option iblock): iblock := +Fixpoint expand (ib: iblock) (k: iblock): iblock := match ib with - | Bseq ib1 ib2 => expand ib1 (Some (expand ib2 k)) + | Bseq ib1 ib2 => expand ib1 (expand ib2 k) | Bcond cond args ib1 ib2 iinfo => Bcond cond args (expand ib1 k) (expand ib2 k) iinfo | BF fin iinfo => BF fin iinfo - | ib => - match k with - | None => ib - | Some rem => Bseq ib rem - end + | Bnop None => k + | ib => + if Bnop_dec k then ib else Bseq ib k end. Lemma expand_correct ib: forall k, - (match k with Some rem => is_expand rem | None => True end) + (k <> (Bnop None) -> is_expand k) + -> (expand ib k) <> (Bnop None) -> is_expand (expand ib k). Proof. - induction ib; simpl; intros; try autodestruct; auto. + induction ib; simpl; intros; auto. + 1-4: + try destruct oiinfo; + destruct (Bnop_dec k); auto. + constructor. + - destruct (Bnop_dec (expand ib1 k)); auto. + - destruct (Bnop_dec (expand ib2 k)); auto. Qed. -- cgit From 30e41117b57ab20beb1876e38c26dbddc5a58dfb Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sun, 23 May 2021 20:37:22 +0200 Subject: splitting is_expand property with a weak version for conditions --- scheduling/BTL.v | 81 +++++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 59 insertions(+), 22 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 05391c58..0f9ef44f 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -812,7 +812,7 @@ Definition is_goto (ib: iblock): bool := | _ => false end. -Definition is_atom (ib: iblock): bool := +Definition is_RTLatom (ib: iblock): bool := match ib with | Bseq _ _ | Bcond _ _ _ _ _ | Bnop None => false | _ => true @@ -824,43 +824,80 @@ Proof. intuition congruence. Defined. -(** Is expand property to only support atomic instructions on the left part of a Bseq *) +(** Is expand property to only support atomic instructions on the left part of a Bseq: + The tree is right-expanded, and block are normalized to simplify RTL simulation *) Inductive is_expand: iblock -> Prop := | exp_Bseq ib1 ib2: - is_atom ib1 = true -> + is_RTLatom ib1 = true -> is_expand ib2 -> is_expand (Bseq ib1 ib2) - | exp_Bcond cond args ib1 ib2 iinfo: - is_expand ib1 \/ ib1 = Bnop None -> - is_expand ib2 \/ ib2 = Bnop None -> - is_expand (Bcond cond args ib1 ib2 iinfo) + | exp_Bcond cond args ib1 ib2 i: + is_expand ib1 -> + is_expand ib2 -> + is_expand (Bcond cond args ib1 ib2 i) | exp_others ib: - is_atom ib = true -> + is_RTLatom ib = true -> is_expand ib . Local Hint Constructors is_expand: core. -Fixpoint expand (ib: iblock) (k: iblock): iblock := +(** The weak version with more specific hypothesis for conditions *) +Inductive is_wexpand: iblock -> Prop := + | wexp_Bseq ib1 ib2: + is_RTLatom ib1 = true -> + is_wexpand ib2 -> + is_wexpand (Bseq ib1 ib2) + | wexp_Bcond cond args ib1 ib2 iinfo: + (ib1 <> Bnop None -> is_wexpand ib1) -> + (ib2 <> Bnop None -> is_wexpand ib2) -> + is_wexpand (Bcond cond args ib1 ib2 iinfo) + | wexp_others ib: + is_RTLatom ib = true -> + is_wexpand ib + . +Local Hint Constructors is_wexpand: core. + +Fixpoint normRTL (ib: iblock) (k: iblock): iblock := match ib with - | Bseq ib1 ib2 => expand ib1 (expand ib2 k) + | Bseq ib1 ib2 => normRTL ib1 (normRTL ib2 k) | Bcond cond args ib1 ib2 iinfo => - Bcond cond args (expand ib1 k) (expand ib2 k) iinfo + Bcond cond args (normRTL ib1 k) (normRTL ib2 k) iinfo | BF fin iinfo => BF fin iinfo | Bnop None => k | ib => if Bnop_dec k then ib else Bseq ib k end. -Lemma expand_correct ib: forall k, - (k <> (Bnop None) -> is_expand k) - -> (expand ib k) <> (Bnop None) - -> is_expand (expand ib k). +Lemma normRTL_correct ib: forall k, + (k <> (Bnop None) -> is_wexpand k) -> + (normRTL ib k) <> Bnop None -> + is_wexpand (normRTL ib k). Proof. - induction ib; simpl; intros; auto. - 1-4: - try destruct oiinfo; - destruct (Bnop_dec k); auto. - constructor. - - destruct (Bnop_dec (expand ib1 k)); auto. - - destruct (Bnop_dec (expand ib2 k)); auto. + induction ib; simpl; intros; try autodestruct; auto. + intros; destruct (Bnop_dec k); auto. +Qed. + +Lemma is_join_opt_None {A} (opc1 opc2: option A): + is_join_opt opc1 opc2 None -> opc1 = None /\ opc2 = None. +Proof. + intros X. inv X; auto. +Qed. + +Lemma match_iblock_None_not_Bnop dupmap cfg isfst pc ib: + match_iblock dupmap cfg isfst pc ib None -> ib <> Bnop None. +Proof. + intros X; inv X; try congruence. +Qed. +Local Hint Resolve match_iblock_None_not_Bnop: core. + +Lemma is_wexpand_expand dupmap cfg ib: + is_wexpand ib -> + forall isfst pc + (MIB: match_iblock dupmap cfg isfst pc ib None), + is_expand ib. +Proof. + induction 1; simpl; intros; auto; try (inv MIB); eauto. + (* Bcond *) + destruct (is_join_opt_None opc1 opc2); subst; eauto. + econstructor; eauto. Qed. -- cgit From 51ec982b84851ac3526a0cb3f22e41f974b2d592 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 24 May 2021 22:41:35 +0200 Subject: tiny simplifications in RTLtoBTLproof --- scheduling/BTL.v | 92 +------------------------------------------------------- 1 file changed, 1 insertion(+), 91 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 0f9ef44f..97c54021 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -810,94 +810,4 @@ Definition is_goto (ib: iblock): bool := match ib with | BF (Bgoto _) _ => true | _ => false - end. - -Definition is_RTLatom (ib: iblock): bool := - match ib with - | Bseq _ _ | Bcond _ _ _ _ _ | Bnop None => false - | _ => true - end. - -Definition Bnop_dec k: { k=Bnop None} + { k<>(Bnop None) }. -Proof. - destruct k; simpl; try destruct oiinfo; - intuition congruence. -Defined. - -(** Is expand property to only support atomic instructions on the left part of a Bseq: - The tree is right-expanded, and block are normalized to simplify RTL simulation *) -Inductive is_expand: iblock -> Prop := - | exp_Bseq ib1 ib2: - is_RTLatom ib1 = true -> - is_expand ib2 -> - is_expand (Bseq ib1 ib2) - | exp_Bcond cond args ib1 ib2 i: - is_expand ib1 -> - is_expand ib2 -> - is_expand (Bcond cond args ib1 ib2 i) - | exp_others ib: - is_RTLatom ib = true -> - is_expand ib - . -Local Hint Constructors is_expand: core. - -(** The weak version with more specific hypothesis for conditions *) -Inductive is_wexpand: iblock -> Prop := - | wexp_Bseq ib1 ib2: - is_RTLatom ib1 = true -> - is_wexpand ib2 -> - is_wexpand (Bseq ib1 ib2) - | wexp_Bcond cond args ib1 ib2 iinfo: - (ib1 <> Bnop None -> is_wexpand ib1) -> - (ib2 <> Bnop None -> is_wexpand ib2) -> - is_wexpand (Bcond cond args ib1 ib2 iinfo) - | wexp_others ib: - is_RTLatom ib = true -> - is_wexpand ib - . -Local Hint Constructors is_wexpand: core. - -Fixpoint normRTL (ib: iblock) (k: iblock): iblock := - match ib with - | Bseq ib1 ib2 => normRTL ib1 (normRTL ib2 k) - | Bcond cond args ib1 ib2 iinfo => - Bcond cond args (normRTL ib1 k) (normRTL ib2 k) iinfo - | BF fin iinfo => BF fin iinfo - | Bnop None => k - | ib => - if Bnop_dec k then ib else Bseq ib k - end. - -Lemma normRTL_correct ib: forall k, - (k <> (Bnop None) -> is_wexpand k) -> - (normRTL ib k) <> Bnop None -> - is_wexpand (normRTL ib k). -Proof. - induction ib; simpl; intros; try autodestruct; auto. - intros; destruct (Bnop_dec k); auto. -Qed. - -Lemma is_join_opt_None {A} (opc1 opc2: option A): - is_join_opt opc1 opc2 None -> opc1 = None /\ opc2 = None. -Proof. - intros X. inv X; auto. -Qed. - -Lemma match_iblock_None_not_Bnop dupmap cfg isfst pc ib: - match_iblock dupmap cfg isfst pc ib None -> ib <> Bnop None. -Proof. - intros X; inv X; try congruence. -Qed. -Local Hint Resolve match_iblock_None_not_Bnop: core. - -Lemma is_wexpand_expand dupmap cfg ib: - is_wexpand ib -> - forall isfst pc - (MIB: match_iblock dupmap cfg isfst pc ib None), - is_expand ib. -Proof. - induction 1; simpl; intros; auto; try (inv MIB); eauto. - (* Bcond *) - destruct (is_join_opt_None opc1 opc2); subst; eauto. - econstructor; eauto. -Qed. + end. \ No newline at end of file -- cgit From 6938945d80bf16a6de4986e2815113e938bff6c3 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 25 May 2021 13:36:57 +0200 Subject: starting to experiment SE of fsem --- scheduling/BTL.v | 91 +++++++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 74 insertions(+), 17 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index fb6d5cea..4ae7a6dd 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -159,18 +159,22 @@ Record outcome := out { _fin: option final }. + + + Section RELSEM. + (** [step] (and in particular [final_step]) is parametrized by function [tr_exit] to transfer registers on each iblock exit. - In particular, [tr_exit f pc or rs] computes from [rs] the [rs'] on which the execution from iblock [pc] in [f] will start. + In particular, [tr_exit f lpc or rs] computes from [rs] the [rs'] on which the execution from iblock [pc] in [lpc] in [f] may start. Here, [or] is an optional register that will be assigned after exiting the iblock, but before entering in [pc]: e.g. the register set by a function call before entering in return address. *) -Variable tr_exit: function -> exit -> option reg -> regset -> regset. +Variable tr_exit: function -> list exit -> option reg -> regset -> regset. Variable ge: genv. @@ -282,10 +286,13 @@ Proof. destruct o; try_simplify_someHyps; subst; eauto. Qed. +Import ListNotations. +Local Open Scope list_scope. + Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := | exec_Bgoto pc: final_step stack f sp rs m (Bgoto pc) E0 - (State stack f sp pc (tr_exit f pc None rs) m) + (State stack f sp pc (tr_exit f [pc] None rs) m) | exec_Breturn or stk m': sp = (Vptr stk Ptrofs.zero) -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> @@ -295,7 +302,7 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := find_function ros rs = Some fd -> funsig fd = sig -> final_step stack f sp rs m (Bcall sig ros args res pc') - E0 (Callstate (Stackframe res f sp pc' (tr_exit f pc' (Some res) rs) :: stack) fd rs##args m) + E0 (Callstate (Stackframe res f sp pc' (tr_exit f [pc'] (Some res) rs) :: stack) fd rs##args m) | exec_Btailcall sig ros args stk m' fd: find_function ros rs = Some fd -> funsig fd = sig -> @@ -308,14 +315,14 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := external_call ef ge vargs m t vres m' -> final_step stack f sp rs m (Bbuiltin ef args res pc') (* TODO: not clear that this is the better choice ! - we coud also do something like [regmap_setres res vres (tr_exit f pc' (reg_builtin_res res) rs)] + we coud also do something like [regmap_setres res vres (tr_exit f [pc'] (reg_builtin_res res) rs)] *) - t (State stack f sp pc' (tr_exit f pc' None (regmap_setres res vres rs)) m') + t (State stack f sp pc' (tr_exit f [pc'] None (regmap_setres res vres rs)) m') | exec_Bjumptable arg tbl n pc': rs#arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some pc' -> final_step stack f sp rs m (Bjumptable arg tbl) - E0 (State stack f sp pc' (tr_exit f pc' None rs) m) + E0 (State stack f sp pc' (tr_exit f tbl None rs) m) . (** big-step execution of one iblock *) @@ -375,7 +382,7 @@ Inductive final_state: state -> int -> Prop := (** The basic small-step semantics for a BTL program. *) (* tid = transfer_identity *) -Definition tid (_:function) (_:exit) (_: option reg) (rs:regset) := rs. +Definition tid (_:function) (_:list exit) (_: option reg) (rs:regset) := rs. Definition semantics (p: program) := Semantics (step tid) (initial_state p) final_state (Genv.globalenv p). @@ -405,19 +412,51 @@ Proof. - rewrite Regmap.gso; auto. Qed. -Definition inputs_exit (f:function) (pc: exit) (or:option reg): Regset.t := - match f.(fn_code)!pc with - | None => Regset.empty - | Some ib => - match or with - | Some r => Regset.remove r ib.(input_regs) - | None => ib.(input_regs) - end +Fixpoint inputs_exitrec (f:function) (tbl: list exit): Regset.t := + match tbl with + | nil => Regset.empty + | pc::l => let rs:= inputs_exitrec f l in + match f.(fn_code)!pc with + | None => rs + | Some ib => Regset.union rs ib.(input_regs) + end end. -Definition tr_inputs (f:function) (pc: exit) (or:option reg): regset -> regset +Lemma inputs_exitrec_In f tbl r: + Regset.In r (inputs_exitrec f tbl) -> (exists pc, List.In pc tbl /\ exists ib, f.(fn_code)!pc = Some ib /\ Regset.In r ib.(input_regs)). +Proof. + induction tbl as [|pc l]; simpl; intros. + - exploit Regset.empty_1; eauto. intuition. + - destruct ((fn_code f) ! pc) eqn:ATpc. + + exploit Regset.union_1; eauto. + destruct 1 as [X1|X1]. + * destruct IHl as (pc' & H1 & H2); eauto. + * eexists; intuition eauto. + + destruct IHl as (pc' & H1 & H2); eauto. +Qed. + +Lemma inputs_exitrec_notIn f tbl r: + (forall pc ib, List.In pc tbl -> f.(fn_code)!pc = Some ib -> ~Regset.In r ib.(input_regs)) + -> ~Regset.In r (inputs_exitrec f tbl). +Proof. + induction tbl as [|pc l]; simpl; intuition eauto. + - exploit Regset.empty_1; eauto. + - destruct ((fn_code f) ! pc) eqn:ATpc; intuition eauto. + exploit Regset.union_1; intuition eauto. +Qed. + +Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t := + let rs := inputs_exitrec f tbl in + match or with + | Some r => Regset.remove r rs + | None => rs + end. + +Definition tr_inputs (f:function) (pc: list exit) (or:option reg): regset -> regset := transfer_regs (Regset.elements (inputs_exit f pc or)). + + (* TODO: move this elsewhere *) Lemma SetoidList_InA_eq_equiv A (l: list A): forall x, SetoidList.InA (fun x y => x = y) x l <-> List.In x l. @@ -443,6 +482,24 @@ Proof. rewrite -> SetoidList_InA_eq_equiv; eauto. Qed. +Definition Regset_In_dec r rs: + { Regset.In r rs } + { ~(Regset.In r rs)}. +Proof. + destruct (Regset.mem r rs) eqn: IsIN. + + left. abstract (eapply Regset.mem_2; auto). + + right. + abstract (intro H; exploit Regset.mem_1; eauto; congruence). +Defined. + +Lemma tr_inputs_ext f pc or rs1 rs2: + (forall r, Regset.In r (inputs_exit f pc or) -> rs1#r = rs2#r) -> + (forall r, (tr_inputs f pc or rs1)#r = (tr_inputs f pc or rs2)#r). +Proof. + intros EQ r. destruct (Regset_In_dec r (inputs_exit f pc or)). + + rewrite! tr_inputs_exit; eauto. + + rewrite! tr_inputs_dead; eauto. +Qed. + Definition fsem (p: program) := Semantics (step tr_inputs) (initial_state p) final_state (Genv.globalenv p). -- cgit From 85aa6d418e077a9f492f800b3f61fb5ead705e4d Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 25 May 2021 18:25:22 +0200 Subject: fix Builtin semantics --- scheduling/BTL.v | 34 ++++++++++++++++++++++++---------- 1 file changed, 24 insertions(+), 10 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 4ae7a6dd..954b4cb4 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -18,6 +18,8 @@ Require Import Coqlib Maps. Require Import AST Integers Values Events Memory Globalenvs Smallstep. Require Import RTL Op Registers OptionMonad. +Import ListNotations. + (** * Abstract syntax *) Definition exit := node. (* we may generalize this with register renamings at exit, @@ -159,12 +161,15 @@ Record outcome := out { _fin: option final }. - - +(* follows RTL semantics to set the result of builtin *) +Definition reg_builtin_res (res: builtin_res reg): option reg := + match res with + | BR r => Some r + | _ => None + end. Section RELSEM. - (** [step] (and in particular [final_step]) is parametrized by function [tr_exit] to transfer registers on each iblock exit. In particular, [tr_exit f lpc or rs] computes from [rs] the [rs'] on which the execution from iblock [pc] in [lpc] in [f] may start. @@ -286,7 +291,6 @@ Proof. destruct o; try_simplify_someHyps; subst; eauto. Qed. -Import ListNotations. Local Open Scope list_scope. Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := @@ -314,10 +318,7 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := eval_builtin_args ge (fun r => rs#r) sp m args vargs -> external_call ef ge vargs m t vres m' -> final_step stack f sp rs m (Bbuiltin ef args res pc') - (* TODO: not clear that this is the better choice ! - we coud also do something like [regmap_setres res vres (tr_exit f [pc'] (reg_builtin_res res) rs)] - *) - t (State stack f sp pc' (tr_exit f [pc'] None (regmap_setres res vres rs)) m') + t (State stack f sp pc' (regmap_setres res vres (tr_exit f [pc'] (reg_builtin_res res) rs)) m') | exec_Bjumptable arg tbl n pc': rs#arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some pc' -> @@ -455,8 +456,6 @@ Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t Definition tr_inputs (f:function) (pc: list exit) (or:option reg): regset -> regset := transfer_regs (Regset.elements (inputs_exit f pc or)). - - (* TODO: move this elsewhere *) Lemma SetoidList_InA_eq_equiv A (l: list A): forall x, SetoidList.InA (fun x y => x = y) x l <-> List.In x l. @@ -503,6 +502,21 @@ Qed. Definition fsem (p: program) := Semantics (step tr_inputs) (initial_state p) final_state (Genv.globalenv p). +Local Open Scope list_scope. + +Definition poly_tr {A} (tr: function -> list exit -> option reg -> A) f (i: final): A := + match i with + | Bgoto pc => tr f [pc] None + | Bcall sig ros args res pc => tr f [pc] (Some res) + | Btailcall sig ros args => tr f [] None + | Bbuiltin ef args res pc => tr f [pc] (reg_builtin_res res) + | Breturn or => tr f [] None + | Bjumptable reg tbl => tr f tbl None + end. + +Definition tr_regs: function -> final -> regset -> regset := + poly_tr tr_inputs. + (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) (** Matching BTL and RTL code -- cgit From 47599a2ea88799d654ec644fe5ba9892087adb39 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 26 May 2021 16:27:21 +0200 Subject: fix tr_sis definition --- scheduling/BTL.v | 66 +++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 42 insertions(+), 24 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 954b4cb4..5f75231a 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -453,8 +453,8 @@ Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t | None => rs end. -Definition tr_inputs (f:function) (pc: list exit) (or:option reg): regset -> regset - := transfer_regs (Regset.elements (inputs_exit f pc or)). +Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset + := transfer_regs (Regset.elements (inputs_exit f tbl or)). (* TODO: move this elsewhere *) Lemma SetoidList_InA_eq_equiv A (l: list A): forall x, @@ -465,38 +465,39 @@ Proof. - induction l; simpl; intuition. Qed. -Lemma tr_inputs_exit f pc or rs r: - Regset.In r (inputs_exit f pc or) -> (tr_inputs f pc or rs)#r = rs#r. +Lemma tr_inputs_exit f tbl or rs r: + Regset.In r (inputs_exit f tbl or) -> (tr_inputs f tbl or rs)#r = rs#r. Proof. intros; eapply transfer_regs_inputs. rewrite <- SetoidList_InA_eq_equiv. eapply Regset.elements_1; eauto. Qed. -Lemma tr_inputs_dead f pc or rs r: - ~(Regset.In r (inputs_exit f pc or)) -> (tr_inputs f pc or rs)#r = Vundef. +Lemma tr_inputs_dead f tbl or rs r: + ~(Regset.In r (inputs_exit f tbl or)) -> (tr_inputs f tbl or rs)#r = Vundef. Proof. intros X; eapply transfer_regs_dead; intuition eauto. eapply X. eapply Regset.elements_2. rewrite -> SetoidList_InA_eq_equiv; eauto. Qed. -Definition Regset_In_dec r rs: - { Regset.In r rs } + { ~(Regset.In r rs)}. +Local Hint Resolve tr_inputs_exit Regset.mem_2 Regset.mem_1: core. + +Lemma tr_inputs_get f tbl or rs r: + (tr_inputs f tbl or rs)#r = if Regset.mem r (inputs_exit f tbl or) then rs#r else Vundef. Proof. - destruct (Regset.mem r rs) eqn: IsIN. - + left. abstract (eapply Regset.mem_2; auto). - + right. - abstract (intro H; exploit Regset.mem_1; eauto; congruence). -Defined. + autodestruct; eauto. + intros; apply tr_inputs_dead; eauto. + intro X; exploit Regset.mem_1; eauto. + congruence. +Qed. -Lemma tr_inputs_ext f pc or rs1 rs2: - (forall r, Regset.In r (inputs_exit f pc or) -> rs1#r = rs2#r) -> - (forall r, (tr_inputs f pc or rs1)#r = (tr_inputs f pc or rs2)#r). +Lemma tr_inputs_ext f tbl or rs1 rs2: + (forall r, Regset.In r (inputs_exit f tbl or) -> rs1#r = rs2#r) -> + (forall r, (tr_inputs f tbl or rs1)#r = (tr_inputs f tbl or rs2)#r). Proof. - intros EQ r. destruct (Regset_In_dec r (inputs_exit f pc or)). - + rewrite! tr_inputs_exit; eauto. - + rewrite! tr_inputs_dead; eauto. + intros EQ r. rewrite !tr_inputs_get. + autodestruct; auto. Qed. Definition fsem (p: program) := @@ -507,16 +508,33 @@ Local Open Scope list_scope. Definition poly_tr {A} (tr: function -> list exit -> option reg -> A) f (i: final): A := match i with | Bgoto pc => tr f [pc] None - | Bcall sig ros args res pc => tr f [pc] (Some res) - | Btailcall sig ros args => tr f [] None - | Bbuiltin ef args res pc => tr f [pc] (reg_builtin_res res) - | Breturn or => tr f [] None - | Bjumptable reg tbl => tr f tbl None + | Bcall _ _ _ res pc => tr f [pc] (Some res) + | Btailcall _ _ args => tr f [] None + | Bbuiltin _ _ res pc => tr f [pc] (reg_builtin_res res) + | Breturn _ => tr f [] None + | Bjumptable _ tbl => tr f tbl None end. Definition tr_regs: function -> final -> regset -> regset := poly_tr tr_inputs. +Definition liveout: function -> final -> Regset.t := + poly_tr inputs_exit. + +Lemma tr_regs_liveout_equiv f fi : tr_regs f fi = transfer_regs (Regset.elements (liveout f fi)). +Proof. + destruct fi; simpl; auto. +Qed. + +Local Hint Resolve tr_inputs_get: core. + +Lemma tr_regs_get f fi rs r: (tr_regs f fi rs)#r = if Regset.mem r (liveout f fi) then rs#r else Vundef. +Proof. + Local Opaque inputs_exit. + destruct fi; simpl; auto. +Qed. + + (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) (** Matching BTL and RTL code -- cgit From d76f6a446a8c4866d7e89b1b5b13b24a20e6d1dc Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 26 May 2021 21:42:33 +0200 Subject: end of BTL_SEtheory w.r.t fsem --- scheduling/BTL.v | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 5f75231a..6f699cd0 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -391,10 +391,11 @@ Definition semantics (p: program) := (** The "functional" small-step semantics for a BTL program. at each exit, we only transfer register in "input_regs" (i.e. "alive" registers). *) - Definition transfer_regs (inputs: list reg) (rs: regset): regset := init_regs (rs##inputs) inputs. +(* TODO: LEMMA BELOW ON transfer_regs USEFUL ? *) + Lemma transfer_regs_inputs inputs rs r: List.In r inputs -> (transfer_regs inputs rs)#r = rs#r. Proof. @@ -456,6 +457,9 @@ Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset := transfer_regs (Regset.elements (inputs_exit f tbl or)). +(* TODO: BELOW, LEMMA on tr_inputs USEFUL ? *) + + (* TODO: move this elsewhere *) Lemma SetoidList_InA_eq_equiv A (l: list A): forall x, SetoidList.InA (fun x y => x = y) x l <-> List.In x l. @@ -518,6 +522,7 @@ Definition poly_tr {A} (tr: function -> list exit -> option reg -> A) f (i: fina Definition tr_regs: function -> final -> regset -> regset := poly_tr tr_inputs. +(* TODO: NOT USEFUL ? Definition liveout: function -> final -> Regset.t := poly_tr inputs_exit. @@ -533,7 +538,7 @@ Proof. Local Opaque inputs_exit. destruct fi; simpl; auto. Qed. - +*) (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) -- cgit From e30376ce891d0710757c65e85a24e7d2550a37ed Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 27 May 2021 13:49:35 +0200 Subject: cleaning BTL_SEtheory --- scheduling/BTL.v | 73 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 73 insertions(+) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 6f699cd0..bf19f4ac 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -540,6 +540,79 @@ Proof. Qed. *) +(* * Reasoning modulo extensionality of [regset] into BTL semantics *) +Inductive equiv_stackframe: stackframe -> stackframe -> Prop := + | equiv_stackframe_intro res f sp pc rs1 rs2 + (EQUIV: forall r : positive, rs1 !! r = rs2 !! r): + equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2) + . + +Inductive equiv_state: state -> state -> Prop := + | State_equiv stack f sp pc rs1 m rs2 + (EQUIV: forall r, rs1#r = rs2#r): + equiv_state (State stack f sp pc rs1 m) (State stack f sp pc rs2 m) + | Call_equiv stk stk' f args m + (STACKS: list_forall2 equiv_stackframe stk stk'): + equiv_state (Callstate stk f args m) (Callstate stk' f args m) + | Return_equiv stk stk' v m + (STACKS: list_forall2 equiv_stackframe stk stk'): + equiv_state (Returnstate stk v m) (Returnstate stk' v m) + . + +Local Hint Constructors equiv_stackframe equiv_state: core. + +Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf. +Proof. + destruct stf; eauto. +Qed. + +Lemma equiv_stack_refl stk: list_forall2 equiv_stackframe stk stk. +Proof. + Local Hint Resolve equiv_stackframe_refl: core. + induction stk; simpl; constructor; auto. +Qed. + +Lemma equiv_state_refl s: equiv_state s s. +Proof. + Local Hint Resolve equiv_stack_refl: core. + induction s; simpl; constructor; auto. +Qed. + +Lemma equiv_stackframe_trans stf1 stf2 stf3: + equiv_stackframe stf1 stf2 -> equiv_stackframe stf2 stf3 -> equiv_stackframe stf1 stf3. +Proof. + destruct 1; intros EQ; inv EQ; try econstructor; eauto. + intros; eapply eq_trans; eauto. +Qed. + +Lemma equiv_stack_trans stk1 stk2: + list_forall2 equiv_stackframe stk1 stk2 -> + forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> + list_forall2 equiv_stackframe stk1 stk3. +Proof. + Local Hint Resolve equiv_stackframe_trans: core. + induction 1; intros stk3 EQ; inv EQ; econstructor; eauto. +Qed. + +Lemma equiv_state_trans s1 s2 s3: equiv_state s1 s2 -> equiv_state s2 s3 -> equiv_state s1 s3. +Proof. + Local Hint Resolve equiv_stack_trans: core. + destruct 1; intros EQ; inv EQ; econstructor; eauto. + intros; eapply eq_trans; eauto. +Qed. + +Lemma regmap_setres_eq (rs rs': regset) res vres: + (forall r, rs # r = rs' # r) -> + forall r, (regmap_setres res vres rs) # r = (regmap_setres res vres rs') # r. +Proof. + intros RSEQ r. destruct res; simpl; try congruence. + destruct (peq x r). + - subst. repeat (rewrite Regmap.gss). reflexivity. + - repeat (rewrite Regmap.gso); auto. +Qed. + + + (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) (** Matching BTL and RTL code -- cgit From 1a78c940f46273b7146d2111b1e2da309434f021 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 27 May 2021 16:55:18 +0200 Subject: [disabled checker] BTL Scheduling and Renumbering OK! --- scheduling/BTL.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 0f9ef44f..991361ca 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -25,11 +25,11 @@ Definition exit := node. (* we may generalize this with register renamings at e (* inst_info is a ghost record to provide instruction information through oracles *) Parameter inst_info: Set. -Extract Constant inst_info => "BTLaux.inst_info". +Extract Constant inst_info => "BTLtypes.inst_info". (* block_info is a ghost record to provide block information through oracles *) Parameter block_info: Set. -Extract Constant block_info => "BTLaux.block_info". +Extract Constant block_info => "BTLtypes.block_info". (** final instructions (that stops block execution) *) Inductive final: Type := -- cgit From 43ab0b948ac379e55bbe334a0a541c1680437fbf Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 28 May 2021 10:40:54 +0200 Subject: most of the proof BTL.fsem -> BTL.cfgsem. --- scheduling/BTL.v | 308 +++++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 267 insertions(+), 41 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index bf19f4ac..389d8d93 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -17,6 +17,7 @@ Require Import Coqlib Maps. Require Import AST Integers Values Events Memory Globalenvs Smallstep. Require Import RTL Op Registers OptionMonad. +Require Import Lia. Import ListNotations. @@ -380,22 +381,20 @@ Inductive final_state: state -> int -> Prop := | final_state_intro: forall r m, final_state (Returnstate nil (Vint r) m) r. -(** The basic small-step semantics for a BTL program. *) +(** The "raw" CFG small-step semantics for a BTL program (e.g. close to RTL semantics) *) (* tid = transfer_identity *) Definition tid (_:function) (_:list exit) (_: option reg) (rs:regset) := rs. -Definition semantics (p: program) := +Definition cfgsem (p: program) := Semantics (step tid) (initial_state p) final_state (Genv.globalenv p). -(** The "functional" small-step semantics for a BTL program. +(** The full "functional" small-step semantics for a BTL program. at each exit, we only transfer register in "input_regs" (i.e. "alive" registers). *) Definition transfer_regs (inputs: list reg) (rs: regset): regset := init_regs (rs##inputs) inputs. -(* TODO: LEMMA BELOW ON transfer_regs USEFUL ? *) - Lemma transfer_regs_inputs inputs rs r: List.In r inputs -> (transfer_regs inputs rs)#r = rs#r. Proof. @@ -414,18 +413,20 @@ Proof. - rewrite Regmap.gso; auto. Qed. -Fixpoint inputs_exitrec (f:function) (tbl: list exit): Regset.t := +Fixpoint union_inputs (f:function) (tbl: list exit): Regset.t := match tbl with | nil => Regset.empty - | pc::l => let rs:= inputs_exitrec f l in + | pc::l => let rs:= union_inputs f l in match f.(fn_code)!pc with | None => rs | Some ib => Regset.union rs ib.(input_regs) end end. -Lemma inputs_exitrec_In f tbl r: - Regset.In r (inputs_exitrec f tbl) -> (exists pc, List.In pc tbl /\ exists ib, f.(fn_code)!pc = Some ib /\ Regset.In r ib.(input_regs)). +(* TODO: lemma not yet used + +Lemma union_inputs_In f tbl r: + Regset.In r (union_inputs f tbl) -> (exists pc, List.In pc tbl /\ exists ib, f.(fn_code)!pc = Some ib /\ Regset.In r ib.(input_regs)). Proof. induction tbl as [|pc l]; simpl; intros. - exploit Regset.empty_1; eauto. intuition. @@ -437,27 +438,33 @@ Proof. + destruct IHl as (pc' & H1 & H2); eauto. Qed. -Lemma inputs_exitrec_notIn f tbl r: +Lemma union_inputs_notIn f tbl r: (forall pc ib, List.In pc tbl -> f.(fn_code)!pc = Some ib -> ~Regset.In r ib.(input_regs)) - -> ~Regset.In r (inputs_exitrec f tbl). + -> ~Regset.In r (union_inputs f tbl). Proof. induction tbl as [|pc l]; simpl; intuition eauto. - exploit Regset.empty_1; eauto. - destruct ((fn_code f) ! pc) eqn:ATpc; intuition eauto. exploit Regset.union_1; intuition eauto. Qed. +*) -Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t := - let rs := inputs_exitrec f tbl in +(* This function computes the union of the inputs associated to the exits + minus the optional register in [or] (typically the result of a call or a builtin). + i.e. similar to [pre_output_regs] in RTLpath. +*) +Definition pre_inputs (f:function) (tbl: list exit) (or: option reg): Regset.t := + let rs := union_inputs f tbl in match or with | Some r => Regset.remove r rs | None => rs - end. + end + . -Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset - := transfer_regs (Regset.elements (inputs_exit f tbl or)). +(* TODO: lemma pre_inputs_In + pre_inputs_notIn ? *) -(* TODO: BELOW, LEMMA on tr_inputs USEFUL ? *) +Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset + := transfer_regs (Regset.elements (pre_inputs f tbl or)). (* TODO: move this elsewhere *) @@ -469,8 +476,8 @@ Proof. - induction l; simpl; intuition. Qed. -Lemma tr_inputs_exit f tbl or rs r: - Regset.In r (inputs_exit f tbl or) -> (tr_inputs f tbl or rs)#r = rs#r. +Lemma tr_pre_inputs f tbl or rs r: + Regset.In r (pre_inputs f tbl or) -> (tr_inputs f tbl or rs)#r = rs#r. Proof. intros; eapply transfer_regs_inputs. rewrite <- SetoidList_InA_eq_equiv. @@ -478,17 +485,17 @@ Proof. Qed. Lemma tr_inputs_dead f tbl or rs r: - ~(Regset.In r (inputs_exit f tbl or)) -> (tr_inputs f tbl or rs)#r = Vundef. + ~(Regset.In r (pre_inputs f tbl or)) -> (tr_inputs f tbl or rs)#r = Vundef. Proof. intros X; eapply transfer_regs_dead; intuition eauto. eapply X. eapply Regset.elements_2. rewrite -> SetoidList_InA_eq_equiv; eauto. Qed. -Local Hint Resolve tr_inputs_exit Regset.mem_2 Regset.mem_1: core. +Local Hint Resolve tr_pre_inputs Regset.mem_2 Regset.mem_1: core. Lemma tr_inputs_get f tbl or rs r: - (tr_inputs f tbl or rs)#r = if Regset.mem r (inputs_exit f tbl or) then rs#r else Vundef. + (tr_inputs f tbl or rs)#r = if Regset.mem r (pre_inputs f tbl or) then rs#r else Vundef. Proof. autodestruct; eauto. intros; apply tr_inputs_dead; eauto. @@ -496,13 +503,15 @@ Proof. congruence. Qed. +(* TODO: not yet used Lemma tr_inputs_ext f tbl or rs1 rs2: - (forall r, Regset.In r (inputs_exit f tbl or) -> rs1#r = rs2#r) -> + (forall r, Regset.In r (pre_inputs f tbl or) -> rs1#r = rs2#r) -> (forall r, (tr_inputs f tbl or rs1)#r = (tr_inputs f tbl or rs2)#r). Proof. intros EQ r. rewrite !tr_inputs_get. autodestruct; auto. Qed. +*) Definition fsem (p: program) := Semantics (step tr_inputs) (initial_state p) final_state (Genv.globalenv p). @@ -524,7 +533,7 @@ Definition tr_regs: function -> final -> regset -> regset := (* TODO: NOT USEFUL ? Definition liveout: function -> final -> Regset.t := - poly_tr inputs_exit. + poly_tr pre_inputs. Lemma tr_regs_liveout_equiv f fi : tr_regs f fi = transfer_regs (Regset.elements (liveout f fi)). Proof. @@ -535,30 +544,34 @@ Local Hint Resolve tr_inputs_get: core. Lemma tr_regs_get f fi rs r: (tr_regs f fi rs)#r = if Regset.mem r (liveout f fi) then rs#r else Vundef. Proof. - Local Opaque inputs_exit. + Local Opaque pre_inputs. destruct fi; simpl; auto. Qed. *) -(* * Reasoning modulo extensionality of [regset] into BTL semantics *) +(* * Comparing BTL semantics modulo extensionality of [regset]. + +NB: This is at least used in BTL_SEtheory (and probably in the future BTL_SchedulerProof). + +*) Inductive equiv_stackframe: stackframe -> stackframe -> Prop := - | equiv_stackframe_intro res f sp pc rs1 rs2 - (EQUIV: forall r : positive, rs1 !! r = rs2 !! r): - equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2) + | equiv_stackframe_intro res f sp pc (rs1 rs2: regset) + (EQUIV: forall r, rs1#r = rs2#r) + :equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2) . Inductive equiv_state: state -> state -> Prop := - | State_equiv stack f sp pc rs1 m rs2 - (EQUIV: forall r, rs1#r = rs2#r): - equiv_state (State stack f sp pc rs1 m) (State stack f sp pc rs2 m) - | Call_equiv stk stk' f args m - (STACKS: list_forall2 equiv_stackframe stk stk'): - equiv_state (Callstate stk f args m) (Callstate stk' f args m) - | Return_equiv stk stk' v m - (STACKS: list_forall2 equiv_stackframe stk stk'): - equiv_state (Returnstate stk v m) (Returnstate stk' v m) + | State_equiv stk1 stk2 f sp pc rs1 m rs2 + (STACKS: list_forall2 equiv_stackframe stk1 stk2) + (EQUIV: forall r, rs1#r = rs2#r) + :equiv_state (State stk1 f sp pc rs1 m) (State stk2 f sp pc rs2 m) + | Call_equiv stk1 stk2 f args m + (STACKS: list_forall2 equiv_stackframe stk1 stk2) + :equiv_state (Callstate stk1 f args m) (Callstate stk2 f args m) + | Return_equiv stk1 stk2 v m + (STACKS: list_forall2 equiv_stackframe stk1 stk2) + :equiv_state (Returnstate stk1 v m) (Returnstate stk2 v m) . - Local Hint Constructors equiv_stackframe equiv_state: core. Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf. @@ -571,10 +584,10 @@ Proof. Local Hint Resolve equiv_stackframe_refl: core. induction stk; simpl; constructor; auto. Qed. +Local Hint Resolve equiv_stack_refl: core. Lemma equiv_state_refl s: equiv_state s s. Proof. - Local Hint Resolve equiv_stack_refl: core. induction s; simpl; constructor; auto. Qed. @@ -584,13 +597,13 @@ Proof. destruct 1; intros EQ; inv EQ; try econstructor; eauto. intros; eapply eq_trans; eauto. Qed. +Local Hint Resolve equiv_stackframe_trans: core. Lemma equiv_stack_trans stk1 stk2: list_forall2 equiv_stackframe stk1 stk2 -> forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> list_forall2 equiv_stackframe stk1 stk3. Proof. - Local Hint Resolve equiv_stackframe_trans: core. induction 1; intros stk3 EQ; inv EQ; econstructor; eauto. Qed. @@ -611,7 +624,220 @@ Proof. - repeat (rewrite Regmap.gso); auto. Qed. +(* * Simulation of BTL fsem by BTL cfgsem: a lock-step less-def simulation. +We start by extending the previous [equiv_*] stuff for [Val.lessdef]: we need to also compare memories +for Mem.extends, because Vundef values are propagated in memory through stores, allocation, etc. + +*) + +Inductive lessdef_stackframe: stackframe -> stackframe -> Prop := + | lessdef_stackframe_intro res f sp pc rs1 rs2 + (REGS: forall r, Val.lessdef rs1#r rs2#r) + :lessdef_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2) + . + +Inductive lessdef_state: state -> state -> Prop := + | State_lessdef stk1 stk2 f sp pc rs1 m1 rs2 m2 + (STACKS: list_forall2 lessdef_stackframe stk1 stk2) + (REGS: forall r, Val.lessdef rs1#r rs2#r) + (MEMS: Mem.extends m1 m2) + :lessdef_state (State stk1 f sp pc rs1 m1) (State stk2 f sp pc rs2 m2) + | Call_lessdef stk1 stk2 f args1 args2 m1 m2 + (STACKS: list_forall2 lessdef_stackframe stk1 stk2) + (ARGS: Val.lessdef_list args1 args2) + (MEMS: Mem.extends m1 m2) + :lessdef_state (Callstate stk1 f args1 m1) (Callstate stk2 f args2 m2) + | Return_lessdef stk1 stk2 v1 v2 m1 m2 + (STACKS: list_forall2 lessdef_stackframe stk1 stk2) + (REGS: Val.lessdef v1 v2) + (MEMS: Mem.extends m1 m2) + :lessdef_state (Returnstate stk1 v1 m1) (Returnstate stk2 v2 m2) + . +Local Hint Constructors lessdef_stackframe lessdef_state: core. + +Lemma lessdef_stackframe_refl stf: lessdef_stackframe stf stf. +Proof. + destruct stf; eauto. +Qed. + +Local Hint Resolve lessdef_stackframe_refl: core. +Lemma lessdef_stack_refl stk: list_forall2 lessdef_stackframe stk stk. +Proof. + induction stk; simpl; constructor; auto. +Qed. + +Local Hint Resolve lessdef_stack_refl: core. + +Lemma lessdef_list_refl args: Val.lessdef_list args args. +Proof. + induction args; simpl; auto. +Qed. + +Local Hint Resolve lessdef_list_refl Mem.extends_refl: core. + +Lemma lessdef_state_refl s: lessdef_state s s. +Proof. + induction s; simpl; constructor; auto. +Qed. + +Local Hint Resolve Val.lessdef_trans: core. +Lemma lessdef_stackframe_trans stf1 stf2 stf3: + lessdef_stackframe stf1 stf2 -> lessdef_stackframe stf2 stf3 -> lessdef_stackframe stf1 stf3. +Proof. + destruct 1. intros LD; inv LD; try econstructor; eauto. +Qed. + +Local Hint Resolve lessdef_stackframe_trans: core. +Lemma lessdef_stack_trans stk1 stk2: + list_forall2 lessdef_stackframe stk1 stk2 -> + forall stk3, list_forall2 lessdef_stackframe stk2 stk3 -> + list_forall2 lessdef_stackframe stk1 stk3. +Proof. + induction 1; intros stk3 LD; inv LD; econstructor; eauto. +Qed. + +Local Hint Resolve lessdef_stack_trans Mem.extends_extends_compose Val.lessdef_list_trans: core. +Lemma lessdef_state_trans s1 s2 s3: lessdef_state s1 s2 -> lessdef_state s2 s3 -> lessdef_state s1 s3. +Proof. + destruct 1; intros LD; inv LD; econstructor; eauto. +Qed. + +Lemma init_regs_lessdef_preserv args1 args2 + (ARGS : Val.lessdef_list args1 args2) + : forall rl r, Val.lessdef (init_regs args1 rl)#r (init_regs args2 rl)#r. +Proof. + induction ARGS; simpl; auto. + intros rl r1; destruct rl; simpl in *; auto. + eapply set_reg_lessdef; eauto. + intros r2; eauto. +Qed. +Local Hint Resolve init_regs_lessdef_preserv: core. + +Lemma tr_inputs_lessdef f rs1 rs2 tbl or r + (REGS: forall r, Val.lessdef rs1#r rs2#r) + :Val.lessdef (tr_inputs f tbl or rs1)#r (tid f tbl or rs2)#r. +Proof. + unfold tid; rewrite tr_inputs_get. + autodestruct. +Qed. +Local Hint Resolve tr_inputs_lessdef: core. + +Lemma find_function_lessdef ge ros rs1 rs2 fd + (FIND: find_function ge ros rs1 = Some fd) + (REGS: forall r, Val.lessdef rs1#r rs2#r) + : find_function ge ros rs2 = Some fd. +Proof. + destruct ros; simpl in *; auto. + exploit Genv.find_funct_inv; eauto. + intros (b & EQ). + destruct (REGS r); try congruence. +Qed. +Local Hint Resolve find_function_lessdef regs_lessdef_regs: core. + + +Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 ib rs1' m1' of + (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of) + rs2 m2 + (REGS: forall r, Val.lessdef rs1#r rs2#r) + (MEMS: Mem.extends m1 m2) + : exists rs2' m2', iblock_istep_run ge sp ib rs2 m2 = Some (out rs2' m2' of) + /\ (forall r, Val.lessdef rs1'#r rs2'#r) + /\ (Mem.extends m1' m2'). +Proof. + induction ISTEP; simpl; try_simplify_someHyps. +Admitted. + +Local Hint Constructors final_step list_forall2: core. +Local Hint Unfold regs_lessdef: core. + +Lemma fsem2cfgsem_finalstep_simu ge stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2 + (FSTEP: final_step tr_inputs ge stk1 f sp rs1 m1 fin t s1) + (STACKS: list_forall2 lessdef_stackframe stk1 stk2) + (REGS: forall r, Val.lessdef rs1#r rs2#r) + (MEMS: Mem.extends m1 m2) + : exists s2, final_step tid ge stk2 f sp rs2 m2 fin t s2 + /\ lessdef_state s1 s2. +Proof. + destruct FSTEP; try (eexists; split; simpl; econstructor; eauto; fail). + - (* return *) + exploit Mem.free_parallel_extends; eauto. + intros (m2' & FREE & MEMS2). + eexists; split; simpl; econstructor; eauto. + destruct or; simpl; auto. + - (* tailcall *) + exploit Mem.free_parallel_extends; eauto. + intros (m2' & FREE & MEMS2). + eexists; split; simpl; econstructor; eauto. + - (* builtin *) + exploit (eval_builtin_args_lessdef (ge:=ge) (e1:=(fun r => rs1 # r)) (fun r => rs2 # r)); eauto. + intros (vl2' & BARGS & VARGS). + exploit external_call_mem_extends; eauto. + intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED). + eexists; split; simpl; econstructor; eauto. + intros; apply set_res_lessdef; eauto. + - (* jumptable *) + eexists; split; simpl; econstructor; eauto. + destruct (REGS arg); try congruence. +Qed. + +Lemma fsem2cfgsem_ibstep_simu ge stk1 stk2 f sp rs1 m1 ib t s1 rs2 m2 + (STEP: iblock_step tr_inputs ge stk1 f sp rs1 m1 ib t s1) + (STACKS : list_forall2 lessdef_stackframe stk1 stk2) + (REGS: forall r, Val.lessdef rs1#r rs2#r) + (MEMS : Mem.extends m1 m2) + : exists s2, iblock_step tid ge stk2 f sp rs2 m2 ib t s2 + /\ lessdef_state s1 s2. +Proof. + destruct STEP as (rs1' & m1' & fin & ISTEP & FSTEP). + exploit fsem2cfgsem_ibistep_simu; eauto. + intros (rs2' & m2' & ISTEP2 & REGS2 & MEMS2). + rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP REGS MEMS. + exploit fsem2cfgsem_finalstep_simu; eauto. + intros (s2 & FSTEP2 & LESSDEF). clear FSTEP. + unfold iblock_step; eexists; split; eauto. +Qed. + +Local Hint Constructors step: core. + +Lemma fsem2cfgsem_step_simu ge s1 t s1' s2 + (STEP: step tr_inputs ge s1 t s1') + (REGS: lessdef_state s1 s2) + :exists s2' : state, + step tid ge s2 t s2' /\ + lessdef_state s1' s2'. +Proof. + destruct STEP; inv REGS. + - (* iblock *) + intros; exploit fsem2cfgsem_ibstep_simu; eauto. clear STEP. + intros (s2 & STEP2 & REGS2). + eexists; split; eauto. + - (* internal call *) + exploit (Mem.alloc_extends m m2 0 (fn_stacksize f) stk m' 0 (fn_stacksize f)); eauto. + 1-2: lia. + intros (m2' & ALLOC2 & MEMS2). clear ALLOC MEMS. + eexists; split; econstructor; eauto. + - (* external call *) + exploit external_call_mem_extends; eauto. + intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED). clear EXTCALL MEMS. + eexists; split; econstructor; eauto. + - (* return *) + inversion STACKS as [|d1 d2 d3 d4 STF2 STK2]. subst. + inv STF2. + eexists; split; econstructor; eauto. + intros; eapply set_reg_lessdef; eauto. +Qed. + +Theorem fsem2cfgsem prog: + forward_simulation (fsem prog) (cfgsem prog). +Proof. + eapply forward_simulation_step with lessdef_state; simpl; auto. + - destruct 1; intros; eexists; intuition eauto. econstructor; eauto. + - intros s1 s2 r REGS FINAL; destruct FINAL. + inv REGS; inv STACKS; inv REGS0. + econstructor; eauto. + - intros; eapply fsem2cfgsem_step_simu; eauto. +Qed. (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) -- cgit From 8752cea89f862d92d49183fe10d1918588143ab1 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 28 May 2021 12:38:05 +0200 Subject: fix some merge errors --- scheduling/BTL.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 2be4fcac..2c1dda5b 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -94,7 +94,7 @@ Coercion BF: final >-> Funclass. Record iblock_info := { entry: iblock; - input_regs: Regset.t (* extra liveness information for BTL functional semantics *) + input_regs: Regset.t; (* extra liveness information for BTL functional semantics *) binfo: block_info (* Ghost field used in oracles *) }. @@ -1285,4 +1285,4 @@ Definition is_goto (ib: iblock): bool := match ib with | BF (Bgoto _) _ => true | _ => false - end. \ No newline at end of file + end. -- cgit From 25595a7b34b70011dcb77aae277ee1cdb8920c60 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 28 May 2021 14:28:56 +0200 Subject: splitting BTL by introducing BTLmatchRTL reduce also copy-paste between BTLtoRTLproof and RTLtoBTLproof sharing is done in BTLmatchRTL --- scheduling/BTL.v | 565 +------------------------------------------------------ 1 file changed, 6 insertions(+), 559 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 2c1dda5b..6536addb 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -90,8 +90,6 @@ Coercion BF: final >-> Funclass. - the same trick appears for all "basic" instructions and [Icond]. *) - - Record iblock_info := { entry: iblock; input_regs: Regset.t; (* extra liveness information for BTL functional semantics *) @@ -187,6 +185,8 @@ Section RELSEM. Here, [or] is an optional register that will be assigned after exiting the iblock, but before entering in [pc]: e.g. the register set by a function call before entering in return address. + See [tr_inputs] implementation below. + *) Variable tr_exit: function -> list exit -> option reg -> regset -> regset. @@ -390,14 +390,6 @@ Inductive final_state: state -> int -> Prop := | final_state_intro: forall r m, final_state (Returnstate nil (Vint r) m) r. -(** The "raw" CFG small-step semantics for a BTL program (e.g. close to RTL semantics) *) - -(* tid = transfer_identity *) -Definition tid (_:function) (_:list exit) (_: option reg) (rs:regset) := rs. - -Definition cfgsem (p: program) := - Semantics (step tid) (initial_state p) final_state (Genv.globalenv p). - (** The full "functional" small-step semantics for a BTL program. at each exit, we only transfer register in "input_regs" (i.e. "alive" registers). *) @@ -633,9 +625,9 @@ Proof. - repeat (rewrite Regmap.gso); auto. Qed. -(* * Simulation of BTL fsem by BTL cfgsem: a lock-step less-def simulation. +(* * Comparing BTL semantics modulo [regs_lessdef]. -We start by extending the previous [equiv_*] stuff for [Val.lessdef]: we need to also compare memories +This extends the previous [equiv_*] stuff for [Val.lessdef]. Here, we need to also compare memories for Mem.extends, because Vundef values are propagated in memory through stores, allocation, etc. *) @@ -721,16 +713,6 @@ Proof. eapply set_reg_lessdef; eauto. intros r2; eauto. Qed. -Local Hint Resolve init_regs_lessdef_preserv: core. - -Lemma tr_inputs_lessdef f rs1 rs2 tbl or r - (REGS: forall r, Val.lessdef rs1#r rs2#r) - :Val.lessdef (tr_inputs f tbl or rs1)#r (tid f tbl or rs2)#r. -Proof. - unfold tid; rewrite tr_inputs_get. - autodestruct. -Qed. -Local Hint Resolve tr_inputs_lessdef: core. Lemma find_function_lessdef ge ros rs1 rs2 fd (FIND: find_function ge ros rs1 = Some fd) @@ -742,547 +724,12 @@ Proof. intros (b & EQ). destruct (REGS r); try congruence. Qed. -Local Hint Resolve find_function_lessdef regs_lessdef_regs: core. - - -Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 ib rs1' m1' of - (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of) - rs2 m2 - (REGS: forall r, Val.lessdef rs1#r rs2#r) - (MEMS: Mem.extends m1 m2) - : exists rs2' m2', iblock_istep_run ge sp ib rs2 m2 = Some (out rs2' m2' of) - /\ (forall r, Val.lessdef rs1'#r rs2'#r) - /\ (Mem.extends m1' m2'). -Proof. - induction ISTEP; simpl; try_simplify_someHyps. -Admitted. - -Local Hint Constructors final_step list_forall2: core. -Local Hint Unfold regs_lessdef: core. - -Lemma fsem2cfgsem_finalstep_simu ge stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2 - (FSTEP: final_step tr_inputs ge stk1 f sp rs1 m1 fin t s1) - (STACKS: list_forall2 lessdef_stackframe stk1 stk2) - (REGS: forall r, Val.lessdef rs1#r rs2#r) - (MEMS: Mem.extends m1 m2) - : exists s2, final_step tid ge stk2 f sp rs2 m2 fin t s2 - /\ lessdef_state s1 s2. -Proof. - destruct FSTEP; try (eexists; split; simpl; econstructor; eauto; fail). - - (* return *) - exploit Mem.free_parallel_extends; eauto. - intros (m2' & FREE & MEMS2). - eexists; split; simpl; econstructor; eauto. - destruct or; simpl; auto. - - (* tailcall *) - exploit Mem.free_parallel_extends; eauto. - intros (m2' & FREE & MEMS2). - eexists; split; simpl; econstructor; eauto. - - (* builtin *) - exploit (eval_builtin_args_lessdef (ge:=ge) (e1:=(fun r => rs1 # r)) (fun r => rs2 # r)); eauto. - intros (vl2' & BARGS & VARGS). - exploit external_call_mem_extends; eauto. - intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED). - eexists; split; simpl; econstructor; eauto. - intros; apply set_res_lessdef; eauto. - - (* jumptable *) - eexists; split; simpl; econstructor; eauto. - destruct (REGS arg); try congruence. -Qed. - -Lemma fsem2cfgsem_ibstep_simu ge stk1 stk2 f sp rs1 m1 ib t s1 rs2 m2 - (STEP: iblock_step tr_inputs ge stk1 f sp rs1 m1 ib t s1) - (STACKS : list_forall2 lessdef_stackframe stk1 stk2) - (REGS: forall r, Val.lessdef rs1#r rs2#r) - (MEMS : Mem.extends m1 m2) - : exists s2, iblock_step tid ge stk2 f sp rs2 m2 ib t s2 - /\ lessdef_state s1 s2. -Proof. - destruct STEP as (rs1' & m1' & fin & ISTEP & FSTEP). - exploit fsem2cfgsem_ibistep_simu; eauto. - intros (rs2' & m2' & ISTEP2 & REGS2 & MEMS2). - rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP REGS MEMS. - exploit fsem2cfgsem_finalstep_simu; eauto. - intros (s2 & FSTEP2 & LESSDEF). clear FSTEP. - unfold iblock_step; eexists; split; eauto. -Qed. - -Local Hint Constructors step: core. - -Lemma fsem2cfgsem_step_simu ge s1 t s1' s2 - (STEP: step tr_inputs ge s1 t s1') - (REGS: lessdef_state s1 s2) - :exists s2' : state, - step tid ge s2 t s2' /\ - lessdef_state s1' s2'. -Proof. - destruct STEP; inv REGS. - - (* iblock *) - intros; exploit fsem2cfgsem_ibstep_simu; eauto. clear STEP. - intros (s2 & STEP2 & REGS2). - eexists; split; eauto. - - (* internal call *) - exploit (Mem.alloc_extends m m2 0 (fn_stacksize f) stk m' 0 (fn_stacksize f)); eauto. - 1-2: lia. - intros (m2' & ALLOC2 & MEMS2). clear ALLOC MEMS. - eexists; split; econstructor; eauto. - - (* external call *) - exploit external_call_mem_extends; eauto. - intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED). clear EXTCALL MEMS. - eexists; split; econstructor; eauto. - - (* return *) - inversion STACKS as [|d1 d2 d3 d4 STF2 STK2]. subst. - inv STF2. - eexists; split; econstructor; eauto. - intros; eapply set_reg_lessdef; eauto. -Qed. - -Theorem fsem2cfgsem prog: - forward_simulation (fsem prog) (cfgsem prog). -Proof. - eapply forward_simulation_step with lessdef_state; simpl; auto. - - destruct 1; intros; eexists; intuition eauto. econstructor; eauto. - - intros s1 s2 r REGS FINAL; destruct FINAL. - inv REGS; inv STACKS; inv REGS0. - econstructor; eauto. - - intros; eapply fsem2cfgsem_step_simu; eauto. -Qed. - -(** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) - -(** Matching BTL and RTL code - -We should be able to define a single verifier able to prove a bisimulation between BTL and RTL code. - -NB 1: the proof of BTL -> RTL (plus simulation) should be much easier than RTL -> BTL (star simulation). - -NB 2: our scheme allows the BTL to duplicate some RTL code. -- in other words: RTL -> BTL allows tail duplication, loop unrolling, etc. Exactly like "Duplicate" on RTL. -- BTL -> RTL allows to "undo" some duplications (e.g. remove duplications that have not enabled interesting optimizations) ! - -Hence, in a sense, our verifier imitates the approach of Duplicate, where [dupmap] maps the BTL nodes to the RTL nodes. - -The [match_*] definitions gives a "relational" specification of the verifier... -*) - -Require Import Errors. - -Inductive match_final_inst (dupmap: PTree.t node): final -> instruction -> Prop := -(* TODO: it may be simplify the oracle for BTL -> RTL, but may makes the verifier more complex ? - | mfi_goto pc pc': - dupmap!pc = (Some pc') -> match_final_inst dupmap (Bgoto pc) (Inop pc') -*) - | mfi_return or: match_final_inst dupmap (Breturn or) (Ireturn or) - | mfi_call pc pc' s ri lr r: - dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc) (Icall s ri lr r pc') - | mfi_tailcall s ri lr: - match_final_inst dupmap (Btailcall s ri lr) (Itailcall s ri lr) - | mfi_builtin pc pc' ef la br: - dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc) (Ibuiltin ef la br pc') - | mfi_jumptable ln ln' r: - list_forall2 (fun pc pc' => (dupmap!pc = (Some pc'))) ln ln' -> - match_final_inst dupmap (Bjumptable r ln) (Ijumptable r ln') -. - -Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop := - | ijo_None_left o: is_join_opt None o o - | ijo_None_right o: is_join_opt o None o - | ijo_Some x: is_join_opt (Some x) (Some x) (Some x) - . - -(* [match_iblock dupmap cfg isfst pc ib opc] means that [ib] match a block in a RTL code starting at [pc], with: - - [isfst] (in "input") indicates that no step in the surrounding block has been executed before entering [pc] - - if [opc] (in "ouput") is [None], this means that all branches of the block ends on a final instruction - - if [opc] is [Some pc'], this means that all branches of the block that do not exit, join on [pc']. -*) -Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> iblock -> (option node) -> Prop := - | mib_BF isfst fi pc i iinfo: - cfg!pc = Some i -> - match_final_inst dupmap fi i -> - match_iblock dupmap cfg isfst pc (BF fi iinfo) None - | mib_nop_on_rtl isfst pc pc' iinfo: - cfg!pc = Some (Inop pc') -> - match_iblock dupmap cfg isfst pc (Bnop (Some iinfo)) (Some pc') - | mib_nop_skip pc: - match_iblock dupmap cfg false pc (Bnop None) (Some pc) - | mib_op isfst pc pc' op lr r iinfo: - cfg!pc = Some (Iop op lr r pc') -> - match_iblock dupmap cfg isfst pc (Bop op lr r iinfo) (Some pc') - | mib_load isfst pc pc' m a lr r iinfo: - cfg!pc = Some (Iload TRAP m a lr r pc') -> - match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r iinfo) (Some pc') - | mib_store isfst pc pc' m a lr r iinfo: - cfg!pc = Some (Istore m a lr r pc') -> - match_iblock dupmap cfg isfst pc (Bstore m a lr r iinfo) (Some pc') - | mib_exit pc pc' iinfo: - dupmap!pc = (Some pc') -> - match_iblock dupmap cfg false pc' (BF (Bgoto pc) iinfo) None - (* NB: on RTL side, we exit the block by a "basic" instruction (or Icond). - Thus some step should have been executed before [pc'] in the RTL code *) - | mib_seq_Some isfst b1 b2 pc1 pc2 opc: - match_iblock dupmap cfg isfst pc1 b1 (Some pc2) -> - match_iblock dupmap cfg false pc2 b2 opc -> - match_iblock dupmap cfg isfst pc1 (Bseq b1 b2) opc -(* | mib_seq_None isfst b1 b2 pc: - match_iblock dupmap cfg isfst pc b1 None -> - match_iblock dupmap cfg isfst (Bseq b1 b2) pc None - (* TODO: here [b2] is dead code ! Is this case really useful ? - The oracle could remove this dead code. - And the verifier could fail if there is such dead code! - *) -*) - | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i iinfo: - cfg!pc = Some (Icond c lr pcso pcnot i) -> - match_iblock dupmap cfg false pcso bso opc1 -> - match_iblock dupmap cfg false pcnot bnot opc2 -> - is_join_opt opc1 opc2 opc -> - match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot iinfo) opc - . - -Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop := - forall pc pc', dupmap!pc = Some pc' -> - exists ib, cfg!pc = Some ib /\ match_iblock dupmap cfg' true pc' ib.(entry) None. - -(** Shared verifier between RTL -> BTL and BTL -> RTL *) - -Local Open Scope error_monad_scope. - -Definition verify_is_copy dupmap n n' := - match dupmap!n with - | None => Error(msg "BTL.verify_is_copy None") - | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "BTL.verify_is_copy invalid map") end - end. - -Fixpoint verify_is_copy_list dupmap ln ln' := - match ln with - | n::ln => match ln' with - | n'::ln' => do _ <- verify_is_copy dupmap n n'; - verify_is_copy_list dupmap ln ln' - | nil => Error (msg "BTL.verify_is_copy_list: ln' bigger than ln") end - | nil => match ln' with - | n :: ln' => Error (msg "BTL.verify_is_copy_list: ln bigger than ln'") - | nil => OK tt end - end. - -Lemma verify_is_copy_correct dupmap n n' tt: - verify_is_copy dupmap n n' = OK tt -> - dupmap ! n = Some n'. -Proof. - unfold verify_is_copy; repeat autodestruct. - intros NP H; destruct (_ ! n) eqn:REVM; [|inversion H]. - eapply Pos.compare_eq in NP. congruence. -Qed. -Local Hint Resolve verify_is_copy_correct: core. - -Lemma verify_is_copy_list_correct dupmap ln: forall ln' tt, - verify_is_copy_list dupmap ln ln' = OK tt -> - list_forall2 (fun n n' => dupmap ! n = Some n') ln ln'. -Proof. - induction ln. - - intros. destruct ln'; monadInv H. constructor. - - intros. destruct ln'; monadInv H. constructor; eauto. -Qed. - -(* TODO Copied from duplicate, should we import ? *) -Lemma product_eq {A B: Type} : - (forall (a b: A), {a=b} + {a<>b}) -> - (forall (c d: B), {c=d} + {c<>d}) -> - forall (x y: A+B), {x=y} + {x<>y}. -Proof. - intros H H'. intros. decide equality. -Qed. - -(* TODO Copied from duplicate, should we import ? *) -(** FIXME Ideally i would like to put this in AST.v but i get an "illegal application" - * error when doing so *) -Remark builtin_arg_eq_pos: forall (a b: builtin_arg positive), {a=b} + {a<>b}. -Proof. - intros. - apply (builtin_arg_eq Pos.eq_dec). -Defined. -Global Opaque builtin_arg_eq_pos. - -(* TODO Copied from duplicate, should we import ? *) -Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}. -Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed. -Global Opaque builtin_res_eq_pos. - -Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) := - match ib with - | BF fi _ => - match fi with - | Bgoto pc1 => - do u <- verify_is_copy dupmap pc1 pc; - if negb isfst then - OK None - else Error (msg "BTL.verify_block: isfst is true Bgoto") - | Breturn or => - match cfg!pc with - | Some (Ireturn or') => - if option_eq Pos.eq_dec or or' then OK None - else Error (msg "BTL.verify_block: different opt reg in Breturn") - | _ => Error (msg "BTL.verify_block: incorrect cfg Breturn") - end - | Bcall s ri lr r pc1 => - match cfg!pc with - | Some (Icall s' ri' lr' r' pc2) => - do u <- verify_is_copy dupmap pc1 pc2; - if (signature_eq s s') then - if (product_eq Pos.eq_dec ident_eq ri ri') then - if (list_eq_dec Pos.eq_dec lr lr') then - if (Pos.eq_dec r r') then OK None - else Error (msg "BTL.verify_block: different r r' in Bcall") - else Error (msg "BTL.verify_block: different lr in Bcall") - else Error (msg "BTL.verify_block: different ri in Bcall") - else Error (msg "BTL.verify_block: different signatures in Bcall") - | _ => Error (msg "BTL.verify_block: incorrect cfg Bcall") - end - | Btailcall s ri lr => - match cfg!pc with - | Some (Itailcall s' ri' lr') => - if (signature_eq s s') then - if (product_eq Pos.eq_dec ident_eq ri ri') then - if (list_eq_dec Pos.eq_dec lr lr') then OK None - else Error (msg "BTL.verify_block: different lr in Btailcall") - else Error (msg "BTL.verify_block: different ri in Btailcall") - else Error (msg "BTL.verify_block: different signatures in Btailcall") - | _ => Error (msg "BTL.verify_block: incorrect cfg Btailcall") - end - | Bbuiltin ef la br pc1 => - match cfg!pc with - | Some (Ibuiltin ef' la' br' pc2) => - do u <- verify_is_copy dupmap pc1 pc2; - if (external_function_eq ef ef') then - if (list_eq_dec builtin_arg_eq_pos la la') then - if (builtin_res_eq_pos br br') then OK None - else Error (msg "BTL.verify_block: different brr in Bbuiltin") - else Error (msg "BTL.verify_block: different lbar in Bbuiltin") - else Error (msg "BTL.verify_block: different ef in Bbuiltin") - | _ => Error (msg "BTL.verify_block: incorrect cfg Bbuiltin") - end - | Bjumptable r ln => - match cfg!pc with - | Some (Ijumptable r' ln') => - do u <- verify_is_copy_list dupmap ln ln'; - if (Pos.eq_dec r r') then OK None - else Error (msg "BTL.verify_block: different r in Bjumptable") - | _ => Error (msg "BTL.verify_block: incorrect cfg Bjumptable") - end - end - | Bnop oiinfo => - match oiinfo with - | Some _ => - match cfg!pc with - | Some (Inop pc') => OK (Some pc') - | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop") - end - | None => - if negb isfst then OK (Some pc) - else Error (msg "BTL.verify_block: isfst is true Bnop (on_rtl is false)") - end - | Bop op lr r _ => - match cfg!pc with - | Some (Iop op' lr' r' pc') => - if (eq_operation op op') then - if (list_eq_dec Pos.eq_dec lr lr') then - if (Pos.eq_dec r r') then - OK (Some pc') - else Error (msg "BTL.verify_block: different r in Bop") - else Error (msg "BTL.verify_block: different lr in Bop") - else Error (msg "BTL.verify_block: different operations in Bop") - | _ => Error (msg "BTL.verify_block: incorrect cfg Bop") - end - | Bload tm m a lr r _ => - match cfg!pc with - | Some (Iload tm' m' a' lr' r' pc') => - if (trapping_mode_eq tm TRAP && trapping_mode_eq tm' TRAP) then - if (chunk_eq m m') then - if (eq_addressing a a') then - if (list_eq_dec Pos.eq_dec lr lr') then - if (Pos.eq_dec r r') then - OK (Some pc') - else Error (msg "BTL.verify_block: different r in Bload") - else Error (msg "BTL.verify_block: different lr in Bload") - else Error (msg "BTL.verify_block: different addressing in Bload") - else Error (msg "BTL.verify_block: different mchunk in Bload") - else Error (msg "BTL.verify_block: NOTRAP trapping_mode unsupported in Bload") - | _ => Error (msg "BTL.verify_block: incorrect cfg Bload") - end - | Bstore m a lr r _ => - match cfg!pc with - | Some (Istore m' a' lr' r' pc') => - if (chunk_eq m m') then - if (eq_addressing a a') then - if (list_eq_dec Pos.eq_dec lr lr') then - if (Pos.eq_dec r r') then OK (Some pc') - else Error (msg "BTL.verify_block: different r in Bstore") - else Error (msg "BTL.verify_block: different lr in Bstore") - else Error (msg "BTL.verify_block: different addressing in Bstore") - else Error (msg "BTL.verify_block: different mchunk in Bstore") - | _ => Error (msg "BTL.verify_block: incorrect cfg Bstore") - end - | Bseq b1 b2 => - do opc <- verify_block dupmap cfg isfst pc b1; - match opc with - | Some pc' => - verify_block dupmap cfg false pc' b2 - | None => Error (msg "BTL.verify_block: None next pc in Bseq (deadcode)") - end - | Bcond c lr bso bnot _ => - match cfg!pc with - | Some (Icond c' lr' pcso pcnot i') => - if (list_eq_dec Pos.eq_dec lr lr') then - if (eq_condition c c') then - do opc1 <- verify_block dupmap cfg false pcso bso; - do opc2 <- verify_block dupmap cfg false pcnot bnot; - match opc1, opc2 with - | None, o => OK o - | o, None => OK o - | Some x, Some x' => - if Pos.eq_dec x x' then OK (Some x) - else Error (msg "BTL.verify_block: is_join_opt incorrect for Bcond") - end - else Error (msg "BTL.verify_block: incompatible conditions in Bcond") - else Error (msg "BTL.verify_block: different lr in Bcond") - | _ => Error (msg "BTL.verify_block: incorrect cfg Bcond") - end - end. - -(* This property expresses that "relation" [match_iblock] is a partial function (see also [iblock_istep_run_equiv] above) *) -Lemma verify_block_correct dupmap cfg ib: forall pc isfst fin, - verify_block dupmap cfg isfst pc ib = (OK fin) -> match_iblock dupmap cfg isfst pc ib fin. -Proof. - induction ib; intros; - try (unfold verify_block in H; destruct (cfg!pc) eqn:EQCFG; [ idtac | discriminate; fail ]). - - (* BF *) - destruct fi; unfold verify_block in H. - + (* Bgoto *) - monadInv H. - destruct (isfst); simpl in EQ0; inv EQ0. - eapply verify_is_copy_correct in EQ. - constructor; assumption. - + (* Breturn *) - destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. - destruct (option_eq _ _ _); try discriminate. inv H. - eapply mib_BF; eauto. constructor. - + (* Bcall *) - destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. - monadInv H. - eapply verify_is_copy_correct in EQ. - destruct (signature_eq _ _); try discriminate. - destruct (product_eq _ _ _ _); try discriminate. - destruct (list_eq_dec _ _ _); try discriminate. - destruct (Pos.eq_dec _ _); try discriminate. subst. - inv EQ0. eapply mib_BF; eauto. constructor; assumption. - + (* Btailcall *) - destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. - destruct (signature_eq _ _); try discriminate. - destruct (product_eq _ _ _ _); try discriminate. - destruct (list_eq_dec _ _ _); try discriminate. subst. - inv H. eapply mib_BF; eauto. constructor. - + (* Bbuiltin *) - destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. - monadInv H. - eapply verify_is_copy_correct in EQ. - destruct (external_function_eq _ _); try discriminate. - destruct (list_eq_dec _ _ _); try discriminate. - destruct (builtin_res_eq_pos _ _); try discriminate. subst. - inv EQ0. eapply mib_BF; eauto. constructor; assumption. - + (* Bjumptable *) - destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. - monadInv H. - eapply verify_is_copy_list_correct in EQ. - destruct (Pos.eq_dec _ _); try discriminate. subst. - inv EQ0. eapply mib_BF; eauto. constructor; assumption. - - (* Bnop *) - destruct oiinfo; simpl in *. - + destruct (cfg!pc) eqn:EQCFG; try discriminate. - destruct i0; inv H. constructor; assumption. - + destruct isfst; try discriminate. inv H. - constructor; assumption. - - (* Bop *) - destruct i; try discriminate. - destruct (eq_operation _ _); try discriminate. - destruct (list_eq_dec _ _ _); try discriminate. - destruct (Pos.eq_dec _ _); try discriminate. inv H. - constructor; assumption. - - (* Bload *) - destruct i; try discriminate. - do 2 (destruct (trapping_mode_eq _ _); try discriminate). - simpl in H. - destruct (chunk_eq _ _); try discriminate. - destruct (eq_addressing _ _); try discriminate. - destruct (list_eq_dec _ _ _); try discriminate. - destruct (Pos.eq_dec _ _); try discriminate. inv H. - constructor; assumption. - - (* Bstore *) - destruct i; try discriminate. - destruct (chunk_eq _ _); try discriminate. - destruct (eq_addressing _ _); try discriminate. - destruct (list_eq_dec _ _ _); try discriminate. - destruct (Pos.eq_dec _ _); try discriminate. inv H. - constructor; assumption. - - (* Bseq *) - monadInv H. - destruct x; try discriminate. - eapply mib_seq_Some. - eapply IHib1; eauto. - eapply IHib2; eauto. - - (* Bcond *) - destruct i; try discriminate. - destruct (list_eq_dec _ _ _); try discriminate. - destruct (eq_condition _ _); try discriminate. - fold (verify_block dupmap cfg false n ib1) in H. - fold (verify_block dupmap cfg false n0 ib2) in H. - monadInv H. - destruct x, x0; try destruct (Pos.eq_dec _ _); try discriminate. - all: inv EQ2; eapply mib_cond; eauto; econstructor. -Qed. -Local Hint Resolve verify_block_correct: core. - -Fixpoint verify_blocks dupmap (cfg: code) (cfg':RTL.code) l: res unit := - match l with - | nil => OK tt - | (pc, pc')::l => - match cfg!pc with - | Some ib => do o <- verify_block dupmap cfg' true pc' ib.(entry); - match o with - | None => verify_blocks dupmap cfg cfg' l - | _ => Error(msg "BTL.verify_blocks.end") - end - | _ => Error(msg "BTL.verify_blocks.entry") - end - end. -Definition verify_cfg dupmap (cfg: code) (cfg':RTL.code): res unit := - verify_blocks dupmap cfg cfg' (PTree.elements dupmap). - -Lemma verify_cfg_correct dupmap cfg cfg' tt: - verify_cfg dupmap cfg cfg' = OK tt -> - match_cfg dupmap cfg cfg'. -Proof. - unfold verify_cfg. - intros X pc pc' H; generalize X; clear X. - exploit PTree.elements_correct; eauto. - generalize tt pc pc' H; clear tt pc pc' H. - generalize (PTree.elements dupmap). - induction l as [|[pc1 pc1']l]; simpl. - - tauto. - - intros pc pc' DUP u H. - unfold bind. - repeat autodestruct. - intros; subst. - destruct H as [H|H]; eauto. - inversion H; subst. - eexists; split; eauto. -Qed. - -Definition verify_function dupmap f f' : res unit := - do _ <- verify_is_copy dupmap (fn_entrypoint f) (RTL.fn_entrypoint f'); - verify_cfg dupmap (fn_code f) (RTL.fn_code f'). +(** * Auxiliary general purpose functions on BTL *) Definition is_goto (ib: iblock): bool := match ib with | BF (Bgoto _) _ => true | _ => false end. + -- cgit From b063fb03af84483671833d40491f4fa8d2c8b4c9 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 23 Jul 2021 18:25:00 +0200 Subject: non trapping loads --- scheduling/BTL.v | 51 ++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 38 insertions(+), 13 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 6536addb..96377943 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -205,7 +205,7 @@ Definition find_function (ros: reg + ident) (rs: regset) : option fundef := Local Open Scope option_monad_scope. -(* (* TODO: a new (hopefully simpler) scheme to support "NOTRAP" wrt current scheme of RTL *) +(* TODO: a new (hopefully simpler) scheme to support "NOTRAP" wrt current scheme of RTL *) Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop := | has_loaded_normal a trap @@ -217,11 +217,10 @@ Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop := (DEFAULT: v = default_notrap_load_value chunk) : has_loaded sp rs m chunk addr args v NOTRAP . +Local Hint Constructors has_loaded: core. (* TODO: move this scheme in "Memory" module if this scheme is useful ! *) -*) - (** internal big-step execution of one iblock *) Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop := | exec_final rs m fin iinfo: iblock_istep sp rs m (BF fin iinfo) rs m (Some fin) @@ -229,15 +228,9 @@ Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option fi | exec_op rs m op args res v iinfo (EVAL: eval_operation ge sp op rs##args m = Some v) : iblock_istep sp rs m (Bop op args res iinfo) (rs#res <- v) m None - | exec_load_TRAP rs m chunk addr args dst a v iinfo - (EVAL: eval_addressing ge sp addr rs##args = Some a) - (LOAD: Mem.loadv chunk m a = Some v) - : iblock_istep sp rs m (Bload TRAP chunk addr args dst iinfo) (rs#dst <- v) m None -(* TODO: replace [exec_load_TRAP] above by this one. See "new scheme" for "NOTRAP" above - | exec_load rs m trap chunk addr args dst v + | exec_load rs m trap chunk addr args dst v iinfo (LOAD: has_loaded sp rs m chunk addr args v trap) - : iblock_istep sp rs m (Bload trap chunk addr args dst) (rs#dst <- v) m None -*) + : iblock_istep sp rs m (Bload trap chunk addr args dst iinfo) (rs#dst <- v) m None | exec_store rs m chunk addr args src a m' iinfo (EVAL: eval_addressing ge sp addr rs##args = Some a) (STORE: Mem.storev chunk m a rs#src = Some m') @@ -274,7 +267,18 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome := SOME v <- Mem.loadv chunk m a IN Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} | Bload NOTRAP chunk addr args dst _ => - None (* TODO *) + match eval_addressing ge sp addr rs##args with + | Some a => + match Mem.loadv chunk m a with + | Some v => Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} + | None => + let v := default_notrap_load_value chunk in + Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} + end + | None => + let v := default_notrap_load_value chunk in + Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} + end | Bstore chunk addr args src _ => SOME a <- eval_addressing ge sp addr rs##args IN SOME m' <- Mem.storev chunk m a rs#src IN @@ -291,13 +295,34 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome := iblock_istep_run sp (if b then ifso else ifnot) rs m end. +Lemma iblock_istep_run_equiv_load sp ib v rs rs' m trap chunk addr args dst iinfo ofin: + ib = (Bload trap chunk addr args dst iinfo) -> + rs' = rs # dst <- v -> + has_loaded sp rs m chunk addr args v trap -> + iblock_istep sp rs m ib rs' m ofin <-> + iblock_istep_run sp ib rs m = Some {| _rs := rs'; _m := m; _fin := ofin |}. +Proof. + split; subst; inv H1; simpl in *; intros. + - destruct trap; inv H; simpl in *; repeat autodestruct. + - inv H; autodestruct; rewrite LOAD; auto. + - destruct trap; inv H; simpl in *; + rewrite EVAL, LOAD in H1; inv H1; repeat econstructor; eauto. + - generalize H; autodestruct. + + rewrite LOAD in *; inv H; auto; constructor. + eapply has_loaded_default; eauto; try_simplify_someHyps. + + inv H; constructor. eapply has_loaded_default; eauto; try_simplify_someHyps. +Qed. +Local Hint Resolve iblock_istep_run_equiv_load: core. + Lemma iblock_istep_run_equiv sp rs m ib rs' m' ofin: iblock_istep sp rs m ib rs' m' ofin <-> iblock_istep_run sp ib rs m = Some {| _rs := rs'; _m:= m'; _fin := ofin |}. Proof. constructor. - - induction 1; simpl; try autodestruct; try_simplify_someHyps. + - induction 1; try (eapply iblock_istep_run_equiv_load; eauto; fail); + simpl; try autodestruct; try_simplify_someHyps. - generalize rs m rs' m' ofin; clear rs m rs' m' ofin. induction ib; simpl; repeat (try autodestruct; try_simplify_someHyps). + 1,2: constructor; eapply has_loaded_default; try_simplify_someHyps. destruct o; try_simplify_someHyps; subst; eauto. Qed. -- cgit