Extract instr_info & var_info to standard OCaml int

CHANGELOG.md

@@ -32,6 +32,9 @@
 
 - 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`
+   ([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

@@ -122,13 +122,13 @@ let var_of_cvar tbl cv =
 (* ------------------------------------------------------------------------ *)
 
 let get_loc tbl p =
-  try Hashtbl.find tbl.vari (int_of_pos 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;
-  pos_of_int n
+  n
 
 let cvari_of_vari tbl v =
   let p = set_loc tbl (L.loc v) in
@@ -230,10 +230,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;

compiler/src/conv.mli

@@ -35,7 +35,7 @@ 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 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
@@ -51,7 +51,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

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

proofs/compiler/linearization_proof.v

@@ -346,7 +346,7 @@ Record h_linearization_params :=
       forall (lp : lprog) (s : estate) sp_rsp ii fn pc ts sz,
         let rsp := vid sp_rsp in
         let vm := evm s in
-        let args := lip_allocate_stack_frame liparams (VarI rsp xH) sz in
+        let args := lip_allocate_stack_frame liparams (VarI rsp dummy_var_info) sz in
         let i := MkLI ii (Lopn args.1.1 args.1.2 args.2) in
         let ts' := pword_of_word (ts + wrepr Uptr sz) in
         let s' := with_vm s (vm.[rsp <- ok ts'])%vmap in
@@ -358,7 +358,7 @@ Record h_linearization_params :=
       forall (lp : lprog) (s : estate) sp_rsp ii fn pc ts sz,
         let rsp := vid sp_rsp in
         let vm := evm s in
-        let args := lip_free_stack_frame liparams (VarI rsp xH) sz in
+        let args := lip_free_stack_frame liparams (VarI rsp dummy_var_info) sz in
         let i := MkLI ii (Lopn args.1.1 args.1.2 args.2) in
         let ts' := pword_of_word (ts - wrepr Uptr sz) in
         let s' := with_vm s (vm.[rsp <- ok ts'])%vmap in
@@ -369,7 +369,7 @@ Record h_linearization_params :=
     spec_lip_ensure_rsp_alignment :
       forall (lp : lprog) (s : estate) rsp_id ii fn pc ws ts',
         let vrsp := Var (sword Uptr) rsp_id in
-        let vrspi := VarI vrsp xH in
+        let vrspi := VarI vrsp dummy_var_info in
         let rsp' := align_word ws ts' in
         let args := lip_ensure_rsp_alignment liparams vrspi ws in
         let i := MkLI ii (Lopn args.1.1 args.1.2 args.2) in
@@ -1312,7 +1312,7 @@ Section PROOF.
       mapM (get_var vm2) xs = ok vs2 & List.Forall2 value_uincl vs1 vs2.
   Proof.
     move=> h1 h2;
-    have := get_vars_uincl (xs := map (fun x => {| v_var := x; v_info := xH |}) xs) h1.
+    have := get_vars_uincl (xs := map (fun x => {| v_var := x; v_info := dummy_var_info |}) xs) h1.
     by rewrite !mapM_map => /(_ _ h2).
   Qed.
 
@@ -2697,7 +2697,7 @@ Section PROOF.
           by case: _.[_]%vmap => //= - [] sz w ? /pword_of_word_uincl[] /= ? -> {w}; subst.
         set vm_save := vm1.[{| vtype := spointer; vname := saved_stack |} <- ok (pword_of_word (top_stack (emem s1)))]%vmap.
         set sf_sz := (sf_stk_sz _ + _)%Z.
-        set alloc := allocate_stack_frame p liparams false xH sf_sz.
+        set alloc := allocate_stack_frame p liparams false dummy_instr_info sf_sz.
         have :
           ∃ vm, [/\
             lsem
@@ -2713,7 +2713,7 @@ Section PROOF.
                  lvm := vm;
                  lfn := fn;
                  lpc := size
-                   ((head {| li_ii := xH; li_i := Lalign; |} P) :: alloc) + 0;
+                   ((head {| li_ii := dummy_instr_info; li_i := Lalign; |} P) :: alloc) + 0;
               |}
             , wf_vm vm
             , vm = vm_save [\ Sv.singleton vrsp ]
@@ -2781,7 +2781,7 @@ Section PROOF.
             (s := {| escs:= escs s1; evm := vm; emem := m1; |})
             hliparams
             p'
-            xH
+            dummy_instr_info
             fn
             ((size alloc).+1 + 0)
             (sf_align (f_extra fd))
@@ -2860,9 +2860,9 @@ Section PROOF.
             set ws := sf_align (f_extra fd).
             replace (P ++ lbody ++ Q) with
                 ((head
-                    {| li_ii := xH; li_i := Lalign; |}
-                    P :: allocate_stack_frame p liparams false xH sz)
-                  ++ [:: ensure_rsp_alignment p liparams xH ws ]
+                    {| li_ii := dummy_instr_info; li_i := Lalign; |}
+                    P :: allocate_stack_frame p liparams false dummy_instr_info sz)
+                  ++ [:: ensure_rsp_alignment p liparams dummy_instr_info ws ]
                   ++ lbody
                   ++ Q);
               last by rewrite /P /= -catA.
@@ -2992,7 +2992,7 @@ Section PROOF.
             (s := {| escs:= escs s1; evm := vm_rsp; emem := m1; |})
             hliparams
             p'
-            xH
+            dummy_instr_info
             fn
             ((1 + 0).+1)
             (sf_align (f_extra fd))
@@ -3147,7 +3147,7 @@ Section PROOF.
           rewrite read_in_m3; last lia.
           by rewrite -topE (writeP_eq ok_m2).
         have :
-          let: tail := pop_to_save p liparams xH (sf_to_save (f_extra fd)) in
+          let: tail := pop_to_save p liparams dummy_instr_info (sf_to_save (f_extra fd)) in
           exists vm5,
             [/\
                lsem
@@ -3302,9 +3302,9 @@ Section PROOF.
             replace (P ++ lbody ++ Q)
             with
               (take 2 P
-              ++ [:: ensure_rsp_alignment p liparams xH (sf_align (f_extra fd)),
-                     lstore liparams xH (VarI vrsp xH) stack_saved_rsp Uptr (mk_lvar var_tmp) &
-                     push_to_save p liparams xH (sf_to_save (f_extra fd)) ] ++ lbody ++ Q);
+              ++ [:: ensure_rsp_alignment p liparams dummy_instr_info (sf_align (f_extra fd)),
+                     lstore liparams dummy_instr_info (VarI vrsp dummy_var_info) stack_saved_rsp Uptr (mk_lvar var_tmp) &
+                     push_to_save p liparams dummy_instr_info (sf_to_save (f_extra fd)) ] ++ lbody ++ Q);
               last by rewrite /P catA.
             move => /find_instr_skip -> /=.
             rewrite -/vm_save -/vm_rsp.
@@ -3315,8 +3315,8 @@ Section PROOF.
             replace (P ++ lbody ++ Q)
             with
               (take 3 P
-              ++ [:: lstore liparams xH (VarI vrsp xH) stack_saved_rsp Uptr (mk_lvar var_tmp) &
-                      push_to_save p liparams xH (sf_to_save (f_extra fd)) ] ++ lbody ++ Q);
+              ++ [:: lstore liparams dummy_instr_info (VarI vrsp dummy_var_info) stack_saved_rsp Uptr (mk_lvar var_tmp) &
+                      push_to_save p liparams dummy_instr_info (sf_to_save (f_extra fd)) ] ++ lbody ++ Q);
               last by rewrite /P catA.
             move => /find_instr_skip -> /=.
             rewrite /lstore.
@@ -3601,7 +3601,7 @@ Section PROOF.
     set k' := Sv.union k (Sv.union match fd.(f_extra).(sf_return_address) with RAreg ra => Sv.singleton ra | RAstack _ => Sv.empty | RAnone => Sv.add var_tmp vflags end (if fd.(f_extra).(sf_save_stack) is SavedStackReg r then Sv.singleton r else Sv.empty)).
     set s1 := {| escs := scs; emem := m ; evm := vm |}.
     set s2 := {| escs := scs'; emem := free_stack m2 ; evm := set_RSP p (free_stack m2) vm2 |}.
-    have {sexec} /linear_fdP : sem_call p extra_free_registers var_tmp 1%positive k' s1 fn s2.
+    have {sexec} /linear_fdP : sem_call p extra_free_registers var_tmp dummy_instr_info k' s1 fn s2.
     - econstructor.
       + exact: ok_fd.
       + by rewrite /ra_valid; move/eqP: Export => ->.

proofs/compiler/merge_varmaps_proof.v

@@ -963,7 +963,7 @@ Lemma merge_varmaps_export_callP scs m fn args scs' m' res :
   sem_one_varmap.sem_export_call p extra_free_registers var_tmp global_data scs m fn args scs' m' res.
 Proof.
   case => fd ok_fd Export.
-  move => /merge_varmaps_callP /(_ 1%positive fd _ _ ok_fd).
+  move => /merge_varmaps_callP /(_ dummy_instr_info fd _ _ ok_fd).
 
   case: (checkP ok_p ok_fd) => _ok_wrf.
   rewrite /check_fd; t_xrbindP => D.

proofs/compiler/remove_globals.v

@@ -327,7 +327,7 @@ Section REMOVE.
     Definition remove_glob_fundef (f:ufundef) :=
       let env := Mvar.empty _ in
       let check_var xi :=
-        if is_glob xi.(v_var) then Error (rm_glob_error xH xi) else ok tt in
+        if is_glob xi.(v_var) then Error (rm_glob_error dummy_instr_info xi) else ok tt in
       Let _ := mapM check_var f.(f_params) in
       Let _ := mapM check_var f.(f_res) in
       Let envc := remove_glob remove_glob_i env f.(f_body) in

proofs/compiler/tunneling.v

@@ -58,7 +58,7 @@ End LprogSem.
 
 Section Tunneling.
 
-  Definition Linstr_align := (MkLI xH Lalign).
+  Definition Linstr_align := (MkLI dummy_instr_info Lalign).
 
   Definition tunnel_chart fn uf c c' :=
     match c, c' with