Extract instr_info & var_info to standard OCaml int

CHANGELOG.md

@@ -32,6 +32,10 @@
 
 - Lowering of a memory-to-memory copy always introduce an intermediate copy through a register
 
+- `instr_info` are now plain OCaml `int` and `var_info` are `Location.t`;
+   this removes costly translations with `positive` and a big conversion table
+   ([PR #209](https://github.com/jasmin-lang/jasmin/pull/209)).
+
 # Jasmin 22.0
 
 This release is the result of more than two years of active development. It thus

compiler/src/conv.ml

@@ -70,7 +70,6 @@ type 'info coq_tbl = {
      mutable count : int;
      var           : (Var.var, var) Hashtbl.t;
      cvar          : Var.var Hv.t;
-     vari          : (int, L.t) Hashtbl.t;
      iinfo         : (int, L.i_loc * 'info * Syntax.annotations) Hashtbl.t;
      funname       : (funname, BinNums.positive) Hashtbl.t;
      cfunname      : (BinNums.positive, funname) Hashtbl.t;
@@ -87,7 +86,6 @@ let empty_tbl info = {
     count    = 1;
     var      = Hashtbl.create 101;
     cvar     = Hv.create 101;
-    vari     = Hashtbl.create 1000;
     iinfo    = Hashtbl.create 1000;
     funname  = Hashtbl.create 101;
     cfunname = Hashtbl.create 101;
@@ -121,23 +119,13 @@ let var_of_cvar tbl cv =
 
 (* ------------------------------------------------------------------------ *)
 
-let get_loc tbl p =
-  try Hashtbl.find tbl.vari (int_of_pos p)
-  with Not_found -> L._dummy
-
-let set_loc tbl loc =
-  let n = new_count tbl in
-  Hashtbl.add tbl.vari n loc;
-  pos_of_int n
-
 let cvari_of_vari tbl v =
-  let p = set_loc tbl (L.loc v) in
+  let p = L.loc v in
   let cv = cvar_of_var tbl (L.unloc v) in
   { C.v_var = cv; C.v_info = p }
 
 let vari_of_cvari tbl v =
-  let loc =  get_loc tbl v.C.v_info in
-  L.mk_loc loc (var_of_cvar tbl v.C.v_var)
+  L.mk_loc v.C.v_info (var_of_cvar tbl v.C.v_var)
 
 let cgvari_of_gvari tbl v = 
   { C.gv = cvari_of_vari tbl v.gv;
@@ -184,15 +172,15 @@ let rec expr_of_cexpr tbl = function
 (* ------------------------------------------------------------------------ *)
 
 let clval_of_lval tbl = function
-  | Lnone(loc, ty)  -> C.Lnone (set_loc tbl loc, cty_of_ty ty)
+  | Lnone(loc, ty)  -> C.Lnone (loc, cty_of_ty ty)
   | Lvar x          -> C.Lvar  (cvari_of_vari tbl x)
   | Lmem (ws, x, e) -> C.Lmem (ws, cvari_of_vari tbl x, cexpr_of_expr tbl e)
   | Laset(aa,ws,x,e)-> C.Laset (aa, ws, cvari_of_vari tbl x, cexpr_of_expr tbl e)
   | Lasub(aa,ws,len,x,e)-> 
     C.Lasub (aa, ws, pos_of_int len, cvari_of_vari tbl x, cexpr_of_expr tbl e)
 
 let lval_of_clval tbl = function
-  | C.Lnone(p,ty)   -> Lnone (get_loc tbl p, ty_of_cty ty)
+  | C.Lnone(p, ty)  -> Lnone (p, ty_of_cty ty)
   | C.Lvar x        -> Lvar (vari_of_cvari tbl x)
   | C.Lmem(ws,x,e)  -> Lmem (ws, vari_of_cvari tbl x, expr_of_cexpr tbl e)
   | C.Laset(aa,ws,x,e) -> Laset (aa,ws, vari_of_cvari tbl x, expr_of_cexpr tbl e)
@@ -230,10 +218,9 @@ let string_of_funname tbl p =
 let set_iinfo tbl loc ii ia =
   let n = new_count tbl in
   Hashtbl.add tbl.iinfo n (loc, ii, ia);
-  pos_of_int n
+  n
 
 let get_iinfo tbl n =
-  let n = int_of_pos n in
   try Hashtbl.find tbl.iinfo n
   with Not_found ->
     Format.eprintf "WARNING: CAN NOT FIND IINFO %i@." n;
@@ -412,12 +399,11 @@ let to_array ty p t =
 (* ---------------------------------------------------------------------------- *)
 
 (* This avoids printing dummy locations. Hope that it will not hide errors. *)
-let patch_vi_loc tbl (e : Compiler_util.pp_error_loc) =
+let patch_vi_loc (e : Compiler_util.pp_error_loc) =
   match e.Compiler_util.pel_vi with
   | None -> e
   | Some vi ->
-    let l = get_loc tbl vi in
-    if L.isdummy l then { e with Compiler_util.pel_vi = None }
+    if L.isdummy vi then { e with Compiler_util.pel_vi = None }
     else e
 
 (* do we want more complex logic, e.g. if both vi and ii are <> None,
@@ -426,10 +412,9 @@ let patch_vi_loc tbl (e : Compiler_util.pp_error_loc) =
 *)
 let iloc_of_loc tbl e =
   let open Utils in
-  let e = patch_vi_loc tbl e in
+  let e = patch_vi_loc e in
   match e.pel_vi with
-  | Some vi ->
-    let loc = get_loc tbl vi in
+  | Some loc ->
     begin match e.pel_ii with
     | None -> Lone loc
     | Some ii ->

compiler/src/conv.mli

@@ -34,9 +34,8 @@ val z_of_word : wsize -> Obj.t -> Z.t
 (* -------------------------------------------------------------------- *)
 val cty_of_ty : Prog.ty -> Type.stype
 val ty_of_cty : Type.stype -> Prog.ty
-(* -------------------------------------------------------------------- *)
-val get_loc : 'a coq_tbl -> BinNums.positive -> L.t
 
+(* -------------------------------------------------------------------- *)
 val cvar_of_var : 'a coq_tbl -> var -> Var0.Var.var
 val var_of_cvar : 'a coq_tbl -> Var0.Var.var -> var
 val vari_of_cvari : 'a coq_tbl -> Expr.var_i -> var L.located
@@ -51,7 +50,7 @@ val fun_of_cfun : 'info coq_tbl -> BinNums.positive -> funname
 
 val string_of_funname : 'info coq_tbl -> BinNums.positive -> string
 
-val get_iinfo   : 'info coq_tbl -> BinNums.positive -> L.i_loc * 'info * Syntax.annotations
+val get_iinfo   : 'info coq_tbl -> Expr.instr_info -> L.i_loc * 'info * Syntax.annotations
 
 val get_finfo   : 'info coq_tbl -> BinNums.positive -> L.t * f_annot * call_conv * Syntax.annotations list
 

compiler/src/evaluator.ml

@@ -149,7 +149,7 @@ let init_state scs0 p fn m =
   { s_prog = p;
     s_cmd = f.f_body;
     s_estate = {escs = scs0; emem = m; evm = vmap0 };
-    s_stk = Sempty(Coq_xO Coq_xH, f) }
+    s_stk = Sempty(dummy_instr_info, f) }
 
 
 let exec pd sc_sem asmOp scs0 p fn m =

compiler/src/main_compiler.ml

@@ -267,7 +267,7 @@ let main () =
               in
               (match m_init with
                  | Utils0.Ok m -> m
-                 | Utils0.Error err -> raise (Evaluator.Eval_error (Coq_xH, err)))
+                 | Utils0.Error err -> raise (Evaluator.Eval_error (Expr.dummy_instr_info, err)))
               |>
               Evaluator.exec
                 Arch.reg_size

compiler/src/printer.ml

@@ -504,8 +504,7 @@ let pp_err ~debug tbl fmt (pp_e : Compiler_util.pp_error) =
     match pp_e with
     | Compiler_util.PPEstring s -> Format.fprintf fmt "%a" pp_string0 s
     | Compiler_util.PPEvar v -> Format.fprintf fmt "%a" (pp_var tbl) v
-    | Compiler_util.PPEvarinfo vi ->
-      let loc = Conv.get_loc tbl vi in
+    | Compiler_util.PPEvarinfo loc ->
       Format.fprintf fmt "%a" L.pp_loc loc
     | Compiler_util.PPEfunname fn -> Format.fprintf fmt "%s" (Conv.fun_of_cfun tbl fn).fn_name
     | Compiler_util.PPEiinfo ii ->

proofs/arch/asm_gen.v

@@ -289,7 +289,7 @@ Definition compile_arg rip ii (ade: (arg_desc * stype) * pexpr) (m: nmap asm_arg
   match ad.1 with
   | ADImplicit i =>
     Let _ :=
-      assert (eq_expr (Plvar (VarI (var_of_implicit i) xH)) e)
+      assert (eq_expr (Plvar (VarI (var_of_implicit i) dummy_var_info)) e)
              (E.internal_error ii "(compile_arg) bad implicit register") in
     ok m
   | ADExplicit k n o =>
@@ -316,7 +316,7 @@ Definition compat_imm ty a' a :=
 
 Definition check_sopn_arg rip ii (loargs : seq asm_arg) (x : pexpr) (adt : arg_desc * stype) :=
   match adt.1 with
-  | ADImplicit i => eq_expr x (Plvar (VarI (var_of_implicit i) xH))
+  | ADImplicit i => eq_expr x (Plvar (VarI (var_of_implicit i) dummy_var_info))
   | ADExplicit k n o =>
     match onth loargs n with
     | Some a =>
@@ -328,7 +328,7 @@ Definition check_sopn_arg rip ii (loargs : seq asm_arg) (x : pexpr) (adt : arg_d
 
 Definition check_sopn_dest rip ii (loargs : seq asm_arg) (x : pexpr) (adt : arg_desc * stype) :=
   match adt.1 with
-  | ADImplicit i => eq_expr x (Plvar (VarI (var_of_implicit i) xH))
+  | ADImplicit i => eq_expr x (Plvar (VarI (var_of_implicit i) dummy_var_info))
   | ADExplicit _ n o =>
     match onth loargs n with
     | Some a =>

proofs/arch/asm_gen_proof.v

@@ -234,7 +234,7 @@ Qed.
 
 Variant check_sopn_argI rip ii args e : arg_desc -> stype -> Prop :=
 | CSA_Implicit i ty :
-       (eq_expr e (Plvar {| v_var := var_of_implicit i; v_info := 1%positive |}))
+       (eq_expr e (Plvar {| v_var := var_of_implicit i; v_info := dummy_var_info |}))
     -> check_sopn_argI rip ii args e (ADImplicit i) ty
 
 | CSA_Explicit k n o a a' ty :
@@ -1572,7 +1572,7 @@ Proof.
     exists lc; first exact: omap_lc.
     constructor => //=; last by congr _.+1.
     move: ok_r_x.
-    change x with (v_var (VarI x xH)).
+    change x with (v_var (VarI x dummy_var_info)).
     apply: lom_eqv_write_var; first exact: eqm.
     by rewrite /write_var ok_vm.
   - t_xrbindP => cnd lbl cndt ok_c <- b v ok_v ok_b.

proofs/compiler/array_init.v

@@ -101,14 +101,11 @@ Section Section.
 
 Context (is_ptr : var -> bool).
 
-(* TODO: move *)
-Definition dummy_info := xH.
-
-Definition add_init_aux ii x c := 
+Definition add_init_aux ii x c :=
   match x.(vtype) with
   | sarr n =>
     if ~~ is_ptr x then
-      let x := VarI x dummy_info in
+      let x := VarI x dummy_var_info in
       MkI ii (Cassgn (Lvar x) AT_none (sarr n) (Parr_init n)) :: c
     else c
   | _ => c

proofs/compiler/linearization.v

@@ -236,7 +236,7 @@ Context
   (fn_align : wsize).
 
 Let rsp : var := Var (sword Uptr) (sp_rsp (p_extra p)).
-Let rspi : var_i := VarI rsp xH.
+Let rspi : var_i := VarI rsp dummy_var_info.
 Let rspg : gvar := Gvar rspi Slocal.
 Let var_tmp : var := Var (sword Uptr) (lip_tmp liparams).
 
@@ -335,7 +335,7 @@ Definition push_to_save
   : lcmd :=
   let mkli '(x, ofs) :=
     if is_word_type x.(vtype) is Some ws
-    then lstore ii rspi ofs ws {| gv := VarI x xH; gs := Slocal; |}
+    then lstore ii rspi ofs ws {| gv := VarI x dummy_var_info; gs := Slocal; |}
     else MkLI ii Lalign (* Absurd case. *)
   in List.map mkli to_save.
 
@@ -353,7 +353,7 @@ Definition pop_to_save
   : lcmd :=
   let mkli '(x, ofs) :=
     if is_word_type x.(vtype) is Some ws
-    then lload ii (VarI x xH) ws rspi ofs
+    then lload ii (VarI x dummy_var_info) ws rspi ofs
     else MkLI ii Lalign (* Absurd case. *)
   in List.map mkli to_save.
 
@@ -464,7 +464,7 @@ Fixpoint linear_i (i:instr) (lbl:label) (lc:lcmd) :=
            * 7. Continue.
            *)
           if extra_free_registers ii is Some ra
-          then let glob_ra := Gvar (VarI ra xH) Slocal in
+          then let glob_ra := Gvar (VarI ra dummy_var_info) Slocal in
                (lbl, before
                        ++ MkLI ii (LstoreLabel ra lret)
                        :: lstore ii rspi z Uptr glob_ra
@@ -484,13 +484,13 @@ Definition linear_body (e: stk_fun_extra) (body: cmd) : lcmd :=
   let: (tail, head, lbl) :=
      match sf_return_address e with
      | RAreg r =>
-       ( [:: MkLI xH (Ligoto (Pvar (Gvar (VarI r xH) Slocal))) ]
-       , [:: MkLI xH (Llabel 1) ]
+       ( [:: MkLI dummy_instr_info (Ligoto (Pvar (Gvar (VarI r dummy_var_info) Slocal))) ]
+       , [:: MkLI dummy_instr_info (Llabel 1) ]
        , 2%positive
        )
      | RAstack z =>
-       ( [:: MkLI xH (Ligoto (Pload Uptr rspi (cast_const z))) ]
-       , [:: MkLI xH (Llabel 1) ]
+       ( [:: MkLI dummy_instr_info (Ligoto (Pload Uptr rspi (cast_const z))) ]
+       , [:: MkLI dummy_instr_info (Llabel 1) ]
        , 2%positive
        )
      | RAnone =>
@@ -502,11 +502,11 @@ Definition linear_body (e: stk_fun_extra) (body: cmd) : lcmd :=
           * Head: R[x] := R[rsp]
           *       Setup stack.
           *)
-         let r := VarI x xH in
-         ( [:: lmove xH rspi Uptr (Gvar r Slocal) ]
-         , lmove xH r Uptr rspg
-             :: allocate_stack_frame false xH (sf_stk_sz e + sf_stk_extra_sz e)
-             ++ [:: ensure_rsp_alignment xH e.(sf_align) ]
+         let r := VarI x dummy_var_info in
+         ( [:: lmove dummy_instr_info rspi Uptr (Gvar r Slocal) ]
+         , lmove dummy_instr_info r Uptr rspg
+             :: allocate_stack_frame false dummy_instr_info (sf_stk_sz e + sf_stk_extra_sz e)
+             ++ [:: ensure_rsp_alignment dummy_instr_info e.(sf_align) ]
          , 1%positive
          )
        | SavedStackStk ofs =>
@@ -517,14 +517,14 @@ Definition linear_body (e: stk_fun_extra) (body: cmd) : lcmd :=
           *       M[R[rsp] + ofs] := R[r]
           *       Push registers to save to the stack.
           *)
-         let tmp := VarI var_tmp xH in
-         ( pop_to_save xH e.(sf_to_save)
-             ++ [:: lload xH rspi Uptr rspi ofs ]
-         , lmove xH tmp Uptr rspg
-             :: allocate_stack_frame false xH (sf_stk_sz e + sf_stk_extra_sz e)
-             ++ ensure_rsp_alignment xH e.(sf_align)
-             :: lstore xH rspi ofs Uptr (Gvar tmp Slocal)
-             :: push_to_save xH e.(sf_to_save)
+         let tmp := VarI var_tmp dummy_var_info in
+         ( pop_to_save dummy_instr_info e.(sf_to_save)
+             ++ [:: lload dummy_instr_info rspi Uptr rspi ofs ]
+         , lmove dummy_instr_info tmp Uptr rspg
+             :: allocate_stack_frame false dummy_instr_info (sf_stk_sz e + sf_stk_extra_sz e)
+             ++ ensure_rsp_alignment dummy_instr_info e.(sf_align)
+             :: lstore dummy_instr_info rspi ofs Uptr (Gvar tmp Slocal)
+             :: push_to_save dummy_instr_info e.(sf_to_save)
          , 1%positive)
        end
      end