use call and return for internal function call

Co-authored-by: Benjamin Grēgoire <[email protected]>

CHANGELOG.md

@@ -21,6 +21,10 @@
   ([PR #290](https://github.com/jasmin-lang/jasmin/pull/290)).
   These get extracted to `|<<|` and `|>>|` in EasyCrypt.
 
+- Local functions with return address on the stack use usual `CALL`
+  and `RET` x86 instructions instead of (direct & computed) `JMP`
+  ([PR #194](https://github.com/jasmin-lang/jasmin/pull/194)).
+
 - x86 intrinsics that accept a size suffix (e.g., `_128`) also accept, with a
   warning, a vector suffix (e.g., `_4u32`)
   ([PR #303](https://github.com/jasmin-lang/jasmin/pull/303)).
@@ -31,7 +35,7 @@
 
 ## Bug fixes
 
- - The x86 instructions `VMOVSHDUP` and `VMOVSLDUP` accept a size suffix (`_128`
+- The x86 instructions `VMOVSHDUP` and `VMOVSLDUP` accept a size suffix (`_128`
    or `_256`) instead of a vector description suffix (`4u32` or `8u32`)
   ([PR #303](https://github.com/jasmin-lang/jasmin/pull/303);
   fixes [#301](https://github.com/jasmin-lang/jasmin/issues/301)).

compiler/src/arch_full.ml

@@ -2,6 +2,11 @@ open Arch_decl
 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 *)
+
 (* TODO: check that we cannot use sth already defined on the Coq side *)
 
 module type Core_arch = sig
@@ -29,6 +34,9 @@ module type Core_arch = sig
     (unit, (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.func ->
     (unit, (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.prog ->
     unit
+
+  val callstyle : reg callstyle
+
 end
 
 module type Arch = sig
@@ -56,6 +64,8 @@ module type Arch = sig
   val rsp_var : var
   val all_registers : var list
   val syscall_kill : Sv.t
+
+  val callstyle : var callstyle
 end
 
 module Arch_from_Core_arch (A : Core_arch) : Arch = struct
@@ -193,4 +203,10 @@ module Arch_from_Core_arch (A : Core_arch) : Arch = struct
   let all_registers = reg_vars @ regx_vars @ xreg_vars @ flag_vars
 
   let syscall_kill = Sv.diff (Sv.of_list all_registers) (Sv.of_list callee_save_vars)
+
+  let callstyle = 
+    match A.callstyle with
+    | StackDirect -> StackDirect
+    | ByReg o -> ByReg (Utils.omap var_of_reg o)
+
 end

compiler/src/arch_full.mli

@@ -2,6 +2,15 @@ open Arch_decl
 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 *)
+(* x86    : StackDirect 
+   arm v7 : ByReg (Some ra)
+   riscV  : ByReg (can it be StackDirect too ?)
+*)
+
 module type Core_arch = sig
   type reg
   type regx 
@@ -27,6 +36,9 @@ module type Core_arch = sig
     (unit, (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.func ->
     (unit, (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.prog ->
     unit
+
+  val callstyle : reg callstyle
+
 end
 
 module type Arch = sig
@@ -54,6 +66,9 @@ module type Arch = sig
   val rsp_var : var
   val all_registers : var list
   val syscall_kill : Sv.t
+
+  val callstyle : var callstyle 
+
 end
 
 module Arch_from_Core_arch (A : Core_arch) : Arch

compiler/src/arm_arch_full.ml

@@ -48,4 +48,6 @@ module Arm (Lowering_params : Arm_input) : Arch_full.Core_arch = struct
   let pp_asm = Pp_arm_m4.print_prog
 
   let analyze _ _ _ = failwith "TODO_ARM: analyze"
+
+  let callstyle = Arch_full.ByReg (Some LR)
 end

compiler/src/pp_arm_m4.ml

@@ -187,10 +187,10 @@ let pp_instr tbl fn (_ : Format.formatter) i =
       [ LInstr ("bl", [ pp_remote_label tbl lbl ]) ]
 
   | POPPC ->
-      [ LInstr ("b", [ pp_register LR ]) ]
+      [ LInstr ("pop", [ "{pc}" ]) ]
 
   | SysCall op ->
-      [LInstr ("call", [pp_syscall op])]
+      [LInstr ("call", [ pp_syscall op ])]
 
   | AsmOp (op, args) ->
       let id = instr_desc arm_decl arm_op_decl (None, op) in
@@ -209,10 +209,12 @@ let pp_body tbl fn fmt cmd = List.concat_map (pp_instr tbl fn fmt) cmd
 
 let mangle x = Printf.sprintf "_%s" x
 
+let pp_brace s = Format.sprintf "{%s}" s
+
 let pp_fun tbl fmt (fn, fd) =
   let fn = Conv.string_of_funname tbl fn in
   let pre =
-    if fd.asm_fd_export then [ LLabel (mangle fn); LLabel fn ] else []
+    if fd.asm_fd_export then [ LLabel (mangle fn); LLabel fn; LInstr ("push", [pp_brace (pp_register LR)]) ] else []
   in
   let body = pp_body tbl fn fmt fd.asm_fd_body in
   (* TODO_ARM: Review. *)

compiler/src/ppasm.ml

@@ -429,6 +429,7 @@ module Printer (BP:BPrinter) = struct
       `Instr (iname, [pp_label name lbl])
 
     | JAL _ -> assert false
+
     | CALL lbl ->
        `Instr ("call", [pp_remote_label tbl lbl])
 

compiler/src/printLinear.ml

@@ -74,7 +74,9 @@ let pp_instr asmOp tbl fmt i =
       (pp_opn asmOp) op
       (pp_list ",@ " (pp_expr tbl)) es
   | Lsyscall o -> F.fprintf fmt "SysCall %s" (pp_syscall o)
-  | Lcall lbl  -> F.fprintf fmt "Call %a" (pp_remote_label tbl) lbl
+  | Lcall(lr, lbl) -> 
+      let pp_o fmt o = match o with None -> () | Some v -> Format.fprintf fmt "%a " (pp_var_i tbl) v in
+      F.fprintf fmt "Call %a%a" pp_o lr (pp_remote_label tbl) lbl
   | Lret       -> F.fprintf fmt "Return"
   | Lalign     -> F.fprintf fmt "Align"
   | Llabel (k, lbl) -> F.fprintf fmt "Label %a%a" pp_label_kind k pp_label lbl

compiler/src/printer.ml

@@ -373,7 +373,10 @@ let pp_saved_stack ~debug tbl fmt = function
 
 let pp_return_address ~debug tbl fmt = function
   | Expr.RAreg x -> Format.fprintf fmt "%a" (pp_var ~debug) (Conv.var_of_cvar tbl x)
-  | Expr.RAstack z -> Format.fprintf fmt "RSP + %a" Z.pp_print (Conv.z_of_cz z)
+  | Expr.RAstack(Some x, z) -> 
+    Format.fprintf fmt "%a, RSP + %a" (pp_var ~debug) (Conv.var_of_cvar tbl x) Z.pp_print (Conv.z_of_cz z)
+  | Expr.RAstack(None, z) -> 
+    Format.fprintf fmt "RSP + %a" Z.pp_print (Conv.z_of_cz z)
   | Expr.RAnone   -> Format.fprintf fmt "_"
 
 let pp_sprog ~debug tbl asmOp fmt ((funcs, p_extra):('info, 'asm) Prog.sprog) =

compiler/src/prog.ml

@@ -544,6 +544,15 @@ let rec has_syscall_i i =
 
 and has_syscall c = List.exists has_syscall_i c
 
+let rec has_call_or_syscall_i i =
+  match i.i_desc with
+  | Csyscall _ | Ccall _ -> true
+  | Cassgn _ | Copn _ -> false
+  | Cif (_, c1, c2) | Cwhile(_, c1, _, c2) -> has_call_or_syscall c1 || has_call_or_syscall c2
+  | Cfor (_, _, c) -> has_call_or_syscall c
+
+and has_call_or_syscall c = List.exists has_call_or_syscall_i c
+
 (* -------------------------------------------------------------------- *)
 let clamp (sz : wsize) (z : Z.t) =
   Z.erem z (Z.shift_left Z.one (int_of_ws sz))

compiler/src/prog.mli

@@ -328,7 +328,7 @@ val expr_of_lval : 'len glval -> 'len gexpr option
 (* Functions over instruction                                           *)
 
 val has_syscall : ('len, 'info, 'asm) gstmt -> bool
-
+val has_call_or_syscall : ('len, 'info, 'asm) gstmt -> bool
 (* -------------------------------------------------------------------- *)
 val clamp : wsize -> Z.t -> Z.t
 val clamp_pe : pelem -> Z.t -> Z.t