From fbab30dab7854776a8a660c31255970fa5af3569 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Christophe=20L=C3=A9chenet?= Date: Wed, 23 Oct 2024 19:17:10 +0200 Subject: [PATCH] cleaning --- compiler/src/pp_riscv.ml | 36 +++++++++++++-------------- compiler/src/printer.ml | 4 +-- compiler/src/regalloc.ml | 4 +-- proofs/compiler/linearization_proof.v | 9 ------- 4 files changed, 22 insertions(+), 31 deletions(-) diff --git a/compiler/src/pp_riscv.ml b/compiler/src/pp_riscv.ml index 7bfe9f4a8..b9595aed0 100644 --- a/compiler/src/pp_riscv.ml +++ b/compiler/src/pp_riscv.ml @@ -173,11 +173,11 @@ let pp_instr fn i = [ LInstr ("j", [ pp_remote_label lbl ]) ] | JMPI arg -> - begin match arg with - | Reg RA -> [LInstr ("ret", [])] - | Reg r -> [ LInstr ("jr", [ pp_register r ]) ] - | _ -> failwith "TODO_RISCV: pp_instr jmpi" - end + 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 @@ -185,17 +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 -> - assert false - - | 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])] + | JAL _ + | CALL _ | POPPC -> - failwith ("POPC in function" ^ fn) + assert false | SysCall op -> [LInstr ("call", [ pp_syscall op ])] @@ -236,15 +232,19 @@ 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 [ 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", [ ]) ] + LInstr ("addi", [ pp_register SP; pp_register SP; "4"]); + LInstr ("ret", [ ]) ] else [] in head @ pre @ body @ pos diff --git a/compiler/src/printer.ml b/compiler/src/printer.ml index 92bd473cb..f6b105b61 100644 --- a/compiler/src/printer.ml +++ b/compiler/src/printer.ml @@ -375,10 +375,10 @@ 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= +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= +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 diff --git a/compiler/src/regalloc.ml b/compiler/src/regalloc.ml index fb39dfb1f..80d9032b1 100644 --- a/compiler/src/regalloc.ml +++ b/compiler/src/regalloc.ml @@ -468,7 +468,7 @@ let collect_variables ~(allvars: bool) (excluded:Sv.t) (f: ('info, 'asm) func) : (* TODO: should StackDirect be just StackByReg (None, None, None)? *) type retaddr = | StackDirect - (* ra is passed on and read from the stack *) + (* 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 @@ -1136,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 stored the return address *) + (* compute where the return address will be stored *) let ra = match f.f_cc with | Export _ -> StackDirect diff --git a/proofs/compiler/linearization_proof.v b/proofs/compiler/linearization_proof.v index 8174ad4d0..4955357c0 100644 --- a/proofs/compiler/linearization_proof.v +++ b/proofs/compiler/linearization_proof.v @@ -414,15 +414,6 @@ Definition lstore_correct_aux lip_check_ws lip_lstore := sem_fopn_args (lip_lstore xd ofs xs) s = ok (with_mem s m). Definition lstore_correct := lstore_correct_aux (lip_check_ws liparams) (lip_lstore liparams). -(* -Definition lload_correct_aux := - forall (xd xs : var_i) ofs ws wp s w, - vtype xs = sword ws -> - lip_check_ws liparams ws -> - (get_var true (evm s) xd >>= to_word Uptr) = ok wp -> - read (emem s) Aligned (wp + wrepr Uptr ofs)%R ws = ok w -> - sem_fopn_args (lip_lload liparams xd xs ofs) s = - ok (with_vm s (evm s).[xd <- Vword w]). *) Definition lload_correct_aux lip_check_ws lip_lload := forall (xd xs : var_i) ofs ws wp s w vm,