cleaning

compiler/src/pp_riscv.ml

@@ -173,29 +173,25 @@ 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
       let cond_fst = pp_cond_arg ct.cond_fst in
       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

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

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

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,