diff --git a/compiler/src/arch_full.ml b/compiler/src/arch_full.ml index 3d8785aad..799b4d524 100644 --- a/compiler/src/arch_full.ml +++ b/compiler/src/arch_full.ml @@ -4,9 +4,14 @@ open Arch_extra open Prog type 'a callstyle = - | StackDirect (* call instruction push the return address on top of the stack *) - | ByReg of 'a option (* call instruction store the return address on a register, - (Some r) neams that the register is forced to be r *) + | StackDirect + (* call instruction push the return address on top of the stack *) + | ByReg of { call : 'a option; return : bool } + (* call instruction store the return address on a register, + - call: (Some r) means that the register is forced to be r + - return: + + true means that the register is also used for the return + + false means that there is no constraint (stack is also ok) *) (* TODO: check that we cannot use sth already defined on the Coq side *) @@ -191,7 +196,7 @@ module Arch_from_Core_arch (A : Core_arch) : let callstyle = match A.callstyle with | StackDirect -> StackDirect - | ByReg o -> ByReg (Option.map var_of_reg o) + | ByReg { call; return } -> ByReg { call = Option.map var_of_reg call; return } let arch_info = Pretyping.{ pd = reg_size; diff --git a/compiler/src/arch_full.mli b/compiler/src/arch_full.mli index d9ce086f8..c9ef78f55 100644 --- a/compiler/src/arch_full.mli +++ b/compiler/src/arch_full.mli @@ -3,9 +3,15 @@ open Arch_extra open Prog type 'a callstyle = - | StackDirect (* call instruction push the return address on top of the stack *) - | ByReg of 'a option (* call instruction store the return address on a register, - (Some r) neams that the register is forced to be r *) + | StackDirect + (* call instruction push the return address on top of the stack *) + | ByReg of { call : 'a option; return : bool } + (* call instruction store the return address on a register, + - call: (Some r) means that the register is forced to be r + - return: + + true means that the register is also used for the return + + false means that there is no constraint (stack is also ok) *) + (* x86 : StackDirect arm v7 : ByReg (Some ra) riscV : ByReg (can it be StackDirect too ?) diff --git a/compiler/src/arm_arch_full.ml b/compiler/src/arm_arch_full.ml index 3ffe72b3e..4a2f0f2d4 100644 --- a/compiler/src/arm_arch_full.ml +++ b/compiler/src/arm_arch_full.ml @@ -115,5 +115,5 @@ module Arm (Lowering_params : Arm_input) : Arch_full.Core_arch = struct let pp_asm = Pp_arm_m4.print_prog - let callstyle = Arch_full.ByReg (Some LR) + let callstyle = Arch_full.ByReg { call = Some LR; return = false } end diff --git a/compiler/src/pp_riscv.ml b/compiler/src/pp_riscv.ml index 267389066..b9595aed0 100644 --- a/compiler/src/pp_riscv.ml +++ b/compiler/src/pp_riscv.ml @@ -173,13 +173,11 @@ let pp_instr fn i = [ LInstr ("j", [ pp_remote_label lbl ]) ] | JMPI arg -> - (* TODO_RISCV: Review. *) - let lbl = - match arg with - | Reg r -> pp_register r - | _ -> failwith "TODO_RISCV: pp_instr jmpi" - in - [ LInstr ("jr", [ lbl ]) ] + begin match arg with + | Reg RA -> [LInstr ("ret", [])] + | Reg r -> [ LInstr ("jr", [ pp_register r ]) ] + | _ -> failwith "TODO_RISCV: pp_instr jmpi" + end | Jcc (lbl, ct) -> let iname = pp_condition_kind ct.cond_kind in @@ -187,19 +185,13 @@ let pp_instr fn i = let cond_snd = pp_cond_arg ct.cond_snd in [ LInstr (iname, [ cond_fst; cond_snd; pp_label fn lbl ]) ] - | CALL lbl -> - [LInstr ("call", [pp_remote_label lbl])] - - | JAL (reg, lbl) -> - begin match reg with - | RA -> [LInstr ("call", [pp_remote_label lbl] )] - | _ -> [LInstr ("jalr", [pp_register reg; pp_remote_label lbl] )] - end + | JAL (RA, lbl) -> + [LInstr ("call", [pp_remote_label lbl])] - | POPPC -> - [ LInstr ("lw", [ pp_register RA; pp_reg_address_aux (pp_register SP) None None None]); - LInstr ("addi", [ pp_register SP; pp_register SP; "4"]); - LInstr ("ret", [ ]) ] + | JAL _ + | CALL _ + | POPPC -> + assert false | SysCall op -> [LInstr ("call", [ pp_syscall op ])] @@ -240,11 +232,21 @@ let pp_fun (fn, fd) = else [] in let pre = let fn = escape fn in - if fd.asm_fd_export then [ LLabel (mangle fn); LLabel fn; LInstr ("addi", [ pp_register SP; pp_register SP; "-4"]); LInstr ("sw", [ pp_register RA; pp_reg_address_aux (pp_register SP) None None None])] else [] + if fd.asm_fd_export then + [ LLabel (mangle fn); + LLabel fn; + LInstr ("addi", [ pp_register SP; pp_register SP; "-4"]); + LInstr ("sw", [ pp_register RA; pp_reg_address_aux (pp_register SP) None None None])] + else [] in let body = pp_body fn fd.asm_fd_body in - (* TODO_RISCV: Review. *) - let pos = if fd.asm_fd_export then pp_instr fn POPPC else [] in + let pos = + if fd.asm_fd_export then + [ LInstr ("lw", [ pp_register RA; pp_reg_address_aux (pp_register SP) None None None]); + LInstr ("addi", [ pp_register SP; pp_register SP; "4"]); + LInstr ("ret", [ ]) ] + else [] + in head @ pre @ body @ pos let pp_funcs funs = List.concat_map pp_fun funs diff --git a/compiler/src/printer.ml b/compiler/src/printer.ml index 23b8cf69b..f6b105b61 100644 --- a/compiler/src/printer.ml +++ b/compiler/src/printer.ml @@ -375,14 +375,22 @@ let pp_saved_stack ~debug fmt = function let pp_tmp_option ~debug = Format.pp_print_option (fun fmt x -> Format.fprintf fmt " [tmp = %a]" (pp_var ~debug) (Conv.var_of_cvar x)) +let pp_ra_call ~debug = + Format.pp_print_option (fun fmt ra_call -> Format.fprintf fmt "%a -> " (pp_var ~debug) (Conv.var_of_cvar ra_call)) + +let pp_ra_return ~debug = + Format.pp_print_option (fun fmt ra_return -> Format.fprintf fmt " -> %a" (pp_var ~debug) (Conv.var_of_cvar ra_return)) + let pp_return_address ~debug fmt = function | Expr.RAreg (x, o) -> Format.fprintf fmt "%a%a" (pp_var ~debug) (Conv.var_of_cvar x) (pp_tmp_option ~debug) o - | Expr.RAstack(Some x, z, o) -> - Format.fprintf fmt "%a, RSP + %a%a" (pp_var ~debug) (Conv.var_of_cvar x) Z.pp_print (Conv.z_of_cz z) (pp_tmp_option ~debug) o - | Expr.RAstack(None, z, o) -> - Format.fprintf fmt "RSP + %a%a" Z.pp_print (Conv.z_of_cz z) (pp_tmp_option ~debug) o + | Expr.RAstack(ra_call, ra_return, z, o) -> + Format.fprintf fmt "%aRSP + %a%a%a" + (pp_ra_call ~debug) ra_call Z.pp_print (Conv.z_of_cz z) + (pp_tmp_option ~debug) o + (pp_ra_return ~debug) ra_return + | Expr.RAnone -> Format.fprintf fmt "_" let pp_sprog ~debug pd asmOp fmt ((funcs, p_extra):('info, 'asm) Prog.sprog) = diff --git a/compiler/src/regalloc.ml b/compiler/src/regalloc.ml index 68822dee7..80d9032b1 100644 --- a/compiler/src/regalloc.ml +++ b/compiler/src/regalloc.ml @@ -454,21 +454,36 @@ let collect_variables_cb ~(allvars: bool) (excluded: Sv.t) (fresh: unit -> int) let n = fresh () in Hv.add tbl v n -let collect_variables_aux ~(allvars: bool) (excluded: Sv.t) (fresh: unit -> int) (tbl: int Hv.t) (extra: var option) (f: ('info, 'asm) func) : unit = +let collect_variables_aux ~(allvars: bool) (excluded: Sv.t) (fresh: unit -> int) (tbl: int Hv.t) (extra: Sv.t) (f: ('info, 'asm) func) : unit = let get v = collect_variables_cb ~allvars excluded fresh tbl v in iter_variables get f; - match extra with Some x -> get x | None -> () + Sv.iter get extra let collect_variables ~(allvars: bool) (excluded:Sv.t) (f: ('info, 'asm) func) : int Hv.t * int = let fresh, total = make_counter () in let tbl : int Hv.t = Hv.create 97 in - collect_variables_aux ~allvars excluded fresh tbl None f; + collect_variables_aux ~allvars excluded fresh tbl Sv.empty f; tbl, total () +(* TODO: should StackDirect be just StackByReg (None, None, None)? *) type retaddr = | StackDirect - | StackByReg of var * var option + (* ra is passed on the stack and read from the stack *) + | StackByReg of var * var option * var option + (* StackByReg (ra_call, ra_return, tmp) *) | ByReg of var * var option + (* ByReg (ra, tmp) *) + +let vars_retaddr ra = + let oadd ov s = + match ov with + | None -> s + | Some v -> Sv.add v s + in + match ra with + | StackByReg (ra_call, ra_return, tmp) -> oadd tmp (oadd ra_return (Sv.singleton ra_call)) + | ByReg (ra, tmp) -> oadd tmp (Sv.singleton ra) + | StackDirect -> Sv.empty let collect_variables_in_prog ~(allvars: bool) @@ -479,12 +494,8 @@ let collect_variables_in_prog let fresh, total = make_counter () in let tbl : int Hv.t = Hv.create 97 in List.iter (fun f -> - let extra, tmp = - match Hf.find return_adresses f.f_name with - | StackByReg (v, tmp) | ByReg (v, tmp) -> Some v, tmp - | StackDirect -> None, None in - collect_variables_aux ~allvars excluded fresh tbl extra f; - Option.may (collect_variables_cb ~allvars excluded fresh tbl) tmp) f; + let extra = vars_retaddr (Hf.find return_adresses f.f_name) in + collect_variables_aux ~allvars excluded fresh tbl extra f) f; List.iter (collect_variables_cb ~allvars excluded fresh tbl) all_reg; tbl, total () @@ -694,10 +705,27 @@ let allocate_forced_registers return_addresses translate_var nv (vars: int Hv.t) if FInfo.is_export f.f_cc then alloc_args loc identity f.f_args; if FInfo.is_export f.f_cc then alloc_ret loc L.unloc f.f_ret; alloc_stmt f.f_body; - match Hf.find return_addresses f.f_name, Arch.callstyle with - | (StackByReg (ra,_) | ByReg (ra, _)), Arch_full.ByReg (Some r) -> + match Arch.callstyle with + | Arch_full.ByReg { call = Some r; return } -> + begin match Hf.find return_addresses f.f_name with + | StackDirect -> () + | StackByReg (ra_call, ra_return, _) -> + let i = Hv.find vars ra_call in + allocate_one nv vars (Location.i_loc f.f_loc []) cnf ra_call i r a; + if return then begin + match ra_return with + | Some ra_return -> + let i = Hv.find vars ra_return in + allocate_one nv vars (Location.i_loc f.f_loc []) cnf ra_return i r a + | None -> + (* calling convention requires the return address to be in a register, + but there is no booked register. This must not happen. *) + assert false + end + | ByReg (ra, _) -> let i = Hv.find vars ra in allocate_one nv vars (Location.i_loc f.f_loc []) cnf ra i r a + end | _ -> () (* Returns a variable from [regs] that is allocated to a friend variable of [i]. Defaults to [dflt]. *) @@ -943,7 +971,7 @@ let subroutine_ra_by_stack f = | Subroutine _ -> match Arch.callstyle with | Arch_full.StackDirect -> true - | Arch_full.ByReg oreg -> + | Arch_full.ByReg { call = oreg } -> let dfl = oreg <> None && has_call_or_syscall f.f_body in match f.f_annot.retaddr_kind with | None -> dfl @@ -1108,7 +1136,7 @@ let global_allocation translate_var get_internal_size (funcs: ('info, 'asm) func let preprocess f = let f = f |> fill_in_missing_names |> Ssa.split_live_ranges false in Hf.add liveness_table f.f_name (Liveness.live_fd true f); - (* compute where will be store the return address *) + (* compute where the return address will be stored *) let ra = match f.f_cc with | Export _ -> StackDirect @@ -1116,7 +1144,7 @@ let global_allocation translate_var get_internal_size (funcs: ('info, 'asm) func | Subroutine _ -> match Arch.callstyle with | Arch_full.StackDirect -> StackDirect - | Arch_full.ByReg oreg -> + | Arch_full.ByReg { call = oreg; return } -> let dfl = oreg <> None && has_call_or_syscall f.f_body in let r = V.mk ("ra_"^f.f_name.fn_name) (Reg(Normal,Direct)) (tu Arch.reg_size) f.f_loc [] in (* Fixme: Add an option in Arch to say when the tmp reg is needed *) @@ -1130,7 +1158,14 @@ let global_allocation translate_var get_internal_size (funcs: ('info, 'asm) func match f.f_annot.retaddr_kind with | None -> dfl | Some k -> dfl || k = OnStack in - if rastack then StackByReg (r, tmp) + if rastack then + let r_return = + if return then + let r_return = V.mk ("ra_"^f.f_name.fn_name) (Reg(Normal,Direct)) (tu Arch.reg_size) f.f_loc [] in + Some r_return + else None + in + StackByReg (r, r_return, tmp) else ByReg (r, tmp) in Hf.add return_addresses f.f_name ra; let written = @@ -1139,10 +1174,7 @@ let global_allocation translate_var get_internal_size (funcs: ('info, 'asm) func match f.f_cc with | (Export _ | Internal) -> written | Subroutine _ -> - match ra with - | StackDirect -> written - | StackByReg (r, None) | ByReg (r, None) -> Sv.add r written - | StackByReg (r, Some t) | ByReg (r, Some t) -> Sv.add t (Sv.add r written) + Sv.union (vars_retaddr ra) written in let killed_by_calls = Mf.fold (fun fn _locs acc -> Sv.union (killed fn) acc) @@ -1217,14 +1249,32 @@ let global_allocation translate_var get_internal_size (funcs: ('info, 'asm) func List.fold_left (fun cnf x -> conflicts_add_one Arch.pointer_data Arch.reg_size Arch.asmOp vars tr Lnone ra x cnf) in List.fold_left (fun a f -> match Hf.find return_addresses f.f_name with - | ByReg (ra, None) | StackByReg(ra,None) -> - doit ra a f.f_args - | ByReg (ra, Some tmp) | StackByReg(ra,Some tmp) -> + | StackDirect -> a + | StackByReg (ra_call, ra_return, tmp) -> + (* ra_call conflicts with function arguments *) + let a = doit ra_call a f.f_args in + let a = + match ra_return with + | Some ra_return -> + (* ra_return conflicts with function results *) + doit ra_return a (List.map L.unloc f.f_ret) + | None -> a + in + begin match tmp with + | Some tmp -> + (* tmp register used to increment the stack conflicts with function arguments and results *) + let a = doit tmp a f.f_args in + doit tmp a (List.map L.unloc f.f_ret) + | None -> a + end + | ByReg (ra, tmp) -> let a = doit ra a f.f_args in - (* tmp register used to increment the stack conflicts with function arguments and results *) - let a = doit tmp a f.f_args in - doit tmp a (List.map L.unloc f.f_ret) - | StackDirect -> a) + match tmp with + | Some tmp -> + (* tmp register used to increment the stack conflicts with function arguments and results *) + let a = doit tmp a f.f_args in + doit tmp a (List.map L.unloc f.f_ret) + | None -> a) conflicts funcs in (* Inter-procedural conflicts *) let conflicts = @@ -1304,7 +1354,8 @@ let alloc_prog translate_var (has_stack: ('info, 'asm) func -> 'a -> bool) get_i let ro_return_address = match Hf.find return_addresses f.f_name with | StackDirect -> StackDirect - | StackByReg(r, tmp) -> StackByReg (subst r, Option.map subst tmp) + | StackByReg(ra_call, ra_return, tmp) -> + StackByReg (subst ra_call, Option.map subst ra_return, Option.map subst tmp) | ByReg(r, tmp) -> ByReg (subst r, Option.map subst tmp) in let ro_to_save = if FInfo.is_export f.f_cc then Sv.elements to_save else [] in e, { ro_to_save ; ro_rsp ; ro_return_address }, f diff --git a/compiler/src/regalloc.mli b/compiler/src/regalloc.mli index c1c82a466..ec2d9c21f 100644 --- a/compiler/src/regalloc.mli +++ b/compiler/src/regalloc.mli @@ -4,7 +4,7 @@ val fill_in_missing_names : ('info, 'asm) Prog.func -> ('info, 'asm) Prog.func type retaddr = | StackDirect - | StackByReg of var * var option + | StackByReg of var * var option * var option | ByReg of var * var option type reg_oracle_t = { diff --git a/compiler/src/riscv_arch_full.ml b/compiler/src/riscv_arch_full.ml index a1ed2be6f..fde3e93d6 100644 --- a/compiler/src/riscv_arch_full.ml +++ b/compiler/src/riscv_arch_full.ml @@ -51,5 +51,5 @@ module Riscv (Lowering_params : Riscv_input) : Arch_full.Core_arch = struct let pp_asm = Pp_riscv.print_prog - let callstyle = Arch_full.ByReg (Some RA) + let callstyle = Arch_full.ByReg { call = Some RA; return = true } end diff --git a/compiler/src/stackAlloc.ml b/compiler/src/stackAlloc.ml index 24f9fdb1b..f2c43c67b 100644 --- a/compiler/src/stackAlloc.ml +++ b/compiler/src/stackAlloc.ml @@ -319,7 +319,7 @@ let memory_analysis pp_err ~debug up = sao_rsp = saved_stack; sao_return_address = (* This is a dummy value it will be fixed in fix_csao *) - RAstack (None, Conv.cz_of_int 0, None) + RAstack (None, None, Conv.cz_of_int 0, None) } in Hf.replace atbl fn csao in @@ -339,8 +339,9 @@ let memory_analysis pp_err ~debug up = Stack_alloc.{ csao with sao_return_address = match ro.ro_return_address with - | StackDirect -> RAstack (None, Conv.cz_of_int 0, None) (* FIXME stackDirect should provide a tmp register *) - | StackByReg (r, tmp) -> RAstack (Some (Conv.cvar_of_var r), Conv.cz_of_int 0, Option.map Conv.cvar_of_var tmp) + | StackDirect -> RAstack (None, None, Conv.cz_of_int 0, None) (* FIXME stackDirect should provide a tmp register *) + | StackByReg (ra_call, ra_return, tmp) -> + RAstack (Some (Conv.cvar_of_var ra_call), Option.map Conv.cvar_of_var ra_return, Conv.cz_of_int 0, Option.map Conv.cvar_of_var tmp) | ByReg (r, tmp) -> RAreg (Conv.cvar_of_var r, Option.map Conv.cvar_of_var tmp) } in Hf.replace atbl fn csao diff --git a/compiler/src/varalloc.ml b/compiler/src/varalloc.ml index a3b8b1a76..67fd3425e 100644 --- a/compiler/src/varalloc.ml +++ b/compiler/src/varalloc.ml @@ -396,13 +396,13 @@ let alloc_stack_fd callstyle pd get_info gtbl fd = false (* For export function ra is not counted in the frame *) | Subroutine _ -> match callstyle with - | Arch_full.StackDirect -> + | Arch_full.StackDirect -> if fd.f_annot.retaddr_kind = Some OnReg then Utils.warning Always (L.i_loc fd.f_loc []) "for function %s, return address by reg not allowed for that architecture, annotation is ignored" fd.f_name.fn_name; true - | Arch_full.ByReg oreg -> (* oreg = Some r implies that all call use r, + | Arch_full.ByReg { call = oreg } -> (* oreg = Some r implies that all call use r, so if the function performs some call r will be overwritten, so ra need to be saved on stack *) let dfl = oreg <> None && has_call_or_syscall fd.f_body in diff --git a/proofs/compiler/arm_params.v b/proofs/compiler/arm_params.v index 9b666c337..4ffe1cafd 100644 --- a/proofs/compiler/arm_params.v +++ b/proofs/compiler/arm_params.v @@ -144,6 +144,7 @@ Definition arm_liparams : linearization_params := lip_lmove := arm_lmove; lip_check_ws := arm_check_ws; lip_lstore := arm_lstore; + lip_lload := arm_lload; lip_lstores := lstores_imm_dfl arm_tmp2 arm_lstore ARMFopn.smart_addi is_arith_small; lip_lloads := lloads_imm_dfl arm_tmp2 arm_lload ARMFopn.smart_addi is_arith_small; |}. diff --git a/proofs/compiler/arm_params_proof.v b/proofs/compiler/arm_params_proof.v index a1b09b3db..fc585c1bf 100644 --- a/proofs/compiler/arm_params_proof.v +++ b/proofs/compiler/arm_params_proof.v @@ -264,9 +264,8 @@ Qed. Lemma arm_lload_correct : lload_correct_aux (lip_check_ws arm_liparams) arm_lload. Proof. - move=> xd xs ofs s vm top hgets. - case heq: vtype => [|||ws] //; t_xrbindP. - move=> _ <- /eqP ? w hread hset; subst ws. + move=> xd xs ofs ws top s w vm heq hcheck hgets hread hset. + move/eqP: hcheck => ?; subst ws. rewrite /arm_lload /= hgets /= truncate_word_u /= hread /=. by rewrite /exec_sopn /= truncate_word_u /= zero_extend_u hset. Qed. @@ -294,6 +293,7 @@ Definition arm_hliparams : spec_lip_set_up_sp_register := arm_spec_lip_set_up_sp_register; spec_lip_lmove := arm_lmove_correct; spec_lip_lstore := arm_lstore_correct; + spec_lip_lload := arm_lload_correct; spec_lip_lstores := arm_lstores_correct; spec_lip_lloads := arm_lloads_correct; spec_lip_tmp := arm_tmp_correct; diff --git a/proofs/compiler/linearization.v b/proofs/compiler/linearization.v index 4e17e601a..731bc875e 100644 --- a/proofs/compiler/linearization.v +++ b/proofs/compiler/linearization.v @@ -71,7 +71,8 @@ Record linearization_params {asm_op : Type} {asmop : asmOp asm_op} := lip_tmp2 : Ident.ident; (* Variables that can't be used to save the stack pointer. - If lip_set_up_sp_register use its auxiliary argument, it should contain lip_tmp + If lip_set_up_sp_register uses its auxiliary argument, + it should contain lip_tmp. *) lip_not_saved_stack : seq Ident.ident; @@ -117,25 +118,25 @@ Record linearization_params {asm_op : Type} {asmop : asmOp asm_op} := -> seq fopn_args; (* Return the arguments for a linear instruction that corresponds to - an assignment. - In symbols, the linear instruction derived from [lip_lmove d s] + a move between two registers. + In symbols, the linear instruction derived from [lip_lmove xd xs] corresponds to: - d := (Uptr)s + xd := (Uptr)xs *) lip_lmove : var_i (* Destination variable. *) -> var_i (* Source variable. *) -> fopn_args; - (* Check it the give size can be write/read to/from memory, + (* Check if the given size can be written to/read from memory, i.e if an operation exists for that size. *) lip_check_ws : wsize -> bool; (* Return the arguments for a linear instruction that corresponds to - an assignment. - In symbols, the linear instruction derived from [lip_lstore b ofs xs] + a store to memory. + In symbols, the linear instruction derived from [lip_lstore xd ofs xs] corresponds to: - [b + ofs] := (Uptr) s + [xd + ofs] := xs *) lip_lstore : var_i (* Base register. *) @@ -143,6 +144,18 @@ Record linearization_params {asm_op : Type} {asmop : asmOp asm_op} := -> var_i (* Source register. *) -> fopn_args; + (* Return the arguments for a linear instruction that corresponds to + a load from memory. + In symbols, the linear instruction derived from [lip_lload xd xs ofs] + corresponds to: + xd = [xs + ofs] + *) + lip_lload : + var_i (* Destination register. *) + -> var_i (* Base register. *) + -> Z (* Offset. *) + -> fopn_args; + (* Push variables to the stack at the given offset *) lip_lstores : var_i (* The current stack pointer *) @@ -165,7 +178,7 @@ Record linearization_params {asm_op : Type} {asmop : asmOp asm_op} := LstoreLabel ra lret Lgoto lcall Llabel lret - Internally (to the callee), ra need to be free. + Internally (to the callee), ra needs to be free. The return is implemented by Ligoto ra /!\ For protection against Spectre we should avoid this calling convention @@ -181,29 +194,58 @@ Record linearization_params {asm_op : Type} {asmop : asmOp asm_op} := + For ARM v7: - Return address passed by register in ra - Lcall (Some ra) lcall (i.e BL lcall with the constraint that ra should be LR(r14)) + Lcall (Some ra) lcall (i.e BL lcall with the constraint that ra should be LR (r14)) Llabel lret - Internally (to the callee), ra need to be free. + Internally (to the callee), ra needs to be free. The return is implemented by Ligoto ra (i.e BX ra) The stack frame is incremented by the caller. - Return address passed by stack (on top of the stack): - Lcall (Some ra) lcall (i.e BL lcall with the constraint that ra should be LR(r14)) - Llabel lret - ra need to be free when Lcall is executed (extra_free_registers = Some ra). - The first instruction of the function call need to push ra. - store sp ra - So ra need to be known at call cite and at the entry of the function. + Lcall (Some ra) lcall (i.e BL lcall with the constraint that ra should be LR (r14)) + Llabel lret + ra needs to be free when Lcall is executed. + The first instruction of the function call needs to push ra. + store sp ra + So ra needs to be known at call site and at the entry of the function. The stack frame is incremented by the caller. The return is implemented by - Lret (i.e POP PC in arm v7) + Lret (i.e POP PC in arm v7) + + + + For RISC-V: + + - Return address passed by register in r + Lcall (Some r) lcall (i.e call lcall with the constraint that r should be ra (x1)) + Llabel lret + Internally (to the callee), r needs to be free. + The return is implemented by + Ligoto r (i.e jr r, also written ret if r is ra) + The stack frame is incremented by the caller. + + - Return address passed by stack (on top of the stack): + Lcall (Some ra_call) lcall (i.e call lcall with the constraint that ra_call should be ra (x1)) + Llabel lret + ra_call needs to be free when Lcall is executed. + The first instruction of the function call needs to push ra_call. + store sp ra_call + So ra_call needs to be known at call site and at the entry of the function. + The stack frame is incremented by the caller. + The return is implemented by + load ra_return sp + Ligoto ra_return (i.e. jr ra_return, also written ret if ra_return is ra) + ra_return needs to be free at the end of the callee (in particular, it cannot + be a result). *) -(* The following functions are defined here, so that they can be shared between the architectures. The proofs are shared too (see linearization_proof.v). An architecture can define its own functions when there is something more efficient to do, and rely on one of these implementations in the default case. *) +(* The following functions are defined here, so that they can be shared between + the architectures. The proofs are shared too (see linearization_proof.v). + + An architecture can define its own functions when there is something more + efficient to do, and rely on one of these implementations in the default case. *) Section DEFAULT. Context {asm_op : Type} {pd : PointerData} {asmop : asmOp asm_op}. Context (lip_tmp2 : Ident.ident). @@ -251,7 +293,7 @@ Context (liparams : linearization_params). (* Return a linear instruction that corresponds to copying a register. - The linear instruction [lmove ii rd rs] corresponds to + The linear instruction [lmove rd rs] corresponds to R[rd] := (Uptr)R[rs] *) Definition lmove @@ -261,13 +303,19 @@ Definition lmove li_of_fopn_args dummy_instr_info (lip_lmove liparams rd rs). (* Return a linear instruction that corresponds to loading from memory. - The linear instruction [lload ii rd ws r0 ofs] corresponds to - R[rd] := (ws)M[R[r0] + ofs] + The linear instruction [lload rd rs ofs] corresponds to + R[rd] := M[R[rs] + ofs] *) +Definition lload + (rd : var_i) (* Destination register. *) + (rs : var_i) (* Base register. *) + (ofs : Z) (* Offset. *) + : linstr := + li_of_fopn_args dummy_instr_info (lip_lload liparams rd rs ofs). (* Return a linear instruction that corresponds to storing to memory. - The linear instruction [lstore ii rd ofs ws rs] corresponds to - M[R[rd] + ofs] := (ws)R[rs] + The linear instruction [lstore rd ofs rs] corresponds to + M[R[rd] + ofs] := R[rs] *) Definition lstore (rd : var_i) (* Base register. *) @@ -309,7 +357,7 @@ End EXPR. Definition ovar_of_ra (ra : return_address_location) : option var := match ra with | RAreg ra _ => Some ra - | RAstack ra _ _ => ra + | RAstack ra_call _ _ _ => ra_call | RAnone => None end. @@ -319,7 +367,7 @@ Definition ovari_of_ra (ra : return_address_location) : option var_i := Definition tmp_of_ra (ra : return_address_location) : option var := match ra with | RAreg _ o => o - | RAstack _ _ o => o + | RAstack _ _ _ o => o | RAnone => None end. @@ -528,10 +576,10 @@ Definition check_fd (fn: funname) (fd:sfundef) := Let _ := assert match sf_return_address e with | RAnone => ~~ (var_tmp2 \in map v_var fd.(f_res)) | RAreg ra tmp => (vtype ra == sword Uptr) && ov_type_ptr tmp - | RAstack ora ofs tmp => - [&& ov_type_ptr tmp - , (if ora is Some ra then vtype ra == sword Uptr - else true) + | RAstack ra_call ra_return ofs tmp => + [&& ov_type_ptr ra_call + , ov_type_ptr ra_return + , ov_type_ptr tmp & check_stack_ofs_internal_call e ofs Uptr] end (E.error "bad return-address") in @@ -581,6 +629,12 @@ Definition allocate_stack_frame (free: bool) (ii: instr_info) (sz: Z) (tmp: opti else (lip_allocate_stack_frame liparams) rspi tmp sz in map (li_of_fopn_args ii) args. +Definition is_RAstack_None_call ra := + if ra is RAstack None _ _ _ then true else false. + +Definition is_RAstack_None_return ra := + if ra is RAstack _ None _ _ then true else false. + Let ReturnTarget := Llabel ExternalLabel. Let Llabel := linear.Llabel InternalLabel. @@ -655,8 +709,8 @@ Fixpoint linear_i (i:instr) (lbl:label) (lc:lcmd) := else let sz := stack_frame_allocation_size e in let tmp := tmpi_of_ra ra in - let before := allocate_stack_frame false ii sz tmp (is_RAstack_None ra) in - let after := allocate_stack_frame true ii sz tmp (is_RAstack ra) in + let before := allocate_stack_frame false ii sz tmp (is_RAstack_None_call ra) in + let after := allocate_stack_frame true ii sz tmp (is_RAstack_None_return ra) in let lret := lbl in let lbl := next_lbl lbl in (* The test is used for the proof of linear_has_valid_labels *) @@ -688,11 +742,14 @@ Definition linear_body (e: stk_fun_extra) (body: cmd) : label * lcmd := , [:: MkLI dummy_instr_info (Llabel 1) ] , 2%positive ) - | RAstack ra z _ => - ( [:: MkLI dummy_instr_info Lret ] + | RAstack ra_call ra_return z _ => + ( if ra_return is Some ra_return + then [:: lload (mk_var_i ra_return) rspi z; + MkLI dummy_instr_info (Ligoto (Rexpr (Fvar (mk_var_i ra_return)))) ] + else [:: MkLI dummy_instr_info Lret ] , MkLI dummy_instr_info (Llabel 1) :: - (if ra is Some ra - then [:: lstore rspi z (mk_var_i ra) ] + (if ra_call is Some ra_call + then [:: lstore rspi z (mk_var_i ra_call) ] else [::]) , 2%positive ) diff --git a/proofs/compiler/linearization_proof.v b/proofs/compiler/linearization_proof.v index fd03d3a47..87af55f0b 100644 --- a/proofs/compiler/linearization_proof.v +++ b/proofs/compiler/linearization_proof.v @@ -183,7 +183,7 @@ Section CAT. Proof. move=> xs fn es ii fn' lbl tail /=. case: get_fundef => // fd; case: is_RAnoneP => //. - by case: sf_return_address => // [ ra ? | ra ra_ofs ? ] _; rewrite cats0 -catA. + by case: sf_return_address => // [ ra ? | ra_call ra_return ra_ofs ? ] _; rewrite cats0 -catA. Qed. Lemma linear_i_nil fn i lbl tail : @@ -415,6 +415,17 @@ Definition lstore_correct_aux lip_check_ws lip_lstore := Definition lstore_correct := lstore_correct_aux (lip_check_ws liparams) (lip_lstore liparams). +Definition lload_correct_aux lip_check_ws lip_lload := + forall (xd xs : var_i) ofs ws wp s w vm, + vtype xd = sword ws -> + lip_check_ws ws -> + (get_var true (evm s) xs >>= to_word Uptr) = ok wp -> + read (emem s) Aligned (wp + wrepr Uptr ofs)%R ws = ok w -> + set_var true (evm s) xd (Vword w) = ok vm -> + sem_fopn_args (lip_lload xd xs ofs) s = ok (with_vm s vm). + +Definition lload_correct := lload_correct_aux (lip_check_ws liparams) (lip_lload liparams). + Definition set_up_sp_register_correct := forall vrsp r tmp ts al sz s, let: ts' := align_word al (ts - wrepr Uptr sz) in @@ -485,6 +496,7 @@ Record h_linearization_params := spec_lip_set_up_sp_register : set_up_sp_register_correct; spec_lip_lmove : lmove_correct; spec_lip_lstore : lstore_correct; + spec_lip_lload : lload_correct; spec_lip_lstores : lstores_correct; spec_lip_lloads : lloads_correct; spec_lip_tmp : lip_tmp liparams <> lip_tmp2 liparams; @@ -514,16 +526,7 @@ Context (lip_check_ws : wsize -> bool) Context (lstore_correct : lstore_correct_aux lip_check_ws lip_lstore). -Definition lload_correct_aux := - forall (xd xs : var_i) ofs s vm top, - get_var true (evm s) xs >>= to_word Uptr = ok top -> - (Let: ws := if vtype xd is sword ws then ok ws else Error ErrType in - Let _ := assert (lip_check_ws ws) ErrType in - Let w := read (emem s) Aligned (top + wrepr Uptr ofs)%R ws in - set_var true (evm s) xd (Vword w)) = ok vm -> - sem_fopn_args (lip_lload xd xs ofs) s = ok (with_vm s vm). - -Context (lload_correct : lload_correct_aux). +Context (lload_correct : lload_correct_aux lip_check_ws lip_lload). Definition ladd_imm_correct_aux := forall (x1 x2:var_i) s (w: word Uptr) ofs, @@ -609,8 +612,7 @@ Proof. move=> [x ofs] to_restore ih s /= hnin hget. case heqt: vtype => [|||ws] //=; t_xrbindP. move=> vm1 hchk w hread hset hf. - have /(_ ofs vm1) := lload_correct (xd:= VarI x dummy_var_info) hget. - rewrite heqt /= hchk /= hread /= hset => -> //=. + rewrite (lload_correct (xd := VarI x dummy_var_info) heqt hchk hget hread hset). apply: ih => //. + by move: hnin; rewrite in_cons negb_or => /andP []. rewrite -(get_var_eq_ex _ _ (set_var_eq_ex hset)) //. @@ -626,8 +628,11 @@ Proof. move=> vm2' hchk w hread hset ?; subst vm2'. have [+ hget2]:= lloads_aux_correct hnin hget hf. rewrite /lloads_aux map_cat sem_fopns_args_cat => -> /=. - have /(_ ofs vm2):= lload_correct (xd:= VarI rspi dummy_var_info) (s:= with_vm s vm1) hget2. - by rewrite heqt /= hchk /= hread /= => /(_ hset) -> /=; exists vm2. + rewrite + (lload_correct + (xd := VarI rspi dummy_var_info) (s:= with_vm s vm1) + heqt hchk hget2 hread hset). + by exists vm2. Qed. Lemma lloads_imm_dfl_correct : @@ -702,13 +707,27 @@ Section HLIPARAMS. let: li := lstore liparams x ofs y in eval_instr lp li ls = ok (lnext_pc (lset_mem ls m)). Proof. - move=> hty hgy htr hgx hw /=; rewrite -(lset_estate_same ls). + move=> hty hgy htr hgx hw /=. apply sem_fopn_args_eval_instr => /=. - rewrite (spec_lip_lstore hliparams (s:= to_estate ls) hty (spec_lip_check_ws hliparams) _ _ hw) //. + apply: (spec_lip_lstore hliparams (s:= to_estate ls) hty (spec_lip_check_ws hliparams) _ _ hw). + by rewrite hgx /= truncate_word_u. by rewrite hgy /= htr. Qed. + Lemma spec_lload {lp ls ofs} {x y:var_i} {wx wy} : + vtype x = sword Uptr -> + get_var true (lvm ls) y = ok (Vword wy) -> + read (lmem ls) Aligned (wy + wrepr Uptr ofs)%R Uptr = ok wx -> + let: li := lload liparams x y ofs in + eval_instr lp li ls = ok (lnext_pc (lset_vm ls ls.(lvm).[x <- Vword wx])). + Proof. + move=> hty hgy hread /=. + apply sem_fopn_args_eval_instr => /=. + apply: (spec_lip_lload hliparams (s:= to_estate ls) hty (spec_lip_check_ws hliparams) _ hread). + + by rewrite hgy /= truncate_word_u. + by apply set_var_eq_type. + Qed. + Lemma set_up_sp_register_ok lp sp_rsp ls r tmp ts al sz P Q : let: vrspi := vid sp_rsp in let: vrsp := v_var vrspi in @@ -1078,7 +1097,7 @@ Section NUMBER_OF_LABELS. suff: (Z.of_nat (size (label_in_lcmd head)) + Z.of_nat (size (label_in_lcmd tail)) <= lbl0)%Z by lia. move: h. - case: sf_return_address => [|x _|ra z _]. + case: sf_return_address => [|x _| ra_call ra_return z _]. + case: sf_save_stack => [|x|z] [<- <- <-] //=. + by rewrite set_up_sp_register_label_in_lcmd. @@ -1087,7 +1106,9 @@ Section NUMBER_OF_LABELS. by rewrite label_in_lcmd_push_to_save label_in_lcmd_pop_to_save /=. + by move=> [<- <- <-] /=. - by move=> [<- <- <-] /=; case: ra => //= r; case: get_label. + + move=> [<- <- <-] /=. + by case: ra_call ra_return => [?|] [?|] //. Qed. End NUMBER_OF_LABELS. @@ -1605,7 +1626,7 @@ Section PROOF. is_align (top_stack m) e.(sf_align) ∧ let sz := stack_frame_allocation_size e in ptr = (top_stack m - wrepr Uptr sz)%R. - (* Define where/how the return address is pass by the caller to the callee *) + (* Define where/how the return address is passed by the caller to the callee *) Definition value_of_ra (m: mem) (vm: Vm.t) @@ -1614,29 +1635,25 @@ Section PROOF. : Prop := match ra, target with | RAnone, None => True - | RAreg (Var (sword ws) _ as ra) _, Some ((caller, lbl), cbody, pc) => - if (ws == Uptr)%CMP - then [/\ is_linear_of caller cbody, - find_label lbl cbody = ok pc, - (caller, lbl) \in label_in_lprog p' & - exists2 ptr, - encode_label (label_in_lprog p') (caller, lbl) = Some ptr & - vm.[ra] = Vword (zero_extend ws ptr) - ] - else False - - | RAstack (Some (Var (sword ws) _ as ra)) _ _ , Some ((caller, lbl), cbody, pc) => - if (ws == Uptr)%CMP - then [/\ is_linear_of caller cbody, - find_label lbl cbody = ok pc, - (caller, lbl) \in label_in_lprog p' & - exists2 ptr, - encode_label (label_in_lprog p') (caller, lbl) = Some ptr & - vm.[ra] = Vword (zero_extend ws ptr) - ] - else False - - | RAstack None ofs _, Some ((caller, lbl), cbody, pc) => + | RAreg ra _, Some ((caller, lbl), cbody, pc) => + [/\ is_linear_of caller cbody, + find_label lbl cbody = ok pc, + (caller, lbl) \in label_in_lprog p' & + exists2 ptr, + encode_label (label_in_lprog p') (caller, lbl) = Some ptr & + vm.[ra] = Vword ptr + ] + + | RAstack (Some ra) _ _ _ , Some ((caller, lbl), cbody, pc) => + [/\ is_linear_of caller cbody, + find_label lbl cbody = ok pc, + (caller, lbl) \in label_in_lprog p' & + exists2 ptr, + encode_label (label_in_lprog p') (caller, lbl) = Some ptr & + vm.[ra] = Vword ptr + ] + + | RAstack None _ ofs _, Some ((caller, lbl), cbody, pc) => [/\ is_linear_of caller cbody, find_label lbl cbody = ok pc, (caller, lbl) \in label_in_lprog p' & @@ -1644,7 +1661,6 @@ Section PROOF. exists2 sp, vm.[ vrsp ] = Vword sp & read m Aligned (sp + wrepr Uptr ofs)%R Uptr = ok ptr ] - | _, _ => False end. @@ -1973,7 +1989,7 @@ Section PROOF. match ra with | RAnone => var_tmps | RAreg x _ => Sv.singleton x - | RAstack or _ _ => sv_of_option or + | RAstack or _ _ _ => sv_of_option or end. (* The set of variable killed/written by the execution of the function, @@ -1983,7 +1999,7 @@ Section PROOF. match ra with | RAnone => Sv.diff killed saved | RAreg _ _ => killed - | RAstack _ _ _ => Sv.add vrsp killed + | RAstack _ _ _ _ => Sv.add vrsp killed end. (* The set of variable written by the execution of the exit code of function *) @@ -1992,12 +2008,12 @@ Section PROOF. match ra with | RAnone => Sv.add var_tmp2 saved | RAreg _ _ => saved - | RAstack _ _ _ => saved + | RAstack _ _ _ _ => saved end. Definition sp_alloc_ra (sp : word Uptr) (ra : return_address_location) : word Uptr := - if is_RAstack ra then (sp + wrepr _ (wsize_size Uptr))%R else sp. + if is_RAstack_None_return ra then (sp + wrepr _ (wsize_size Uptr))%R else sp. Let Pfun (ii: instr_info) (k: Sv.t) (s1: estate) (fn: funname) (s2: estate) : Prop := ∀ ls m1 vm1 body ra lret sp callee_saved, @@ -2015,8 +2031,7 @@ Section PROOF. vm_initialized_on vm1 callee_saved → source_mem_split s1 (top_stack (emem s1)) -> max_bound fn (top_stack (emem s1)) -> - (∀ fd, get_fundef (p_funcs p) fn = Some fd -> - if is_RAnone (sf_return_address (f_extra fd)) then m0 = emem s1 else True) -> + (if is_RAnone ra then m0 = emem s1 else True) -> let: ssaved := sv_of_list id callee_saved in exists2_6 m2 vm2, pfun_preserved lret ls (size body) (escs s1) m1 vm1 (escs s2) m2 vm2 @@ -3081,8 +3096,8 @@ Section PROOF. have s1_rsp : (evm s1).[vrsp] = Vword (top_stack (emem s1)). + by move: T; rewrite /valid_RSP /kill_tmp_call /= kill_varsE; case: ifP. move: (s1_rsp); rewrite hsp => -[?]; subst sp. - set rastack_before := is_RAstack_None _. - set rastack_after := is_RAstack _. + set rastack_before := is_RAstack_None_call _. + set rastack_after := is_RAstack_None_return _. set sz := stack_frame_allocation_size _. set sz_before := if rastack_before then (sz - wsize_size Uptr)%Z else sz. set sz_after := if rastack_after then (sz - wsize_size Uptr)%Z else sz. @@ -3091,7 +3106,7 @@ Section PROOF. move: C; set P' := P ++ _ => C. pose Stmp := if tmpi_of_ra (sf_return_address (f_extra fd')) is Some x then Sv.singleton x else Sv.empty. have StmpE : Sv.Equal Stmp (tmp_call (f_extra fd')). - + by rewrite /tmp_call /Stmp /tmpi_of_ra; case: sf_return_address => //= [_ | _ _] []. + + by rewrite /tmp_call /Stmp /tmpi_of_ra; case: sf_return_address => //= [_ | _ _ _] []. move: (X vrsp); rewrite s1_rsp. move=> /get_word_uincl_eq -/(_ (subtype_refl _)) vm2_rsp. have vrsp_ne_aux : @@ -3102,7 +3117,7 @@ Section PROOF. + move: T; rewrite /valid_RSP /kill_tmp_call /= kill_varsE. case: Sv_memP => // + _. rewrite /tmpi_of_ra /fd_tmp_call /tmp_of_ra /tmp_call ok_fd'. - by case: sf_return_address => // [_ | _ _] [?|] //=; SvD.fsetdec. + by case: sf_return_address => // [_ | _ _ _] [?|] //=; SvD.fsetdec. have [vm2_b [hsem_before heqvm2 hvm2_b_rsp]] : exists (vm2_b:Vm.t), [/\ lsem p' (Lstate (escs s1) m1 vm2 fn (size P)) @@ -3117,7 +3132,7 @@ Section PROOF. move=> /(_ (with_mem (with_vm s1 vm2) m1) (top_stack (emem s1))); apply. + case: sf_return_address ok_ret_addr vrsp_ne_aux => //=. + by move=> v [x|] //= /andP [] _ /eqP. - by move=> o z [x|] //= /andP [] /eqP. + by move=> ra_call ra_return z [x|] //= /and5P [_ _ /eqP + _ _]. by rewrite /get_var /with_vm /= vm2_rsp. set ra := sf_return_address (f_extra fd'). @@ -3166,25 +3181,26 @@ Section PROOF. rewrite /ra_valid in ra_sem. rewrite /sz_before /rastack_before in hvm2_b_rsp. rewrite /Stmp in heqvm2. - case eq_ra : sf_return_address ok_ra ok_ret_addr ra_sem hvm2_b_rsp heqvm2 => [ | x | [ x | ] ofs] //= _ + case eq_ra : sf_return_address ok_ra ok_ret_addr ra_sem hvm2_b_rsp heqvm2 => [ | x | [ x | ] ra_return ofs] //= _ ok_ret_addr ra_sem hvm2_b_rsp heqvm2. (* RAreg x _ *) + exists m1, vm2_b.[x <- Vword ptr]; split => //. + by rewrite Vm.setP_neq ?hvm2_b_rsp //; case/and3P : ra_sem. + by move=> /= y hy; rewrite Vm.setP_neq //; apply/eqP; move: hy; clear; SvD.fsetdec. - + case: (x) ok_ret_addr => /= ? vra /andP []/eqP -> _; rewrite eq_refl; split => //. - by rewrite ok_ptr; exists ptr => //; rewrite Vm.setP_eq vm_truncate_val_eq // zero_extend_u. + + move: ok_ret_addr => /andP[] /eqP hty _. + split => //. + by rewrite ok_ptr; exists ptr => //; rewrite Vm.setP_eq vm_truncate_val_eq. by rewrite /= set_var_truncate //=; case/andP: ok_ret_addr => /eqP->. (* RAstack (Some x) ofs _ *) - + case/and5P: ok_ret_addr => _ /eqP ok_ret_addr _ _ _. + + case/and5P: ok_ret_addr => /eqP ok_ret_addr _ _ _ _. exists m1, vm2_b.[x <- Vword ptr]; split => //. - + by rewrite Vm.setP_neq ?hvm2_b_rsp //; case/andP : ra_sem. + + by rewrite Vm.setP_neq ?hvm2_b_rsp //; case/andP : ra_sem => /andP[]. + by move=> /= y hy; rewrite Vm.setP_neq //; apply/eqP; move: hy; clear; SvD.fsetdec. - + case: (x) ok_ret_addr => /= ? vra ->; rewrite eq_refl; split => //. - by rewrite ok_ptr; exists ptr => //; rewrite Vm.setP_eq zero_extend_u vm_truncate_val_eq. + + split => //. + by rewrite ok_ptr; exists ptr => //; rewrite Vm.setP_eq vm_truncate_val_eq. by rewrite /= set_var_truncate //= ok_ret_addr. (* RAstack None ofs _ *) - move: ok_ret_addr => /and4P [] _ /eqP ? /eqP hioff sf_align_for_ptr; subst ofs. + move: ok_ret_addr => /and5P [] _ _ /eqP ? /eqP hioff sf_align_for_ptr; subst ofs. have [m' ok_m' M']: exists2 m1', write m1 Aligned (top_stack_after_alloc (top_stack (emem (kill_tmp_call p fn' s1))) (sf_align (f_extra fd')) (sf_stk_sz (f_extra fd') + sf_stk_extra_sz (f_extra fd')))%R ptr = ok m1' & @@ -3259,7 +3275,7 @@ Section PROOF. + move=> fd''; rewrite ok_fd' => -[?]; subst fd''. rewrite (negbTE ok_ra). by move: (MAX _ ok_fd) => /=; lia. - + by rewrite ok_fd' => _ [<-]; rewrite (negbTE ok_ra). + + by rewrite (negbTE ok_ra). move=> m2' vm2' /= h3 heq_vm hsub_vm' hpres hmatch' U'. set ts := top_stack (M := Memory.M) s1. have vm2'_rsp: @@ -3267,7 +3283,7 @@ Section PROOF. + move: (hsub_vm' vrsp); rewrite /kill_vars /=. rewrite Vm.setP_eq /= cmp_le_refl => /get_word_uincl_eq -/(_ (subtype_refl _)). rewrite /rastack_after /ra. - by case sf_return_address => //= *; rewrite wrepr0 GRing.addr0. + by case sf_return_address => [|??|?[?|//]??] /=; rewrite wrepr0 GRing.addr0. have [vm2'_b [hsem_after heqvm2' hvm2'_b_rsp]] : exists (vm2'_b:Vm.t), [/\ lsem p' (Lstate (escs s2) m2' vm2' fn (size P + size before).+2) @@ -3295,10 +3311,10 @@ Section PROOF. {| li_ii := ii; li_i := linear.Llabel ExternalLabel lbl |}]) ++ after' ++ Q by rewrite -!catA. move => C; have := spec_lip_free_stack_frame_1 hliparams C. move=> /(_ (with_mem (with_vm s2 vm2') m2')). - move=> /(_ (s + wrepr Uptr (if is_RAstack (sf_return_address (f_extra fd')) then wsize_size Uptr else 0%Z))%R) []. + move=> /(_ (s + wrepr Uptr (if is_RAstack_None_return (sf_return_address (f_extra fd')) then wsize_size Uptr else 0%Z))%R) []. + case: sf_return_address ok_ret_addr vrsp_ne_aux => //=. + by move=> v [x|] //= /andP [] _ /eqP. - by move=> ? z [x|] //= /andP [] /eqP. + by move=> ?? z [x|] //= /and5P [_ _ /eqP + _ _]. + by rewrite /get_var /with_vm /= vm2'_rsp. rewrite /= !size_cat /= !addnS addn0 -/after' => vm2'_b [H1 H2 H3]; exists vm2'_b; split => //. rewrite H3 /ts /s /sz; f_equal; case: ifP => _; rewrite ?wrepr_sub ?wrepr0; ssrring.ssring. @@ -3319,24 +3335,28 @@ Section PROOF. rewrite -heqvm2'; last by move: x_notin_k x_neq_rsp; clear; SvD.fsetdec. rewrite -heq_vm; last first. + move: x_notin_k x_neq_rsp; rewrite hk /ra_vm /ra /=; clear. - by case: sf_return_address => [ | r | [ r | ] ?] /=; SvD.fsetdec. + by case: sf_return_address => [ | r ? | [ r | ] ???] /=; SvD.fsetdec. rewrite heqvm2; last by SvD.fsetdec. apply heq_vm'. - move: x_notin_k x_neq_rsp; rewrite hk /ra_vm /ra /=; clear. - by case: sf_return_address => [ | r | [ r | ] ?] /=; SvD.fsetdec. + move: x_notin_k x_neq_rsp; rewrite hk /ra_undef /ra_vm /ra /=; clear. + by case: sf_return_address => [ | r ? | [ r | ] ???] /=; SvD.fsetdec. + have := sem_one_varmap_facts.sem_call_valid_RSP exec_call. rewrite /= /valid_RSP /set_RSP => h x /=. rewrite kill_varsE; case: Sv_memP => [_ | ]. + by apply/compat_value_uincl_undef/Vm.getP. rewrite /fd_tmp_call ok_fd' -StmpE => hnin. have := hsub_vm' x. - rewrite Vm.setP; case: eqP => [? | ]; first by subst x; rewrite h hvm2'_b_rsp. - rewrite kill_varsE; case: Sv_memP => //. - + move: his_ra ok_ra; rewrite /is_ra_of ok_fd' /sv_of_list. - move=> [_ [<-] <-]. - by case: sf_return_address => //=; clear => *; SvD.fsetdec. - move=> _ hne H; apply (value_uincl_trans H). - by rewrite heqvm2' //; move: hnin hne; clear; SvD.fsetdec. + rewrite Vm.setP; case: eqP => [? | hneq]; + first by subst x; rewrite h hvm2'_b_rsp. + rewrite kill_varsE; case: Sv_memP. + + rewrite s2_eq /= Vm.setP_neq; last by apply /eqP. + move: his_ra ok_ra; rewrite /is_ra_of ok_fd'; move=> [_ [<-] <-]. + rewrite kill_varsE; case: Sv_memP. + + by move=> _ _ _ _; apply/compat_value_uincl_undef/Vm.getP. + rewrite /ra_vm_return. + by case: sf_return_address => [|??|????] //=; clear; SvD.fsetdec. + move=> _ H; apply (value_uincl_trans H). + by rewrite heqvm2' //; move: hnin hneq; clear; SvD.fsetdec. + by etransitivity; eauto. + exact hmatch'. by etransitivity; [exact: U | exact: U']. @@ -3723,7 +3743,7 @@ Section PROOF. rewrite /value_of_ra => ok_lret. case; rewrite ok_fd => _ /Some_inj <- /= ok_sp. case; rewrite ok_fd => _ /Some_inj <- /= ok_callee_saved. - move=> wf_to_save S MAX /(_ _ erefl) ok_m0. + move=> wf_to_save S MAX ok_m0. move: (checked_prog ok_fd); rewrite /check_fd /=. t_xrbindP => chk_body ok_to_save ok_stk_sz ok_ret_addr ok_save_stack _. case/and4P: ok_stk_sz => /lezP stk_sz_pos /lezP stk_extra_sz_pos /ltzP frame_noof /lezP stk_frame_le_max. @@ -3737,11 +3757,12 @@ Section PROOF. rewrite /ra_undef_vm in exec_body. rewrite /ra_undef_vm in ih. rewrite /saved_stack_valid in ok_ss. - rewrite /ra_vm. + rewrite /ra_undef /ra_vm. rewrite /saved_stack_vm. case EQ: sf_return_address free_ra ok_to_save ok_callee_saved ok_save_stack ok_ret_addr X ok_lret exec_body ih ok_sp => - /= [ | ra | ora rastack ] free_ra ok_to_save ok_callee_saved ok_save_stack ok_ret_addr X ok_lret exec_body ih. + /= [ | ra ? | ra_call ra_return rastack ? ] + free_ra ok_to_save ok_callee_saved ok_save_stack ok_ret_addr X ok_lret exec_body ih. 2-3: case => sp_aligned. all: move => ?; subst sp. - (* Export function *) @@ -3814,7 +3835,9 @@ Section PROOF. move => x; move: (X2 x); rewrite /set_RSP !Vm.setP kill_varsE Vm.setP. case: eqP => ?; subst. + by rewrite valid_rsp' -(ss_top_stack SS) top_stack_preserved vm_truncate_val_eq. - case: Sv.mem => // _. + case: Sv.mem. + + by move=> _; apply compat_value_uincl_undef; apply Vm.getP. + rewrite kill_varsE; case: Sv.mem => // _. by apply compat_value_uincl_undef; apply Vm.getP. } + (* RSP is saved into register “saved_rsp” *) @@ -3931,8 +3954,10 @@ Section PROOF. + rewrite to_save_empty Sv_diff_empty. clear - ok_rsp K2 hvm. move => x. - rewrite !Sv.union_spec !Sv.add_spec Sv.singleton_spec Vm.setP. - move=> /Decidable.not_or[] x_not_k /Decidable.not_or[] /Decidable.not_or[] x_not_tmp x_not_flags x_not_saved_stack. + rewrite !Sv.union_spec !Sv.add_spec !Sv.singleton_spec Vm.setP. + move=> /Decidable.not_or[] x_not_k + /Decidable.not_or[] /Decidable.not_or[] /Decidable.not_or[] + x_not_tmp x_not_flags x_not_saved_stack _. case: eqP => x_rsp. * by subst; move/get_varP: ok_rsp => [<-]; rewrite vm_truncate_val_eq. rewrite -K2; last exact: x_not_k. @@ -3942,7 +3967,9 @@ Section PROOF. * by subst; rewrite Vm.setP_eq. rewrite Vm.setP_neq; last by apply /eqP. rewrite /set_RSP Vm.setP_neq; last by apply/eqP. - case: Sv.mem => //. + case: Sv.mem. + + by apply compat_value_uincl_undef; apply Vm.getP. + rewrite kill_varsE; case: Sv.mem => //. by apply compat_value_uincl_undef; apply Vm.getP. + move => a [] a_lo a_hi /negbTE nv. have /= [L H] := ass_above_limit A. @@ -4265,7 +4292,7 @@ Section PROOF. by rewrite hxty => ? []. rewrite !SvP.union_mem Sv_mem_add SvP.empty_mem SvP.MP.singleton_equal_add. rewrite Sv_mem_add SvP.empty_mem !orbA !orbF -!orbA. - case/norP => x_ni_k /norP[] x_neq_tmp2 /norP[] x_neq_tmp x_not_flag. + case/norP => x_ni_k /norP[] x_neq_tmp2 /norP[] x_neq_tmp /norP[] x_not_flag _. rewrite (negbTE x_neq_tmp2). case: eqP => heq. + by subst x; rewrite vrsp_to_save; move/get_varP: ok_rsp => -[<- _ _]. @@ -4285,7 +4312,9 @@ Section PROOF. case: eqP. + by move=> ?; subst x; apply compat_value_uincl_undef; apply Vm.getP. move/eqP/negbTE: x_rsp; rewrite eq_sym => -> _ /=. - case: ifP => // hin. + case: ifP => _. + + by apply compat_value_uincl_undef; apply Vm.getP. + rewrite kill_varsE; case: Sv.mem => //. by apply compat_value_uincl_undef; apply Vm.getP. + etransitivity; [exact: H3 | ]. exact: preserved_metadata_alloc ok_m1' H4. @@ -4294,11 +4323,8 @@ Section PROOF. } } - (* Internal function, return address in register “ra” *) - { case: ra EQ ok_ret_addr X free_ra ok_lret exec_body ih => // -[] // ws // ra EQ ra_well_typed X /andP[] _ ra_notin_k. - case: lret => // - [] [] [] caller lret cbody pc. - case: (ws =P Uptr) => // E. - subst ws. - move=> [] ok_cbody ok_pc mem_lret [] retptr ok_retptr ok_ra exec_body ih. + { case: lret ok_lret => // - [] [] [] caller lret cbody pc. + move=> [] ok_cbody ok_pc mem_lret [] retptr ok_retptr ok_ra. have {ih} := ih fn 2%positive. rewrite /checked_c ok_fd chk_body => /(_ erefl). rewrite (linear_c_nil _ _ _ _ _ [:: _ ]). @@ -4362,19 +4388,21 @@ Section PROOF. rewrite catA in ok_body. apply: (eval_lsem1 ok_body) => //. rewrite /eval_instr /= /get_var /=. - have ra_not_written : vm2.[ Var spointer ra ] = vm1.[ Var spointer ra ]. + have ra_not_written : vm2.[ra] = vm1.[ra]. * symmetry; apply: K2. - have /andP [_ ?] := ra_notin_k. + have /and3P [_ _ ?] := free_ra. by apply/Sv_memP. - rewrite ra_not_written ok_ra /= zero_extend_u truncate_word_u. + rewrite ra_not_written ok_ra /= truncate_word_u. have := decode_encode_label small_dom_p' mem_lret. rewrite ok_retptr /rdecode_label /= => -> /=. rewrite (eval_jumpE ok_cbody) ok_pc /=. reflexivity. + apply: eq_exI K2. exact: SvP.MP.union_subset_1. - subst callee_saved; rewrite /kill_vars /=. - move => ?; rewrite /set_RSP !Vm.setP; case: eqP => // ?. + subst callee_saved; rewrite {1}/kill_vars /=. + move => ?; rewrite /set_RSP !Vm.setP; case: eqP => ?; last first. + + rewrite kill_varsE; case: Sv.mem => //. + by apply/compat_value_uincl_undef/Vm.getP. subst; move: (ok_vm2 vrsp). have SS : stack_stable m1' s2'. + exact: sem_one_varmap_facts.sem_stack_stable exec_body. @@ -4385,35 +4413,70 @@ Section PROOF. } (* Internal function, return address in stack at offset “rastack” *) { - case : ora EQ X free_ra ok_ret_addr ok_lret => [ra | ] /= EQ X free_ra ok_ret_addr ok_lret. - (* Initially path by register and stored on top of the stack, like for ARM *) - (* TODO : this case and the next one duplicate proof, we should do lemma *) - + case: ra EQ X free_ra ok_ret_addr ok_lret => // -[] // ws ra EQ X free_ra ok_ret_addr ok_lret. - case: lret ok_lret => // -[] [] [] caller lret cbody pc. - case: eqP => // ?; subst ws => - [] ok_cbody ok_pc mem_lret [] retptr ok_retptr ok_ra1. - have {ih} := ih fn 2%positive. - rewrite /checked_c ok_fd chk_body => /(_ erefl). - rewrite (linear_c_nil _ _ _ _ _ [:: _ ]). - case: (linear_c fn) (valid_c fn (f_body fd) 2%positive) => lbl lbody ok_lbl /= E. - set P1 := (P in P :: _ :: lbody ++ _). - set P2 := (P in _ :: P :: lbody ++ _). - set Q := (Q in P1 :: P2 :: lbody ++ Q). - move => ok_fd'. - have ok_body : is_linear_of fn ([:: P1; P2 ] ++ lbody ++ Q). - + by rewrite /is_linear_of ok_fd'; eauto. - have := X vrsp; rewrite Vm.setP_eq /= cmp_le_refl. - move=> /get_word_uincl_eq -/(_ (subtype_refl _)). - set rsp := (X in Vword X) => ok_rsp. - case/and5P: ok_ret_addr => _ _ /eqP ? /eqP hioff sf_align_for_ptr; subst rastack. - have spec_m1' := alloc_stackP ok_m1'. - have is_align_m1' := ass_align_stk spec_m1'. - have ts_rsp : top_stack m1' = rsp. - + rewrite (alloc_stack_top_stack ok_m1') top_stack_after_aligned_alloc; last by exact: sp_aligned. - by rewrite wrepr_opp -/(stack_frame_allocation_size fd.(f_extra)). - have := ass_align_stk spec_m1'. + have {ih} := ih fn 2%positive. + rewrite /checked_c ok_fd chk_body => /(_ erefl). + rewrite (linear_c_nil _ _ _ _ _ (if _ is Some _ then _ else _)). + case: (linear_c fn) => lbl lbody /= E. + set P1 := (P in P :: _ ++ lbody ++ _). + set P2 := (P in _ :: P ++ lbody ++ _). + set Q := (Q in P1 :: P2 ++ lbody ++ Q). + move => ok_fd'. + have ok_body : is_linear_of fn ((P1 :: P2) ++ lbody ++ Q). + + by rewrite /is_linear_of ok_fd'; eauto. + have := X vrsp; rewrite Vm.setP_eq /= cmp_le_refl. + move=> /get_word_uincl_eq -/(_ (subtype_refl _)). + set rsp := (X in Vword X) => ok_rsp. + case/and5P: ok_ret_addr => + ra_call_ty ra_return_ty _ /eqP ? /andP[] /eqP hioff sf_align_for_ptr; subst rastack. + have spec_m1' := alloc_stackP ok_m1'. + have is_align_m1' := ass_align_stk spec_m1'. + have ts_rsp : top_stack m1' = rsp. + + rewrite (alloc_stack_top_stack ok_m1') top_stack_after_aligned_alloc; last by exact: sp_aligned. + by rewrite wrepr_opp -/(stack_frame_allocation_size fd.(f_extra)). + + (* We factor out what we know thanks to value_of_ra. *) + have {ok_lret} [caller [{}lret [cbody [pc [retptr [-> /= ok_cbody ok_pc mem_lret ok_retptr ok_ra]]]]]]: + exists caller lret' cbody pc retptr, [/\ + lret = Some ((caller, lret'), cbody, pc), + is_linear_of caller cbody, + find_label lret' cbody = ok pc, + (caller, lret') \in label_in_lprog p', + encode_label (label_in_lprog p') (caller, lret') = Some retptr & + match ra_call with + | Some ra_call => vm1.[ra_call] = Vword retptr + | None => read m1 Aligned rsp Uptr = ok retptr + end]. + + case: (ra_call) lret ok_lret => [ra|] [[[[caller lret] cbody] pc]|] //. + + move=> [ok_cbody ok_pc mem_lret [retptr ok_retptr ok_ra]]. + by exists caller, lret, cbody, pc, retptr; split. + move=> [ok_cbody ok_pc mem_lret [retptr ok_retptr ok_ra]]. + exists caller, lret, cbody, pc, retptr; split=> //. + move: ok_ra; rewrite ok_rsp => -[_ [<-] +]. + by rewrite wrepr0 GRing.addr0. + + (* Initial code that stores the return address on top of the stack if it + is passed by register. Else, it is already on top of the stack. + After executing that code, we are in a memory [mi], and the return + address is on top of the stack. *) + have [mi [hsemi hreadi Mi Hi Ui]]: + exists mi, [/\ + lsem p' (setpc (lset_estate ls (escs s1) m1 vm1) 1) + (setpc (lset_estate ls (escs s1) mi vm1) (size (P1 :: P2))), + read mi Aligned rsp Uptr = ok retptr, + match_mem_gen (top_stack m0) s1 mi, + preserved_metadata s1 m1 mi & + target_mem_unchanged m1 mi]. + + case: ra_call EQ ra_call_ty ok_ra {free_ra X} @P2 ok_body {ok_fd'} + => [ra_call|] EQ ra_call_ty ok_ra P2 ok_body; last first. + + (* ra_call = None, easy case: mi = m1 *) + exists m1; split=> //. + exact: rt_refl. + (* ra_call = Some _ *) (* TODO this should be a lemma it is used elsewhere (above)*) have [m1s ok_m1s M']: - exists2 m1s, write m1 Aligned rsp retptr = ok m1s & match_mem_gen (top_stack m0) s1 m1s. + exists2 m1s, + write m1 Aligned rsp retptr = ok m1s & + match_mem_gen (top_stack m0) s1 m1s. + apply: mm_write_invalid. * by have := MAX _ ok_fd; rewrite EQ /=; lia. * exact: M. @@ -4431,119 +4494,25 @@ Section PROOF. move: (stack_frame_allocation_size _) hround frame_noof => SF hround frame_noof. move: (top_stack (emem s1)) => T above_limit. have SF_range : (0 <= SF < wbase Uptr)%Z. - - by move: ( sf_stk_sz (f_extra fd)) (sf_stk_extra_sz (f_extra fd)) stk_sz_pos stk_extra_sz_pos hround; lia. + - by move: (sf_stk_sz (f_extra fd)) (sf_stk_extra_sz (f_extra fd)) stk_sz_pos stk_extra_sz_pos hround; lia. have X : (wunsigned (T - wrepr Uptr SF) <= wunsigned T)%Z. * move: (sf_stk_sz _) stk_sz_pos above_limit => n; lia. have {X} TmS := wunsigned_sub_small SF_range X. rewrite TmS in above_limit. lia. - have X1 : set_RSP p m1' (kill_vars (ra_undef fd var_tmps) s1) <=1 vm1. - + apply: vm_uincl_kill_vars_set_incl X => //. - + by rewrite /ra_undef /ra_vm EQ; SvD.fsetdec. - by rewrite ts_rsp. - have D : disjoint_labels 2 lbl [:: P1; P2]. - + move => q [L H]; rewrite /P1 /P2 /= /is_label /= orbF; apply/eqP; lia. - have hrsp: (set_RSP p m1' (kill_vars (ra_undef fd var_tmps) s1)).[vrsp] = Vword (top_stack m1'). - + by rewrite Vm.setP_eq vm_truncate_val_eq. - have S': source_mem_split m1' (top_stack m1'). - + move=> pr /=. - move=> hvalid; apply /orP; move: hvalid. - rewrite A.(ass_valid). - move=> /orP [/S /orP [hvalid | hpr] | hb]; [by left | right..]. - + apply: pointer_range_incl_l hpr. - by have /= := A.(ass_above_limit); lia. - rewrite pointer_range_between. - apply: zbetween_trans hb. - rewrite /zbetween !zify. - have /= hioff' := A.(ass_ioff). - have /= habove := A.(ass_above_limit). - have hrange1 := [elaborate wunsigned_range (top_stack m1')]. - have hrange2 := [elaborate wunsigned_range (top_stack (emem s1))]. - rewrite wunsigned_add; last by lia. - have := MAX _ ok_fd. - by rewrite EQ /=; lia. - have MAX': max_bound_sub fn (top_stack m1'). - + move=> fd''; rewrite ok_fd => -[?]; subst fd''. - have := MAX _ ok_fd. - rewrite /frame_size EQ /=. - rewrite (wunsigned_top_stack_after_aligned_alloc stk_sz_pos stk_extra_sz_pos frame_noof sp_aligned ok_m1'). - have := stack_frame_allocation_size_bound stk_sz_pos stk_extra_sz_pos. - by lia. - - set ls0 := setpc (lset_estate ls (escs s1) m1 vm1) 2. - have hle: (wunsigned (top_stack (emem s1)) <= wunsigned (top_stack m0))%Z. - + by have := MAX _ ok_fd; rewrite EQ /=; lia. - have {E} [m2 vm2 E K2 ok_vm2 H2 M2 U2] := - E ls0 m1s vm1 [:: P1; P2] Q - (mm_alloc hle M' ok_m1') X1 D ok_body erefl hfn _ hrsp S' MAX'. - exists m2 (vm2.[vrsp <- Vword (rsp + wrepr Uptr (wsize_size Uptr))]). - + apply: (lsem_trans3 _ E). - + apply: (eval_lsem_step1 (pre := [:: P1 ]) ok_body) => //. - apply: (spec_lstore hliparams) => //. - * rewrite /get_var ok_ra1; reflexivity. - * rewrite truncate_word_u; reflexivity. - * rewrite /get_var ok_rsp; reflexivity. - rewrite /= wrepr0 GRing.addr0 zero_extend_u. exact: ok_m1s. - rewrite catA in ok_body. - apply: (eval_lsem_step1 ok_body) => //. - rewrite /eval_instr /= /get_var /=. - move: (ok_vm2 vrsp). - rewrite -(sem_preserved_RSP_GD var_tmps_not_magic exec_body); last exact: RSP_in_magic. - rewrite /= /set_RSP Vm.setP_eq /= lp_rspE -/vrsp cmp_le_refl. - move=> /get_word_uincl_eq -/(_ (subtype_refl _)) -> /=; rewrite truncate_word_u /=. - assert (root_range := wunsigned_range (stack_root m1')). - have top_range := ass_above_limit A. - have top_stackE := wunsigned_top_stack_after_aligned_alloc stk_sz_pos stk_extra_sz_pos frame_noof sp_aligned ok_m1'. - have sf_large : (wsize_size Uptr <= stack_frame_allocation_size (f_extra fd))%Z. - - apply: Z.le_trans; last exact: proj1 (round_ws_range _ _). - have := ass_ioff A. - rewrite -hioff; move: (sf_stk_sz _) (sf_stk_extra_sz _) stk_sz_pos stk_extra_sz_pos; lia. - have rastack_no_overflow : (0 <= wunsigned (top_stack m1'))%Z ∧ (wunsigned (top_stack m1') + wsize_size Uptr <= wunsigned (stack_root m1'))%Z. - * assert (top_stack_range := wunsigned_range (top_stack m1')). - assert (old_top_stack_range := wunsigned_range (top_stack (emem s1))). - assert (h := wsize_size_pos Uptr). - split; first lia. - rewrite (alloc_stack_top_stack ok_m1') top_stack_after_aligned_alloc // wrepr_opp. - rewrite -/(stack_frame_allocation_size _) wunsigned_sub; last first. - - split; last lia. - rewrite top_stackE; move: (stack_frame_allocation_size _) => n; lia. - rewrite A.(ass_root). - etransitivity; last exact: top_stack_below_root. - rewrite -/(top_stack (emem s1)); lia. - have -> : read m2 Aligned (top_stack m1')%R Uptr = read m1s Aligned (top_stack m1')%R Uptr. - * apply: eq_read => al i [] i_lo i_hi; symmetry; rewrite !(read8_alignment Aligned); apply: H2. - - rewrite addE wunsigned_add; lia. - rewrite (Memory.alloc_stackP ok_m1').(ass_valid). - apply/orP; case. - - apply/negP; apply: stack_region_is_free. - rewrite -/(top_stack _). - move: (stack_frame_allocation_size _) top_stackE sf_large => n top_stackE sf_large. - rewrite addE !wunsigned_add; lia. - rewrite !zify (ass_add_ioff A) -hioff addE. - rewrite wunsigned_add; lia. - rewrite ts_rsp (writeP_eq ok_m1s) /=. - have := decode_encode_label small_dom_p' mem_lret. - rewrite ok_retptr /rdecode_label /= => -> /=. - by rewrite (eval_jumpE ok_cbody) ok_pc. - + apply eq_exT with vm2. - + by apply: eq_exI K2; SvD.fsetdec. - by move=> ? hx; rewrite Vm.setP_neq //; apply/eqP; SvD.fsetdec. - + subst callee_saved; rewrite /kill_vars /=. - by move => ?; rewrite /set_RSP !Vm.setP; case: eqP. - + etransitivity. - + apply: (preserved_metadata_store_top_stack ok_m1'); - last by rewrite -hioff; apply Z.le_refl. - by rewrite top_stack_after_aligned_alloc // wrepr_opp; apply: ok_m1s. - move => a [] a_lo a_hi /negbTE nv. - have /= [L R] := ass_above_limit A. - apply: H2. - * by rewrite (ass_root A); lia. - rewrite (ass_valid A) nv /= !zify => - []. - change (wsize_size U8) with 1%Z. - rewrite (ass_add_ioff A). - move: (sf_stk_sz _) (sf_stk_ioff _) (sf_stk_extra_sz _) (ass_ioff A) R; lia. - + exact: mm_free M2. - etransitivity; last exact: U2. + exists m1s; split=> //. + + apply: (eval_lsem_step1 (pre := [:: P1 ]) ok_body) => //. + apply: (spec_lstore hliparams) => /=. + * by move/eqP : ra_call_ty. + * by rewrite /get_var ok_ra; reflexivity. + * by rewrite truncate_word_u; reflexivity. + * by rewrite /get_var ok_rsp; reflexivity. + rewrite wrepr0 GRing.addr0. + exact: ok_m1s. + + exact: (writeP_eq ok_m1s). + + apply: (preserved_metadata_store_top_stack ok_m1'); + last by rewrite -hioff; apply Z.le_refl. + by rewrite top_stack_after_aligned_alloc // wrepr_opp; apply: ok_m1s. (* the frame is inside the stack *) have hb1: zbetween @@ -4564,27 +4533,15 @@ Section PROOF. rewrite hioff /=. by have /= := (alloc_stackP ok_m1').(ass_ioff); lia. by apply (target_mem_unchanged_store hb1 hb2 ok_m1s). - (* Directly path on top of the stack *) - case: lret ok_lret => // - [] [] [] caller lret cbody pc [] ok_cbody ok_pc mem_lret [] retptr ok_retptr [] rsp ok_rsp ok_ra. - have := X vrsp. - rewrite Vm.setP_eq vm_truncate_val_eq // ok_rsp => /andP[] _ /eqP /=. - rewrite zero_extend_u => ?; subst rsp. - have {ih} := ih fn 2%positive. - rewrite /checked_c ok_fd chk_body => /(_ erefl). - rewrite (linear_c_nil _ _ _ _ _ [:: _ ]). - case: (linear_c fn) (valid_c fn (f_body fd) 2%positive) => lbl lbody ok_lbl /= E. - set P := (P in P :: lbody ++ _). - set Q := (Q in P :: lbody ++ Q). - move => ok_fd'. - have ok_body : is_linear_of fn ([:: P ] ++ lbody ++ Q). - + by rewrite /is_linear_of ok_fd'; eauto. + + (* Function body: we rely on the induction hypothesis [E] *) have X1 : set_RSP p m1' (kill_vars (ra_undef fd var_tmps) s1) <=1 vm1. + apply: vm_uincl_kill_vars_set_incl X => //. - + by SvD.fsetdec. - rewrite (alloc_stack_top_stack ok_m1') top_stack_after_aligned_alloc; last by exact: sp_aligned. - by rewrite wrepr_opp -/(stack_frame_allocation_size fd.(f_extra)). - have D : disjoint_labels 2 lbl [:: P]. - + by move => q [L H]; rewrite /P /is_label /= orbF; apply/eqP => ?; subst; lia. + + by rewrite /ra_undef /ra_vm EQ; SvD.fsetdec. + by rewrite ts_rsp. + have D : disjoint_labels 2 lbl (P1 :: P2). + + move => q [L H]; rewrite /P1 /P2 /= /is_label /=. + by case: (ra_call) => [?|] /=; rewrite orbF; apply/eqP; lia. have hrsp: (set_RSP p m1' (kill_vars (ra_undef fd var_tmps) s1)).[vrsp] = Vword (top_stack m1'). + by rewrite Vm.setP_eq vm_truncate_val_eq. have S': source_mem_split m1' (top_stack m1'). @@ -4611,46 +4568,52 @@ Section PROOF. rewrite (wunsigned_top_stack_after_aligned_alloc stk_sz_pos stk_extra_sz_pos frame_noof sp_aligned ok_m1'). have := stack_frame_allocation_size_bound stk_sz_pos stk_extra_sz_pos. by lia. - - set ls0 := setpc (lset_estate ls (escs s1) m1 vm1) 1. + set ls0 := setpc (lset_estate ls (escs s1) m1 vm1) (size (P1 :: P2)). have hle: (wunsigned (top_stack (emem s1)) <= wunsigned (top_stack m0))%Z. + by have := MAX _ ok_fd; rewrite EQ /=; lia. - have {E} [m2 vm2 E K2 ok_vm2 H2 M2 U2] := - E ls0 m1 vm1 [:: P ] Q (mm_alloc hle M ok_m1') X1 D ok_body erefl hfn _ hrsp S' MAX'. - exists m2 (vm2.[vrsp <- Vword - (top_stack (emem s1) - wrepr Uptr (round_ws (sf_align (f_extra fd)) (sf_stk_sz (f_extra fd) + sf_stk_extra_sz (f_extra fd))) + wrepr Uptr (wsize_size Uptr))]); - [ | | | | exact: mm_free M2 | exact: U2 ]. - + apply: (lsem_step_end E). - rewrite catA in ok_body. - apply: (eval_lsem1 ok_body) => //. - rewrite /eval_instr /= /get_var. - move: (ok_vm2 vrsp). - rewrite -(sem_preserved_RSP_GD var_tmps_not_magic exec_body); last exact: RSP_in_magic. - rewrite /= /set_RSP Vm.setP_eq /= lp_rspE -/vrsp cmp_le_refl. - move=> /get_word_uincl_eq -/(_ (subtype_refl _)) -> /=; rewrite truncate_word_u /=. - case/and4P: ok_ret_addr => _ /eqP hrastack /eqP hioff sf_aligned_for_ptr. - assert (root_range := wunsigned_range (stack_root m1')). - have top_range := ass_above_limit A. - have top_stackE := wunsigned_top_stack_after_aligned_alloc stk_sz_pos stk_extra_sz_pos frame_noof sp_aligned ok_m1'. - subst rastack. - have sf_large : (wsize_size Uptr <= stack_frame_allocation_size (f_extra fd))%Z. - - apply: Z.le_trans; last exact: proj1 (round_ws_range _ _). - have := ass_ioff A. - rewrite -hioff; move: (sf_stk_sz _) (sf_stk_extra_sz _) stk_sz_pos stk_extra_sz_pos; lia. - have rastack_no_overflow : (0 <= wunsigned (top_stack m1'))%Z ∧ (wunsigned (top_stack m1') + wsize_size Uptr <= wunsigned (stack_root m1'))%Z. - * assert (top_stack_range := wunsigned_range (top_stack m1')). - assert (old_top_stack_range := wunsigned_range (top_stack (emem s1))). - assert (h := wsize_size_pos Uptr). - split; first lia. - rewrite (alloc_stack_top_stack ok_m1') top_stack_after_aligned_alloc // wrepr_opp. - rewrite -/(stack_frame_allocation_size _) wunsigned_sub; last first. - - split; last lia. - rewrite top_stackE; move: (stack_frame_allocation_size _) => n; lia. - rewrite A.(ass_root). - etransitivity; last exact: top_stack_below_root. - rewrite -/(top_stack (emem s1)); lia. - have -> : read m2 Aligned (top_stack m1')%R Uptr = read m1 Aligned (top_stack m1')%R Uptr. - * apply: eq_read => al i [] i_lo i_hi; symmetry; rewrite !(read8_alignment Aligned); apply: H2. + have [m2 vm2 {}E K2 ok_vm2 H2 M2 U2] := + E ls0 mi vm1 (P1 :: P2) Q + (mm_alloc hle Mi ok_m1') X1 D ok_body erefl hfn _ hrsp S' MAX'. + + (* Final code that jumps back to the return address. The return address + is read directly from the top of the stack (if ra_return = None), + or loaded in ra_return before the jump (if ra_return <> None). + After executing that code, we are in a vmap [vmf], and the value held + in vrsp depends on ra_return. If ra_return = None, the return address + is popped from the stack, so we need to subtract [wsize_size Uptr]. *) + have [vmf hsemf eq_vmf]: + exists2 vmf, + lsem p' (setpc (lset_estate ls (escs s2') m2 vm2) (size ((P1 :: P2) ++ lbody))) + (setcpc (lset_estate ls (escs s2') m2 vmf) caller pc.+1) & + vm2.[vrsp <- Vword (sp_alloc_ra rsp (fd.(f_extra).(sf_return_address)))] + =[\ sv_of_option ra_return] vmf. + + have ok_rsp2: vm2.[vrsp] = Vword rsp. + + have := ok_vm2 vrsp; rewrite valid_rsp'. + move=> /get_word_uincl_eq -/(_ (subtype_refl _)) ->. + have /ss_top_stack /= <- := sem_stack_stable exec_body. + by rewrite ts_rsp. + have hreadf: read m2 Aligned rsp Uptr = read mi Aligned rsp Uptr. + * assert (root_range := wunsigned_range (stack_root m1')). + have top_range := ass_above_limit A. + have top_stackE := wunsigned_top_stack_after_aligned_alloc stk_sz_pos stk_extra_sz_pos frame_noof sp_aligned ok_m1'. + have sf_large : (wsize_size Uptr <= stack_frame_allocation_size (f_extra fd))%Z. + - apply: Z.le_trans; last exact: proj1 (round_ws_range _ _). + have := ass_ioff A. + rewrite -hioff; move: (sf_stk_sz _) (sf_stk_extra_sz _) stk_sz_pos stk_extra_sz_pos; lia. + have rastack_no_overflow : (0 <= wunsigned (top_stack m1'))%Z ∧ (wunsigned (top_stack m1') + wsize_size Uptr <= wunsigned (stack_root m1'))%Z. + * assert (top_stack_range := wunsigned_range (top_stack m1')). + assert (old_top_stack_range := wunsigned_range (top_stack (emem s1))). + assert (h := wsize_size_pos Uptr). + split; first lia. + rewrite (alloc_stack_top_stack ok_m1') top_stack_after_aligned_alloc // wrepr_opp. + rewrite -/(stack_frame_allocation_size _) wunsigned_sub; last first. + - split; last lia. + rewrite top_stackE; move: (stack_frame_allocation_size _) => n; lia. + rewrite A.(ass_root). + etransitivity; last exact: top_stack_below_root. + rewrite -/(top_stack (emem s1)); lia. + rewrite -!ts_rsp. + apply: eq_read => al i [] i_lo i_hi; symmetry; rewrite !(read8_alignment Aligned); apply: H2. - rewrite addE wunsigned_add; lia. rewrite (Memory.alloc_stackP ok_m1').(ass_valid). apply/orP; case. @@ -4660,24 +4623,74 @@ Section PROOF. rewrite addE !wunsigned_add; lia. rewrite !zify (ass_add_ioff A) -hioff addE. rewrite wunsigned_add; lia. - rewrite (alloc_stack_top_stack ok_m1') top_stack_after_aligned_alloc //. - move: ok_ra; rewrite wrepr0 GRing.addr0 /stack_frame_allocation_size wrepr_opp => -> /=. - have := decode_encode_label small_dom_p' mem_lret. - rewrite ok_retptr /rdecode_label /= => -> /=. - by rewrite (eval_jumpE ok_cbody) ok_pc. + case: ra_return EQ ra_return_ty @Q ok_body {free_ra ok_fd'} + => [ra_return|] EQ ra_return_ty Q ok_body. + + move: ok_body; rewrite catA => ok_body. + exists vm2.[ra_return <- Vword retptr]. + + apply: lsem_step2. + + apply: (eval_lsem1 ok_body) => //. + apply: (spec_lload hliparams) => /=. + * by move/eqP: ra_return_ty. + * by rewrite /get_var ok_rsp2; reflexivity. + rewrite wrepr0 GRing.addr0 hreadf. + exact: hreadi. + move: ok_body; rewrite /Q -[[:: _; _]]cat1s catA => ok_body. + apply: (eval_lsem1 ok_body) => //=. + + by rewrite [size (_ ++ [:: _])]size_cat addn1. + rewrite /eval_instr /=. + move /eqP in ra_return_ty. + rewrite /get_var Vm.setP_eq vm_truncate_val_eq //= truncate_word_u /=. + have := decode_encode_label small_dom_p' mem_lret. + rewrite ok_retptr /rdecode_label /= => -> /=. + by rewrite (eval_jumpE ok_cbody) ok_pc. + rewrite /sp_alloc_ra EQ /=. + apply eq_ex_set_r; first by case; clear; SvD.fsetdec. + apply: (eq_ex_set_l _ (eq_ex_refl _)). + by rewrite ok_rsp2 vm_truncate_val_eq. + exists vm2.[vrsp <- Vword (rsp + wrepr _ (wsize_size Uptr))]. + + move: ok_body; rewrite catA => ok_body. + apply: (eval_lsem_step1 ok_body) => //. + rewrite /eval_instr /= lp_rspE. + move /eqP in ra_return_ty. + rewrite /get_var ok_rsp2 /= truncate_word_u /=. + rewrite hreadf hreadi /=. + have := decode_encode_label small_dom_p' mem_lret. + rewrite ok_retptr /rdecode_label /= => -> /=. + by rewrite (eval_jumpE ok_cbody) ok_pc. + by rewrite /sp_alloc_ra EQ /=. + + (* We combine the 3 parts together. *) + exists m2 vmf. + + exact: (lsem_trans3 hsemi E hsemf). + apply eq_exT with vm2. - + by apply: eq_exI K2; SvD.fsetdec. - by move=> x hx; rewrite Vm.setP_neq //; apply/eqP; SvD.fsetdec. - + subst callee_saved; rewrite /kill_vars /=. - by move => ?; rewrite /set_RSP !Vm.setP; case: eqP. - move => a [] a_lo a_hi /negbTE nv. - have /= [L H] := ass_above_limit A. - apply: H2. - * by rewrite (ass_root A); lia. - rewrite (ass_valid A) nv /= !zify => - []. - change (wsize_size U8) with 1%Z. - rewrite (ass_add_ioff A). - move: (sf_stk_sz _) (sf_stk_ioff _) (sf_stk_extra_sz _) (ass_ioff A) H; lia. + + by apply: eq_exI K2; clear; SvD.fsetdec. + apply: eq_exT (eq_exI _ eq_vmf); + last by rewrite /ra_vm_return EQ; clear; SvD.fsetdec. + apply: (eq_ex_set_r _ (eq_ex_refl _)). + by case; clear; SvD.fsetdec. + + subst callee_saved; rewrite {1}/kill_vars /=. + move: eq_vmf; rewrite /ra_vm_return EQ /= => eq_vmf. + move => x; rewrite /set_RSP !Vm.setP; case: eqP => ?. + + subst x. + rewrite -eq_vmf; first by rewrite Vm.setP_eq. + case/andP: free_ra => _. + by case: (ra_return) => [r /andP[] _ /eqP|] /=; clear; SvD.fsetdec. + rewrite kill_varsE; case: Sv_memP => h. + + by apply/compat_value_uincl_undef/Vm.getP. + rewrite -eq_vmf //. + rewrite Vm.setP_neq //. + by apply/eqP. + + transitivity mi => //. + move => a [] a_lo a_hi /negbTE nv. + have /= [L R] := ass_above_limit A. + apply: H2. + * by rewrite (ass_root A); lia. + rewrite (ass_valid A) nv /= !zify => - []. + change (wsize_size U8) with 1%Z. + rewrite (ass_add_ioff A). + move: (sf_stk_sz _) (sf_stk_ioff _) (sf_stk_extra_sz _) (ass_ioff A) R; lia. + + exact: mm_free M2. + by transitivity mi. } Qed. @@ -4738,9 +4751,9 @@ Section PROOF. have {H}[] := H vm args' ok_args' args_args' vm_rsp. - by move: vm_rip; rewrite lp_ripE. move => m1 k m2 vm2 res' ok_save_stack ok_callee_saved ok_m1 sexec ok_res' res_res' vm2_rsp ?; subst m'. - set k' := Sv.union k (Sv.union match fd.(f_extra).(sf_return_address) with RAreg ra _ | RAstack (Some ra) _ _ => Sv.singleton ra | RAstack _ _ _ => Sv.empty | RAnone => Sv.union var_tmps vflags end (if fd.(f_extra).(sf_save_stack) is SavedStackReg r then Sv.singleton r else Sv.empty)). + set k' := Sv.union k (Sv.union (ra_undef fd var_tmps) (ra_vm_return fd.(f_extra))). set s1 := {| escs := scs; emem := m ; evm := vm |}. - set s2 := {| escs := scs'; emem := free_stack m2 ; evm := set_RSP p (free_stack m2) vm2 |}. + set s2 := {| escs := scs'; emem := free_stack m2 ; evm := set_RSP p (free_stack m2) (kill_vars (ra_vm_return fd.(f_extra)) vm2) |}. have /= hss := sem_stack_stable sexec. have {sexec} /linear_fdP : sem_call p var_tmps dummy_instr_info k' s1 fn s2. - econstructor. @@ -4820,7 +4833,7 @@ Section PROOF. + have := [elaborate (wunsigned_range (top_stack m1))]. have := [elaborate (wunsigned_range (top_stack m))]. by lia. - - by rewrite ok_fd => _ [<-]; rewrite Export. + - by reflexivity. move => lmo vmo texec vm_eq_vmo s2_vmo ? M' U'. have vm2_vmo : ∀ r, List.In r (f_res fd) → (value_uincl vm2.[r] vmo.[r]). - move => r r_in_result. @@ -4835,6 +4848,7 @@ Section PROOF. by move: RSP_not_result; rewrite sv_of_listE; apply/negP/negPn/in_map; exists r. rewrite Vm.setP_neq // kill_varsE Vm.setP_neq //. rewrite /killed_by_exit Sv_mem_add. + rewrite /kill_vars /ra_vm_return; move/is_RAnoneP: (Export) => -> /=. case: eqP => [ | _]; last by move /Sv_memP: r_not_saved => /negbTE ->. have := checked_prog ok_fd. rewrite /check_fd; t_xrbindP => _ _ _ + _ _ /= heq. @@ -4865,8 +4879,9 @@ Section PROOF. + exact: texec. move => r hr; apply: vm_eq_vmo. subst k'. + rewrite /ra_vm_return; move/is_RAnoneP: Export => ->. + rewrite (SvP.MP.empty_union_2 _ Sv.empty_spec). move: ok_callee_saved hr; clear. - rewrite -/(ra_vm _ _) -/(saved_stack_vm _). move: (Sv.union k _) => X. clear. rewrite sv_of_list_map Sv.diff_spec => S hrC [] hrX; apply. diff --git a/proofs/compiler/merge_varmaps.v b/proofs/compiler/merge_varmaps.v index a5dc81840..1004545dc 100644 --- a/proofs/compiler/merge_varmaps.v +++ b/proofs/compiler/merge_varmaps.v @@ -59,7 +59,7 @@ Section WRITE1. let ra := match get_fundef (p_funcs p) fn with | None => Sv.empty - | Some fd => Sv.union (ra_vm fd.(f_extra) var_tmp) (saved_stack_vm fd) + | Some fd => Sv.union (ra_undef fd var_tmp) (ra_vm_return fd.(f_extra)) end in Sv.union (writefun fn) ra. @@ -225,9 +225,10 @@ Section CHECK. let params := sv_of_list v_var fd.(f_params) in let DI := Sv.inter params (ra_undef fd var_tmp) in Let D := check_cmd fd.(f_extra).(sf_align) DI fd.(f_body) in + let DF := Sv.union (ra_vm_return fd.(f_extra)) D in let res := sv_of_list v_var fd.(f_res) in let W' := writefun_ra writefun fn in - Let _ := assert (disjoint D res) + Let _ := assert (disjoint DF res) (E.gen_error true None (pp_s "not able to ensure equality of the result")) in Let _ := assert (disjoint params magic_variables) (E.gen_error true None (pp_s "the function has RSP or global-data as parameter")) in @@ -246,11 +247,17 @@ Section CHECK. (E.gen_error true None (pp_s "not (disjoint magic_variables tmp_call)")) in match sf_return_address e with | RAreg ra _ => check_preserved_register W J "return address" ra - | RAstack ra _ _ => - if ra is Some r then + | RAstack ra_call ra_return _ _ => + Let _ := + if ra_call is Some r then assert (vtype r == sword Uptr) - (E.gen_error true None (pp_box [::pp_s "bad register type for"; pp_s "return address"; pp_var r])) - else ok tt + (E.gen_error true None (pp_box [::pp_s "bad register type for"; pp_s "return address (call)"; pp_var r])) + else ok tt + in + if ra_return is Some r then + assert (vtype r == sword Uptr) + (E.gen_error true None (pp_box [::pp_s "bad register type for"; pp_s "return address (return)"; pp_var r])) + else ok tt | RAnone => let to_save := sv_of_list fst fd.(f_extra).(sf_to_save) in Let _ := assert (disjoint to_save res) diff --git a/proofs/compiler/merge_varmaps_proof.v b/proofs/compiler/merge_varmaps_proof.v index a58a2838e..b9df52656 100644 --- a/proofs/compiler/merge_varmaps_proof.v +++ b/proofs/compiler/merge_varmaps_proof.v @@ -727,8 +727,9 @@ Section LEMMA. case: (checkP ok_p ok_fd) => ok_wrf. rewrite /check_fd; t_xrbindP => D. set ID := (ID in check_cmd _ ID _). + set DF := Sv.union _ D. set res := sv_of_list v_var (f_res fd). - set params := sv_of_list v_var(f_params fd). + set params := sv_of_list v_var (f_params fd). move => checked_body hdisj checked_params RSP_not_result preserved_magic checked_save_stack htmp_call_magic checked_ra. @@ -741,7 +742,9 @@ Section LEMMA. ~Sv.In ra (magic_variables p) & ~Sv.In ra params ] - | RAstack ra _ _ => if ra is Some r then [/\ vtype r == sword Uptr & ~Sv.In r (magic_variables p)] else True + | RAstack ra_call ra_return _ _ => + (if ra_call is Some r then [/\ vtype r == sword Uptr & ~Sv.In r (magic_variables p)] else True) /\ + (if ra_return is Some r then [/\ vtype r == sword Uptr & ~Sv.In r (magic_variables p)] else True) | RAnone => let to_save := sv_of_list fst (sf_to_save (f_extra fd)) in [/\ disjoint to_save res, @@ -751,25 +754,40 @@ Section LEMMA. (f_params fd) ] end. - - case heq : sf_return_address checked_ra => [ | ra ? | ra ofs ?]. + - case heq : sf_return_address checked_ra => [ | ra ? | ra_call ra_return ofs ?]. + by t_xrbindP => ??. + t_xrbindP => -> /Sv_memP ra_not_written. by rewrite SvP.union_mem negb_or => /andP[] /Sv_memP ra_not_magic /Sv_memP ra_not_param. - case: ra heq => [ r | ] // heq. - move: preserved_magic; rewrite /writefun_ra ok_fd /ra_vm heq /disjoint. - by t_xrbindP => /Sv.is_empty_spec h ->; split => //; SvD.fsetdec. + t_xrbindP=> hcall hreturn. + move: preserved_magic; + rewrite /writefun_ra ok_fd /ra_undef /ra_vm /ra_vm_return heq /disjoint => hempty. + split. + + case: ra_call heq hempty hcall => [ r | ] // heq. + by t_xrbindP => /Sv.is_empty_spec /= h ->; split => //; SvD.fsetdec. + case: ra_return heq hempty hreturn => [ r | ] // heq. + by t_xrbindP => /Sv.is_empty_spec /= h ->; split => //; SvD.fsetdec. have ra_neq_magic : match sf_return_address (f_extra fd) with - | RAreg ra _ | RAstack (Some ra) _ _ => - [&& ra != vgd, ra != vrsp & vtype ra == sword Uptr] + | RAreg ra _ => [&& ra != vgd, ra != vrsp & vtype ra == sword Uptr] + | RAstack ra_call ra_return _ _ => + (if ra_call is Some ra then [&& ra != vgd, ra != vrsp & vtype ra == sword Uptr] else true) && + (if ra_return is Some ra then [&& ra != vgd, ra != vrsp & vtype ra == sword Uptr] else true) | _ => True end. - - case: sf_return_address checked_ra => // [ ra _ | [ ra | ] _ _] //. + - case: sf_return_address checked_ra => // [ ra _ | ra_call ra_return _ _]. + rewrite /magic_variables -/vgd -/vrsp /= => -[]. - rewrite Sv.add_spec Sv.singleton_spec => -> ra_not_written. + rewrite Sv.add_spec Sv.singleton_spec => -> ra_not_written. by case/Decidable.not_or => /eqP -> /eqP -> _. rewrite /magic_variables -/vgd -/vrsp /= => -[]. - rewrite Sv.add_spec Sv.singleton_spec => ->. + move=> hcall hreturn. + apply /andP; split. + + case: ra_call hcall => [ra_call|//]. + rewrite /magic_variables -/vgd -/vrsp /= => -[]. + rewrite Sv.add_spec Sv.singleton_spec => ->. + by case/Decidable.not_or => /eqP -> /eqP ->. + case: ra_return hreturn => [ra_return|//]. + rewrite /magic_variables -/vgd -/vrsp /= => -[]. + rewrite Sv.add_spec Sv.singleton_spec => ->. by case/Decidable.not_or => /eqP -> /eqP ->. set t1' := with_vm s0 (set_RSP p (emem s0) (ra_undef_vm fd tvm1 var_tmps)). have pre1 : merged_vmap_precondition (write_c (f_body fd)) (sf_align (f_extra fd)) (emem s1) (evm t1'). @@ -827,12 +845,12 @@ Section LEMMA. + move: vgd (ra_undef _ _) (wrf _) hin not_GD; clear; SvD.fsetdec. have z_not_arr : ~~ is_sarr (vtype z). + move: hin ra_neq_magic checked_save_stack; clear => /SvD.F.union_1[]. - * rewrite /ra_vm; case: sf_return_address => [ | ra _ | ra rastack _ ]. + * rewrite /ra_vm; case: sf_return_address => [ | ra _ | ra_call ra_return rastack _ ]. - case/SvD.F.union_iff => [ | /vflagsP ->] //. by case/SvD.F.add_iff => [<- | /Sv.singleton_spec ->]. - by move => /Sv.singleton_spec -> /and3P[] _ _ /eqP ->. - case: ra; last by SvD.fsetdec. - by move => r /Sv.singleton_spec -> /and3P [] _ _ /eqP ->. + case: ra_call; last by SvD.fsetdec. + by move => r /Sv.singleton_spec -> /andP[] /and3P [] _ _ /eqP -> _. rewrite /saved_stack_vm. case: sf_save_stack => [ | ra | ofs ] /=; only 1, 3: SvD.fsetdec. by move/Sv.singleton_spec => -> _; t_xrbindP => /eqP ->. @@ -846,11 +864,11 @@ Section LEMMA. have [ t2 [ k texec hk ] sim2 ] := ih _ _ _ t1' checked_body pre1 sim1. have [tres ok_tres res_uincl] : - let: vm := set_RSP p (free_stack (emem t2)) (evm t2) in + let: vm := set_RSP p (free_stack (emem t2)) (kill_vars (ra_vm_return fd.(f_extra)) (evm t2)) in exists2 tres, get_var_is false vm (f_res fd) = ok tres & List.Forall2 value_uincl vres' tres. - - have : forall x, (x \in [seq (v_var i) | i <- f_res fd]) -> ~Sv.In x D. + - have : forall x, (x \in [seq (v_var i) | i <- f_res fd]) -> ~ Sv.In x DF. + move=> x hx; have /Sv_memP: Sv.mem x res by rewrite /res sv_of_listE. by move /Sv.is_empty_spec: hdisj; SvD.fsetdec. move: ok_vres'; rewrite /dc_truncate_val /= => /mapM2_id ?; subst vres'. @@ -862,12 +880,16 @@ Section LEMMA. move => x xs vx hvxs <- ?; rewrite inE negb_or => /andP [ hne hnin] h; subst vx. have {ih} [ | tres -> /= res_uincl ] := ih _ hvxs hnin. + by move=> ? h1; apply h; rewrite inE h1 orbT. - have ex : value_uincl vm.[x] (set_RSP p m vm').[x]. - + by rewrite /set_RSP Vm.setP_neq //; apply: hvm; apply h; rewrite inE eqxx. + have ex : value_uincl vm.[x] (set_RSP p m (kill_vars (ra_vm_return fd.(f_extra)) vm')).[x]. + + rewrite /set_RSP Vm.setP_neq //. + have := h x; rewrite inE eqxx => /(_ erefl). + rewrite Sv.union_spec => /Decidable.not_or [hra hD]. + rewrite kill_varsE; case: Sv_memP => // _. + by apply: hvm. by eexists; first reflexivity; constructor. exists - (Sv.union k (Sv.union (ra_vm fd.(f_extra) var_tmps) (saved_stack_vm fd))), - (set_RSP p (free_stack (emem t2)) (evm t2)), tres; split. + (Sv.union k (Sv.union (ra_undef fd var_tmps) (ra_vm_return fd.(f_extra)))), + (set_RSP p (free_stack (emem t2)) (kill_vars (ra_vm_return fd.(f_extra)) (evm t2))), tres; split. - econstructor. + exact: ok_fd. + move: ok_wrf. @@ -875,7 +897,10 @@ Section LEMMA. case: sf_return_address ra_neq_magic checked_ra => //. + move => ra _ /and3P [] -> -> -> /= [] _ hra ?? /Sv.subset_spec ok_wrf. by apply/Sv_memP => ?; apply: hra; apply: ok_wrf; exact: hk. - by case => // ? ? ? /and3P [] -> ->. + move=> ra_call ra_return _ _ /andP [hcall hreturn] _ _. + apply /andP; split. + + by case: ra_call hcall => [ra_call|//] /and3P[] -> -> _. + by case: ra_return hreturn => [ra_return|//] /and3P[] -> -> _. + move: ok_wrf. rewrite /valid_writefun /write_fd /saved_stack_valid /=. case: sf_save_stack checked_save_stack => // r; t_xrbindP => _ /Sv_memP r_not_written. @@ -941,6 +966,7 @@ Proof. rewrite /check_fd; t_xrbindP => D. rewrite /top_stack_aligned {1 2}Export. set ID := (ID in check_c _ ID _). + set DF := Sv.union _ D. set results := sv_of_list v_var (f_res fd). set params := sv_of_list v_var (f_params fd). move => checked_body hdisj checked_params RSP_not_result preserved_magic checked_save_stack tmp_call_magic. @@ -962,13 +988,20 @@ Proof. + move/Sv.subset_spec: ok_callee_saved ok_k. move: (writefun_ra _ _ _ _) => W. move: (sv_of_list _ _) => C. - move: (Sv.union _ (saved_stack_vm _)) => X. + move: (ra_undef _ _) => X. clear. SvD.fsetdec. + by move: texec; rewrite /ra_undef /ra_undef_vm_none /ra_vm Export /ra_undef_none. rewrite -ok_res'. apply: mapM_ext => /= r hr. - rewrite {2}/get_var Vm.setP_neq //; apply/eqP => K. + rewrite {2}/get_var Vm.setP_neq. + + rewrite /= kill_varsE. + case: Sv_memP => // hra. + move: hdisj => /disjoint_union [+ _]. + rewrite /results => /disjointP => {}hdisj. + case: (hdisj r hra). + by apply /sv_of_listP/in_map; exists r. + apply/eqP => K. move: RSP_not_result. rewrite /results sv_of_listE => /in_map; apply. by exists r. diff --git a/proofs/compiler/riscv_decl.v b/proofs/compiler/riscv_decl.v index cc312f12f..2ad8d4701 100644 --- a/proofs/compiler/riscv_decl.v +++ b/proofs/compiler/riscv_decl.v @@ -197,7 +197,7 @@ Instance riscv_decl : arch_decl register register_ext xregister rflag condt := To be on the safe side, GP and TP (thread pointer) are marked as callee-saved. *) Definition riscv_linux_call_conv : calling_convention := {| callee_saved := - map ARReg [:: SP; RA; GP; TP; X8; X9; X18; X19; X20; X21; X22; X23; X24; X25; X26; X27 ] + map ARReg [:: SP; GP; TP; X8; X9; X18; X19; X20; X21; X22; X23; X24; X25; X26; X27 ] ; callee_saved_not_bool := erefl true ; call_reg_args := [:: X10; X11; X12; X13; X14; X15; X16; X17 ] ; call_xreg_args := [::] diff --git a/proofs/compiler/riscv_params.v b/proofs/compiler/riscv_params.v index 5ebfcde4e..1b4780705 100644 --- a/proofs/compiler/riscv_params.v +++ b/proofs/compiler/riscv_params.v @@ -145,6 +145,7 @@ Definition riscv_liparams : linearization_params := lip_lmove := riscv_lmove; lip_check_ws := riscv_check_ws; lip_lstore := riscv_lstore; + lip_lload := riscv_lload; lip_lstores := lstores_imm_dfl riscv_tmp2 riscv_lstore RISCVFopn.smart_addi is_arith_small; lip_lloads := lloads_imm_dfl riscv_tmp2 riscv_lload RISCVFopn.smart_addi is_arith_small; |}. diff --git a/proofs/compiler/riscv_params_proof.v b/proofs/compiler/riscv_params_proof.v index 5ac41cebb..16bfcc82f 100644 --- a/proofs/compiler/riscv_params_proof.v +++ b/proofs/compiler/riscv_params_proof.v @@ -255,9 +255,8 @@ Qed. Lemma riscv_lload_correct : lload_correct_aux (lip_check_ws riscv_liparams) riscv_lload. Proof. - move=> xd xs ofs s vm top hgets. - case heq: vtype => [|||ws] //; t_xrbindP. - move=> _ <- /eqP ? w hread hset; subst ws. + move=> xd xs ofs ws top s w vm heq hcheck hgets hread hset. + move/eqP: hcheck => ?; subst ws. rewrite /riscv_lload /= hgets /= truncate_word_u /= hread /=. by rewrite /exec_sopn /= truncate_word_u /= sign_extend_u hset. Qed. @@ -285,6 +284,7 @@ Definition riscv_hliparams : spec_lip_set_up_sp_register := riscv_spec_lip_set_up_sp_register; spec_lip_lmove := riscv_lmove_correct; spec_lip_lstore := riscv_lstore_correct; + spec_lip_lload := riscv_lload_correct; spec_lip_lstores := riscv_lstores_correct; spec_lip_lloads := riscv_lloads_correct; spec_lip_tmp := riscv_tmp_correct; diff --git a/proofs/compiler/x86_params.v b/proofs/compiler/x86_params.v index 21cc59c06..8de3d5514 100644 --- a/proofs/compiler/x86_params.v +++ b/proofs/compiler/x86_params.v @@ -124,6 +124,7 @@ Definition x86_liparams : linearization_params := lip_lmove := x86_lmove; lip_check_ws := x86_check_ws; lip_lstore := x86_lstore; + lip_lload := x86_lload; lip_lstores := lstores_dfl x86_lstore; lip_lloads := lloads_dfl x86_lload; |}. diff --git a/proofs/compiler/x86_params_proof.v b/proofs/compiler/x86_params_proof.v index 7c54115f0..4f95040df 100644 --- a/proofs/compiler/x86_params_proof.v +++ b/proofs/compiler/x86_params_proof.v @@ -242,9 +242,7 @@ Proof. apply/lstores_dfl_correct/x86_lstore_correct. Qed. Lemma x86_lload_correct : lload_correct_aux (lip_check_ws x86_liparams) x86_lload. Proof. - move=> xd xs ofs s vm top hgets. - case heq: vtype => [|||ws] //; t_xrbindP. - move=> _ <- hchk w hread hset. + move=> xd xs ofs ws top s w vm heq hcheck hgets hread hset. rewrite /x86_lload heq. apply: x86_lassign_correct => /=. + by rewrite hgets /= truncate_word_u /= hread /= truncate_word_u. @@ -269,6 +267,7 @@ Definition x86_hliparams {call_conv : calling_convention} : h_linearization_para spec_lip_set_up_sp_register := x86_spec_lip_set_up_sp_register; spec_lip_lmove := x86_lmove_correct; spec_lip_lstore := x86_lstore_correct; + spec_lip_lload := x86_lload_correct; spec_lip_lstores := x86_lstores_correct; spec_lip_lloads := x86_lloads_correct; spec_lip_tmp := x86_tmp_correct; diff --git a/proofs/lang/expr.v b/proofs/lang/expr.v index 160455aa9..29c5590e1 100644 --- a/proofs/lang/expr.v +++ b/proofs/lang/expr.v @@ -549,38 +549,52 @@ Qed. HB.instance Definition _ := hasDecEq.Build saved_stack saved_stack_eq_axiom. +(* An instance of this record describes, for a given Jasmin function, how the + return address is passed and used by the function when it is called. *) Variant return_address_location := | RAnone -| RAreg of var & option var (* The return address is pass by a register and - keeped in this register during function call, - the option is for incrementing the large stack in arm *) -| RAstack of option var & Z & option var. - (* None means that the call instruction directly store ra on the stack - Some r means that the call instruction directly store ra on r and - the function should store r on the stack, - The second option is for incrementing the large stack in arm *) + (* Do not do anything about return address. This is used for export functions, + since they do not deal directly with the return address. *) +| RAreg of var & option var + (* The return address is passed by a register and + kept in this register during function call, + the option is for incrementing the large stack in arm. *) +| RAstack of option var & option var & Z & option var. + (* The return address is saved on the stack for most of the execution of the + function. + - The first argument describes what happens at call time. + + None means that the call instruction directly stores ra on the stack; + + Some r means that the call instruction directly stores ra + on register r and the function should store r on the stack. + - The second argument describes what happens at return time. + + None means that the return instruction reads ra from the stack; + + Some r means that the return instruction reads ra from register r, + it is the duty of the function to write ra in r (the proper code + is inserted by linearization). + - The third option specifies the offset of the stack where ra is written. + - The fourth option is for incrementing the large stack in arm. *) Definition is_RAnone ra := if ra is RAnone then true else false. Definition is_RAstack ra := - if ra is RAstack _ _ _ then true else false. - -Definition is_RAstack_None ra := - if ra is RAstack None _ _ then true else false. + if ra is RAstack _ _ _ _ then true else false. Definition return_address_location_beq (r1 r2: return_address_location) : bool := match r1 with | RAnone => if r2 is RAnone then true else false | RAreg x1 o1 => if r2 is RAreg x2 o2 then (x1 == x2) && (o1 == o2) else false - | RAstack lr1 z1 o1 => if r2 is RAstack lr2 z2 o2 then [&& lr1 == lr2, z1 == z2 & o1 == o2] else false + | RAstack ra_call1 ra_return1 z1 o1 => + if r2 is RAstack ra_call2 ra_return2 z2 o2 then + [&& ra_call1 == ra_call2, ra_return1 == ra_return2, z1 == z2 & o1 == o2] + else false end. Lemma return_address_location_eq_axiom : Equality.axiom return_address_location_beq. Proof. - case => [ | x1 o1 | lr1 z1 o1 ] [ | x2 o2 | lr2 z2 o2 ] /=; try by constructor. + case => [ | x1 o1 | ra_call1 ra_return1 z1 o1 ] [ | x2 o2 | ra_call2 ra_return2 z2 o2 ] /=; try by constructor. + by apply (iffP andP) => [ []/eqP-> /eqP-> | []-> ->]. - by apply (iffP and3P) => [ []/eqP-> /eqP-> /eqP-> | []-> -> ->]. + by apply (iffP and4P) => [ []/eqP-> /eqP-> /eqP-> /eqP-> | []-> -> -> ->]. Qed. HB.instance Definition _ := hasDecEq.Build return_address_location diff --git a/proofs/lang/one_varmap.v b/proofs/lang/one_varmap.v index 4ca47740b..7a36a74d9 100644 --- a/proofs/lang/one_varmap.v +++ b/proofs/lang/one_varmap.v @@ -45,10 +45,17 @@ Definition ra_vm (e: stk_fun_extra) (tmp: Sv.t) : Sv.t := match e.(sf_return_address) with | RAreg ra _ => Sv.singleton ra - | RAstack ra _ _ => - if ra is Some ra then Sv.singleton ra else Sv.empty - | RAnone => - Sv.union tmp vflags + | RAstack ra_call _ _ _ => + sv_of_option ra_call + | RAnone => + Sv.union tmp vflags + end. + +(* TODO: ra_vm, ra_undef, ra_undef_vm... -> pick better names *) +Definition ra_vm_return (e : stk_fun_extra) : Sv.t := + match e.(sf_return_address) with + | RAstack _ ra_return _ _ => sv_of_option ra_return + | _ => Sv.empty end. Definition ra_undef fd (tmp: Sv.t) := @@ -56,7 +63,7 @@ Definition ra_undef fd (tmp: Sv.t) := Definition tmp_call (e: stk_fun_extra) : Sv.t := match e.(sf_return_address) with - | RAreg _ (Some r) | RAstack _ _ (Some r) => Sv.singleton r + | RAreg _ (Some r) | RAstack _ _ _ (Some r) => Sv.singleton r | _ => Sv.empty end. diff --git a/proofs/lang/sem_one_varmap.v b/proofs/lang/sem_one_varmap.v index 557135858..df8b04c88 100644 --- a/proofs/lang/sem_one_varmap.v +++ b/proofs/lang/sem_one_varmap.v @@ -77,9 +77,12 @@ Let vrsp : var := vid p.(p_extra).(sp_rsp). Definition ra_valid fd (ii:instr_info) (k: Sv.t) : bool := match fd.(f_extra).(sf_return_address) with - | RAstack ra _ _ => - if ra is Some ra then (ra != vgd) && (ra != vrsp) - else true + | RAstack ra_call ra_return _ _ => + (if ra_call is Some ra_call then (ra_call != vgd) && (ra_call != vrsp) + else true) + && + (if ra_return is Some ra_return then (ra_return != vgd) && (ra_return != vrsp) + else true) | RAreg ra _ => [&& (ra != vgd), (ra != vrsp) & (~~ Sv.mem ra k) ] | RAnone => true @@ -197,14 +200,15 @@ with sem_call : instr_info → Sv.t → estate → funname → estate → Prop : sem k {| escs := s1.(escs); emem := m1; evm := set_RSP m1 vm1; |} f.(f_body) s2' → valid_RSP s2'.(emem) s2'.(evm) → let m2 := free_stack s2'.(emem) in - s2 = {| escs := s2'.(escs); emem := m2 ; evm := set_RSP m2 s2'.(evm) |} → - let vm := Sv.union (ra_vm f.(f_extra) var_tmp) (saved_stack_vm f) in - sem_call ii (Sv.union k vm) s1 fn s2. + let vm2 := kill_vars (ra_vm_return f.(f_extra)) s2'.(evm) in + s2 = {| escs := s2'.(escs); emem := m2 ; evm := set_RSP m2 vm2 |} → + let k' := Sv.union (ra_undef f var_tmp) (ra_vm_return f.(f_extra)) in + sem_call ii (Sv.union k k') s1 fn s2. Variant sem_export_call_conclusion (scs: syscall_state_t) (m: mem) (fd: sfundef) (args: values) (vm: Vm.t) (scs': syscall_state_t) (m': mem) (res: values) : Prop := | SemExportCallConclusion (m1: mem) (k: Sv.t) (m2: mem) (vm2: Vm.t) (res':values) of saved_stack_valid fd k & - Sv.Subset (Sv.inter callee_saved (Sv.union k (Sv.union (ra_vm fd.(f_extra) var_tmp) (saved_stack_vm fd)))) (sv_of_list fst fd.(f_extra).(sf_to_save)) & + Sv.Subset (Sv.inter callee_saved (Sv.union k (ra_undef fd var_tmp))) (sv_of_list fst fd.(f_extra).(sf_to_save)) & alloc_stack m fd.(f_extra).(sf_align) fd.(f_extra).(sf_stk_sz) fd.(f_extra).(sf_stk_ioff) fd.(f_extra).(sf_stk_extra_sz) = ok m1 & (* all2 check_ty_val fd.(f_tyin) args & *) sem k {| escs := scs; emem := m1 ; evm := set_RSP m1 (ra_undef_vm_none fd.(f_extra).(sf_save_stack) var_tmp vm) |} fd.(f_body) {| escs:= scs'; emem := m2 ; evm := vm2 |} & @@ -307,10 +311,11 @@ Lemma sem_callE ii k s fn s' : sem k' {| escs := s.(escs); emem := m1 ; evm := set_RSP m1 vm; |} f.(f_body) s2') (λ _ _ s2' _, valid_RSP s2'.(emem) s2'.(evm)) (λ f _ s2' _, + let vm2 := kill_vars (ra_vm_return f.(f_extra)) s2'.(evm) in let m2 := free_stack s2'.(emem) in - s' = {| escs := s2'.(escs); emem := m2 ; evm := set_RSP m2 (evm s2') |}) + s' = {| escs := s2'.(escs); emem := m2 ; evm := set_RSP m2 vm2 |}) (λ f _ _ k', - k = Sv.union k' (Sv.union (ra_vm f.(f_extra) var_tmp) (saved_stack_vm f))). + k = Sv.union k' (Sv.union (ra_undef f var_tmp) (ra_vm_return f.(f_extra)))). Proof. case => { ii k s fn s' } /= ii k s s' fn f m1 s2' ok_f ok_ra ok_ss ok_sp ok_RSP ok_alloc exec_body ok_RSP' /= ->. by exists f m1 s2' k. @@ -424,10 +429,11 @@ Section SEM_IND. sem k {| escs := s1.(escs); emem := m1; evm := set_RSP m1 vm1; |} fd.(f_body) s2' → Pc k {| escs := s1.(escs); emem := m1; evm := set_RSP m1 vm1; |} fd.(f_body) s2' → valid_RSP s2'.(emem) s2'.(evm) → + let vm2 := kill_vars (ra_vm_return fd.(f_extra)) s2'.(evm) in let m2 := free_stack s2'.(emem) in - s2 = {| escs := s2'.(escs); emem := m2 ; evm := set_RSP m2 (evm s2') |} → - let vm := Sv.union k (Sv.union (ra_vm fd.(f_extra) var_tmp) (saved_stack_vm fd)) in - Pfun ii vm s1 fn s2. + s2 = {| escs := s2'.(escs); emem := m2 ; evm := set_RSP m2 vm2 |} → + let k' := Sv.union (ra_undef fd var_tmp) (ra_vm_return fd.(f_extra)) in + Pfun ii (Sv.union k k') s1 fn s2. Hypotheses (Hcall: sem_Ind_call) diff --git a/proofs/lang/sem_one_varmap_facts.v b/proofs/lang/sem_one_varmap_facts.v index 9b8a4934c..0da65d71a 100644 --- a/proofs/lang/sem_one_varmap_facts.v +++ b/proofs/lang/sem_one_varmap_facts.v @@ -254,9 +254,12 @@ Proof. rewrite (ass_frames ok_alloc) (ass_root ok_alloc) /= -/(top_stack (emem s1)) cmp_le_refl. exact: ok_RSP. move => /eqP r_neq_rsp. + rewrite kill_varsE. + case: Sv_memP; first by SvD.fsetdec. + move=> _. rewrite -(ih r). 2: SvD.fsetdec. rewrite /set_RSP Vm.setP_neq // /ra_undef_vm kill_varsE. - case: Sv_memP => //; rewrite /ra_undef; SvD.fsetdec. + case: Sv_memP => //; SvD.fsetdec. Qed. Lemma sem_not_written k s1 c s2 : @@ -394,20 +397,32 @@ Qed. Lemma Hproc_pm : sem_Ind_proc p var_tmp Pc Pfun. Proof. red => ii k s1 s2 fn fd m1 s2' ok_fd ok_ra ok_ss ok_sp ok_RSP ok_m1 /sem_stack_stable s ih ok_RSP' ->. - rewrite /ra_valid in ok_ra. - rewrite /saved_stack_valid in ok_ss. - rewrite /Pfun !disjoint_unionE ih /=. - rewrite /ra_vm /saved_stack_vm. - apply/andP; split; last first. - + case: sf_save_stack ok_ss => //. - move=> /= r /and3P[] /eqP r_neq_gd /eqP r_neq_rsp _. - by rewrite /magic_variables /disjoint /is_true Sv.is_empty_spec /=; SvD.fsetdec. - case: sf_return_address ok_ra => //. - + rewrite disjoint_unionE => rax_not_magic. - by apply/andP; split => //; apply: flags_not_magic. - 1: move=> r _ /= /and3P[] /eqP r_neq_gd /eqP r_neq_rsp _. - 2: move=> [] //= r _ _ /andP[] /eqP r_neq_gd /eqP r_neq_rsp. - all: rewrite /magic_variables /disjoint /is_true Sv.is_empty_spec /=; SvD.fsetdec. + have hmagic: forall (r:var), + r != vid (sp_rip (p_extra p)) -> + r != vid (sp_rsp (p_extra p)) -> + disjoint (Sv.singleton r) (magic_variables p). + + by move=> r /eqP + /eqP; + rewrite /magic_variables /disjoint /is_true Sv.is_empty_spec; + clear; SvD.fsetdec. + rewrite /Pfun /ra_undef !disjoint_unionE ih /=. + rewrite -andbA; apply/and3P; split. + + move: ok_ra; rewrite /ra_valid /ra_vm. + case: sf_return_address => //. + + move=> _; rewrite disjoint_unionE. + by apply/andP; split => //; apply: flags_not_magic. + + move=> ra _ /and3P [+ + _]. + by apply hmagic. + move=> ra_call _ _ _ /andP [hcall _]. + case: ra_call hcall => [ra_call|//] /andP[]. + by apply hmagic. + + move: ok_ss; rewrite /saved_stack_valid /saved_stack_vm. + case: sf_save_stack => //. + move=> /= r /and3P[] r_neq_gd r_neq_rsp _. + by apply hmagic. + move: ok_ra; rewrite /ra_valid /ra_vm_return. + case: sf_return_address => // _ ra_return _ _ /andP [_ hreturn]. + case: ra_return hreturn => [ra_return|//] /andP[]. + by apply hmagic. Qed. Lemma sem_RSP_GD_not_written k s1 c s2 :