expr: var_info are locations

CHANGELOG.md

@@ -32,7 +32,8 @@
 
 - Lowering of a memory-to-memory copy always introduce an intermediate copy through a register
 
-- `var_info` and `instr_info` are now plain OCaml `int`
+- `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

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 p
-  with Not_found -> L._dummy
-
-let set_loc tbl loc =
-  let n = new_count tbl in
-  Hashtbl.add tbl.vari n loc;
-  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)
@@ -411,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,
@@ -425,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 -> Expr.var_info -> 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

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/lang/expr.v

@@ -357,7 +357,10 @@ Definition wrange d (n1 n2 : Z) :=
   | DownTo => [seq (Z.sub n2 (Z.of_nat i)) | i <- iota 0 n]
   end.
 
-Module InstrInfo : TAG := VarInfo.
+Module InstrInfo : TAG.
+  Definition t := positive.
+  Definition witness : t := 1%positive.
+End InstrInfo.
 
 Definition instr_info := InstrInfo.t.
 Definition dummy_instr_info : instr_info := InstrInfo.witness.

proofs/lang/extraction.v

@@ -19,9 +19,11 @@ Extraction Inline Datatypes.implb.
 Extract Constant strings.ascii_beq => "Char.equal".
 Extract Constant strings.ascii_cmp => "(fun x y -> let c = Char.compare x y in if c = 0 then Datatypes.Eq else if c < 0 then Datatypes.Lt else Datatypes.Gt)".
 
-Extract Constant expr.VarInfo.t => "Stdlib.Int.t".
-Extract Constant expr.VarInfo.witness => "(-1)".
-Extract Constant expr.var_info => "Stdlib.Int.t".
+Extract Constant expr.VarInfo.t => "Location.t".
+Extract Constant expr.VarInfo.witness => "Location._dummy".
+Extract Constant expr.var_info => "Location.t".
+Extract Constant expr.InstrInfo.t => "Stdlib.Int.t".
+Extract Constant expr.InstrInfo.witness => "(-1)".
 Extract Constant expr.instr_info => "Stdlib.Int.t".
 
 Cd  "lang/ocaml".