Compute max call depth

CHANGELOG.md

@@ -6,6 +6,11 @@
 - Support ARMv7 (Cortex-M4) as target architecture
   ([PR #242](https://github.com/jasmin-lang/jasmin/pull/242)).
 
+- Compute the maximal call depth for each function; a function annotation
+  `#[calldepth=n]` can be used to check that the maximal call depth is exactly
+  `n`
+  ([PR #282](https://github.com/jasmin-lang/jasmin/pull/282)).
+
 ## Other changes
 
 - Explicit if-then-else in flag combinations is no longer supported

compiler/src/annotations.ml

@@ -24,15 +24,17 @@ type returnaddress_kind =
   | OnReg
 
 type f_annot = {
-    retaddr_kind  : returnaddress_kind option;
+    retaddr_kind          : returnaddress_kind option;
     stack_allocation_size : Z.t option;
-    stack_size    : Z.t option;
-    stack_align   : wsize option;
+    stack_size            : Z.t option;
+    stack_align           : wsize option;
+    max_call_depth        : Z.t option;
 }
 
 let f_annot_empty = {
-    retaddr_kind  = None;
+    retaddr_kind          = None;
     stack_allocation_size = None;
-    stack_size    = None;
-    stack_align   = None;
+    stack_size            = None;
+    stack_align           = None;
+    max_call_depth        = None;
   }

compiler/src/checkAnnot.ml

@@ -4,7 +4,7 @@ open Prog
 
 let check_stack_size fds =
   List.iter
-    (fun ( { Expr.sf_stk_sz; Expr.sf_stk_extra_sz; Expr.sf_align },
+    (fun ( { Expr.sf_stk_sz; Expr.sf_stk_extra_sz; Expr.sf_align; Expr.sf_max_call_depth },
            { f_loc; f_annot; f_name } ) ->
       let hierror fmt =
         hierror ~loc:(Lone f_loc) ~funname:f_name.fn_name
@@ -36,7 +36,7 @@ let check_stack_size fds =
           else
             hierror "the stack has size %a (expected: %a)" Z.pp_print actual
               Z.pp_print expected);
-      match f_annot.stack_align with
+      (match f_annot.stack_align with
       | None -> ()
       | Some expected ->
           let actual = sf_align in
@@ -47,7 +47,18 @@ let check_stack_size fds =
                 f_name.fn_name (string_of_ws expected))
           else
             hierror "the stack has alignment %s (expected: %s)"
-              (string_of_ws actual) (string_of_ws expected))
+              (string_of_ws actual) (string_of_ws expected));
+      match f_annot.max_call_depth with
+      | None -> ()
+      | Some expected ->
+          let actual = Conv.z_of_cz sf_max_call_depth in
+          if actual = expected then (
+            if !debug then
+              Format.eprintf "INFO: %s has the expected max call depth (%a)@."
+                f_name.fn_name Z.pp_print expected)
+            else
+              hierror "the maximum call depth is %a (expected: %a)"
+                Z.pp_print actual Z.pp_print expected)
     fds
 
 let rec check_no_for_loop ~funname s =

compiler/src/pretyping.ml

@@ -1902,9 +1902,10 @@ let process_f_annot annot =
   let mk_ra = Annot.filter_string_list None ["stack", OnStack; "reg", OnReg] in
 
   { retaddr_kind          = Annot.ensure_uniq1 "returnaddress"  mk_ra                annot;
-    stack_allocation_size = Annot.ensure_uniq1 "stackallocsize" (Annot.pos_int None) annot; 
-    stack_size            = Annot.ensure_uniq1 "stacksize"      (Annot.pos_int None) annot; 
-    stack_align           = Annot.ensure_uniq1 "stackalign"     (Annot.wsize None)   annot}
+    stack_allocation_size = Annot.ensure_uniq1 "stackallocsize" (Annot.pos_int None) annot;
+    stack_size            = Annot.ensure_uniq1 "stacksize"      (Annot.pos_int None) annot;
+    stack_align           = Annot.ensure_uniq1 "stackalign"     (Annot.wsize None)   annot;
+    max_call_depth        = Annot.ensure_uniq1 "calldepth"      (Annot.pos_int None) annot}
 
 
 (* -------------------------------------------------------------------- *)

compiler/src/printer.ml

@@ -506,10 +506,12 @@ let pp_sprog ~debug tbl asmOp fmt ((funcs, p_extra):('info, 'asm) Prog.sprog) =
   let pp_opn = pp_opn asmOp in
   let pp_var = pp_var ~debug in
   let pp_f_extra fmt f_extra = 
-    Format.fprintf fmt "(* @[<v>stack size = %a + %a; alignment = %s;@ saved register = @[%a@];@ saved stack = %a;@ return_addr = %a@] *)"
+    Format.fprintf fmt "(* @[<v>alignment = %s; stack size = %a + %a; max stack size = %a;@ max call depth = %a;@ saved register = @[%a@];@ saved stack = %a;@ return_addr = %a@] *)"
+      (string_of_ws f_extra.Expr.sf_align)
       Z.pp_print (Conv.z_of_cz f_extra.Expr.sf_stk_sz)
       Z.pp_print (Conv.z_of_cz f_extra.Expr.sf_stk_extra_sz)
-      (string_of_ws f_extra.Expr.sf_align)
+      Z.pp_print (Conv.z_of_cz f_extra.Expr.sf_stk_max)
+      Z.pp_print (Conv.z_of_cz f_extra.Expr.sf_max_call_depth)
       (pp_list ",@ " (pp_to_save ~debug tbl)) (f_extra.Expr.sf_to_save)
       (pp_saved_stack ~debug tbl) (f_extra.Expr.sf_save_stack)
       (pp_return_address ~debug tbl)  (f_extra.Expr.sf_return_address)

compiler/src/stackAlloc.ml

@@ -56,11 +56,12 @@ let pp_return fmt n =
 
 let pp_sao tbl fmt sao =
   let open Stack_alloc in
-    Format.fprintf fmt "alignment = %s; size = %a; extra size = %a; max size = %a@;params =@;<2 2>@[<v>%a@]@;return = @[<hov>%a@]@;slots =@;<2 2>@[<v>%a@]@;alloc= @;<2 2>@[<v>%a@]@;saved register = @[<hov>%a@]@;saved stack = %a@;return address = %a@]"
-   (string_of_ws sao.sao_align)
+  Format.fprintf fmt "alignment = %s; size = %a; extra size = %a; max size = %a@;max call depth = %a@;params =@;<2 2>@[<v>%a@]@;return = @[<hov>%a@]@;slots =@;<2 2>@[<v>%a@]@;alloc= @;<2 2>@[<v>%a@]@;saved register = @[<hov>%a@]@;saved stack = %a@;return address = %a"
+    (string_of_ws sao.sao_align)
     Z.pp_print (Conv.z_of_cz sao.sao_size)
     Z.pp_print (Conv.z_of_cz sao.sao_extra_size)
     Z.pp_print (Conv.z_of_cz sao.sao_max_size)
+    Z.pp_print (Conv.z_of_cz sao.sao_max_call_depth)
     (pp_list "@;" (pp_param_info tbl)) sao.sao_params
     (pp_list "@;" pp_return) sao.sao_return
     (pp_list "@;" (pp_slot tbl)) sao.sao_slots
@@ -129,6 +130,7 @@ let memory_analysis pp_err ~debug tbl up =
         sao_size   = Conv.cz_of_int size;
         sao_extra_size = Z0;
         sao_max_size = Z0;
+        sao_max_call_depth = Z0;
         sao_params = List.map (omap conv_pi) sao.sao_params;
         sao_return = List.map (omap Conv.nat_of_int) sao.sao_return;
         sao_slots  = do_slots sao.sao_slots;
@@ -213,15 +215,17 @@ let memory_analysis pp_err ~debug tbl up =
       if has_stack && ro.ro_rsp = None then extra @ [rsp]
       else extra in
     let extra_size, align, extrapos = Varalloc.extend_sao sao extra in
-    let align, max_stk = 
-      Sf.fold (fun fn (align, max_stk) ->
+    let align, max_stk, max_call_depth =
+      Sf.fold (fun fn (align, max_stk, max_call_depth) ->
           let sao = get_sao fn in
-          let fn_algin = sao.Stack_alloc.sao_align in
-          let align = if wsize_lt align fn_algin then fn_algin else align in
+          let fn_align = sao.Stack_alloc.sao_align in
+          let align = if wsize_lt align fn_align then fn_align else align in
           let fn_max = Conv.z_of_cz (sao.Stack_alloc.sao_max_size) in
-          let max_stk = if Z.lt max_stk fn_max then fn_max else max_stk in
-          align, max_stk
-        ) sao.sao_calls (align, Z.zero) in
+          let max_stk = Z.max max_stk fn_max in
+          let fn_max_call_depth = Conv.z_of_cz (sao.Stack_alloc.sao_max_call_depth) in
+          let max_call_depth = Z.max max_call_depth fn_max_call_depth in
+          align, max_stk, max_call_depth
+        ) sao.sao_calls (align, Z.zero, Z.zero) in
     let max_size = 
       let stk_size = 
         Z.add (Conv.z_of_cz csao.Stack_alloc.sao_size)
@@ -233,6 +237,7 @@ let memory_analysis pp_err ~debug tbl up =
           Conv.z_of_cz (Memory_model.round_ws align (Conv.cz_of_z stk_size))
         | Internal -> assert false in
       Z.add max_stk stk_size in
+    let max_call_depth = Z.succ max_call_depth in
     let saved_stack = 
       if has_stack then
         match ro.ro_rsp with
@@ -257,6 +262,7 @@ let memory_analysis pp_err ~debug tbl up =
         sao_align = align;
         sao_extra_size = Conv.cz_of_int extra_size;
         sao_max_size = Conv.cz_of_z max_size;
+        sao_max_call_depth = Conv.cz_of_z max_call_depth;
         sao_to_save = convert_to_save ro.ro_to_save;
         sao_rsp  = saved_stack;
         sao_return_address =

compiler/tests/fail/annotation/calldepth.jazz

@@ -0,0 +1,8 @@
+/* no call: max call depth is 1 */
+
+#[calldepth=2]
+export fn f () -> reg u64 {
+  reg u64 res;
+  res = 0;
+  return res;
+}

compiler/tests/success/calldepth.jazz

@@ -0,0 +1,20 @@
+fn f () -> reg u64 {
+  reg u64 res;
+  res = 0;
+  return res;
+}
+
+/* conditional call */
+
+#[calldepth=2]
+export fn g (reg u64 x) -> reg u64 {
+  reg u64 res;
+
+  if (x == 0) {
+    res = 0;
+  } else {
+    res = f ();
+  }
+
+  return res;
+}

proofs/compiler/stack_alloc.v

@@ -904,6 +904,7 @@ Record stk_alloc_oracle_t :=
   ; sao_size: Z
   ; sao_extra_size: Z
   ; sao_max_size : Z
+  ; sao_max_call_depth : Z
   ; sao_params : seq (option param_info)  (* Allocation of pointer params *)
   ; sao_return : seq (option nat)         (* Where to find the param input region *)
   ; sao_slots : seq (var * wsize * Z)  
@@ -1398,8 +1399,9 @@ Definition alloc_fd p_extra mglob (fresh_reg : string -> stype -> string) (local
   let f_extra := {|
         sf_align  := sao.(sao_align);
         sf_stk_sz := sao.(sao_size);
-        sf_stk_max := sao.(sao_max_size);
         sf_stk_extra_sz := sao.(sao_extra_size);
+        sf_stk_max := sao.(sao_max_size);
+        sf_max_call_depth := sao.(sao_max_call_depth);
         sf_to_save := sao.(sao_to_save);
         sf_save_stack := sao.(sao_rsp);
         sf_return_address := sao.(sao_return_address);

proofs/lang/expr.v

@@ -585,11 +585,12 @@ Qed.
 Definition return_address_location_eqMixin := Equality.Mixin return_address_location_eq_axiom.
 Canonical  return_address_location_eqType  := Eval hnf in EqType return_address_location return_address_location_eqMixin.
 
-Record stk_fun_extra := MkSFun { 
+Record stk_fun_extra := MkSFun {
   sf_align          : wsize;
   sf_stk_sz         : Z;
   sf_stk_extra_sz   : Z;
-  sf_stk_max        : Z; 
+  sf_stk_max        : Z;
+  sf_max_call_depth : Z;
   sf_to_save        : seq (var * Z);
   sf_save_stack     : saved_stack;
   sf_return_address : return_address_location;
@@ -598,17 +599,18 @@ Record stk_fun_extra := MkSFun {
 Definition sfe_beq (e1 e2: stk_fun_extra) : bool :=
   (e1.(sf_align) == e2.(sf_align)) &&
   (e1.(sf_stk_sz) == e2.(sf_stk_sz)) &&
-  (e1.(sf_stk_max) == e2.(sf_stk_max)) && 
+  (e1.(sf_stk_max) == e2.(sf_stk_max)) &&
+  (e1.(sf_max_call_depth) == e2.(sf_max_call_depth)) &&
   (e1.(sf_stk_extra_sz) == e2.(sf_stk_extra_sz)) &&
   (e1.(sf_to_save) == e2.(sf_to_save)) &&
   (e1.(sf_save_stack) == e2.(sf_save_stack)) &&
   (e1.(sf_return_address) == e2.(sf_return_address)).
 
 Lemma sfe_eq_axiom : Equality.axiom sfe_beq.
 Proof.
-  case => a b c d e f g [] a' b' c' d' e' f' g'; apply: (equivP andP) => /=; split.
-  + by case => /andP[] /andP[] /andP[] /andP[] /andP [] /eqP <- /eqP <- /eqP <- /eqP <- /eqP <- /eqP <- /eqP <-.
-  by case => <- <- <- <- <- <- <-; rewrite !eqxx.
+  case => a b c d e f g h [] a' b' c' d' e' f' g' h'; apply: (equivP andP) => /=; split.
+  + by case => /andP[] /andP[] /andP[] /andP[] /andP[] /andP [] /eqP <- /eqP <- /eqP <- /eqP <- /eqP <- /eqP <- /eqP <- /eqP <-.
+  by case => <- <- <- <- <- <- <- <-; rewrite !eqxx.
 Qed.
 
 Definition sfe_eqMixin   := Equality.Mixin sfe_eq_axiom.