Attach more precise meta-data to variables introduced at compile-time

CHANGELOG.md

@@ -125,6 +125,10 @@
   ([PR #751](https://github.com/jasmin-lang/jasmin/pull/751);
   fixes [#750](https://github.com/jasmin-lang/jasmin/issues/750)).
 
+- Attach more precise meta-data to variables introduced at compile-time
+  ([PR #753](https://github.com/jasmin-lang/jasmin/pull/753);
+  fixes [#718](https://github.com/jasmin-lang/jasmin/issues/718)).
+
 ## Other changes
 
 - Pretty-printing of Jasmin programs is more precise

compiler/src/iInfo.ml

@@ -2,3 +2,4 @@ type t = Location.i_loc * Annotations.annotations
 let dummy = Location.i_dummy, []
 let with_location (l, _) = (l, [])
 let is_inline (_, annot) = Annotations.has_symbol "inline" annot
+let var_info_of_ii (l, _) = Location.(l.base_loc)

proofs/compiler/arm_lowering.v

@@ -74,8 +74,8 @@ Definition flags_of_mn (mn : arm_mnemonic) : seq var :=
   in
   map (fun x => x fv) ids.
 
-Definition lflags_of_mn (mn : arm_mnemonic) : seq lval :=
-  to_lvals (flags_of_mn mn).
+Definition lflags_of_mn (vi : var_info) (mn : arm_mnemonic) : seq lval :=
+  [seq Lvar {| v_var := x; v_info := vi; |} | x <- flags_of_mn mn ].
 
 Definition lower_TST (e0 e1 : pexpr) : option (seq pexpr) :=
   match e0, e1 with
@@ -87,13 +87,17 @@ Definition lower_TST (e0 e1 : pexpr) : option (seq pexpr) :=
 
 (* TODO_ARM: CMP and TST take register shifts. *)
 Definition lower_condition_Papp2
-  (op : sop2) (e0 e1 : pexpr) : option (arm_mnemonic * pexpr * seq pexpr) :=
+  (vi : var_info)
+  (op : sop2)
+  (e0 e1 : pexpr) :
+  option (arm_mnemonic * pexpr * seq pexpr) :=
   let%opt (cf, ws) := cf_of_condition op in
   let%opt _ := chk_ws_reg ws in
-  let cmp := (CMP, pexpr_of_cf cf (fresh_flags fv), [:: e0; e1 ]) in
+  let cmp := (CMP, pexpr_of_cf cf vi (fresh_flags fv), [:: e0; e1 ]) in
   match op with
   | Oeq (Op_w _) =>
-      let eZF := Pvar (mk_lvar (mk_var_i (fvZF fv))) in
+      let zf_var := {| v_var := fvZF fv; v_info := vi |} in
+      let eZF := Pvar (mk_lvar zf_var) in
       Some (if lower_TST e0 e1 is Some es then (TST, eZF, es) else cmp)
   | Oneq (Op_w _)
   | Olt (Cmp_w _ _)
@@ -105,13 +109,13 @@ Definition lower_condition_Papp2
   end.
 
 Definition lower_condition_pexpr
-  (e : pexpr) : option (seq lval * sopn * seq pexpr * pexpr) :=
+  (vi : var_info) (e : pexpr) : option (seq lval * sopn * seq pexpr * pexpr) :=
   let%opt (op, e0, e1) := is_Papp2 e in
-  let%opt (mn, e', es) := lower_condition_Papp2 op e0 e1 in
-  Some (lflags_of_mn mn, Oarm (ARM_op mn default_opts), es, e').
+  let%opt (mn, e', es) := lower_condition_Papp2 vi op e0 e1 in
+  Some (lflags_of_mn vi mn, Oarm (ARM_op mn default_opts), es, e').
 
-Definition lower_condition (e : pexpr) : seq instr_r * pexpr :=
-  if lower_condition_pexpr e is Some (lvs, op, es, c)
+Definition lower_condition (vi: var_info) (e : pexpr) : seq instr_r * pexpr :=
+  if lower_condition_pexpr vi e is Some (lvs, op, es, c)
   then ([:: Copn lvs AT_none op es ], c)
   else ([::], e).
 
@@ -304,12 +308,12 @@ Definition no_pre (ole : lowered_pexpr) :
   option (seq instr_r * arm_op * seq pexpr) :=
   let%opt (aop, es) := ole in Some ([::], aop, es).
 
-Definition lower_pexpr (ws : wsize) (e : pexpr) :
+Definition lower_pexpr (vi: var_info) (ws : wsize) (e : pexpr):
   option (seq instr_r * arm_op * seq pexpr) :=
   if e is Pif (sword ws') c e0 e1 then
     let%opt _ := oassert (ws == ws')%CMP in
     let%opt (ARM_op mn opts, es) := lower_pexpr_aux ws e0 in
-    let '(pre, c') := lower_condition c in
+    let '(pre, c') := lower_condition vi c in
     Some (pre, ARM_op mn (set_is_conditional opts), es ++ [:: c'; e1 ])
   else
     no_pre (lower_pexpr_aux ws e).
@@ -336,15 +340,17 @@ Definition lower_store (ws : wsize) (e : pexpr) : option (arm_op * seq pexpr) :=
 (* Convert an assignment into an architecture-specific operation. *)
 Definition lower_cassgn_word
   (lv : lval) (ws : wsize) (e : pexpr) : option (seq instr_r * copn_args) :=
+  let vi := var_info_of_lval lv in
   let%opt (pre, aop, es) :=
     if is_lval_in_memory lv
     then no_pre (lower_store ws e)
-    else lower_pexpr ws e
+    else lower_pexpr vi ws e
   in
   Some (pre, ([:: lv ], Oarm aop, es)).
 
 Definition lower_cassgn_bool (lv : lval) (tag: assgn_tag) (e : pexpr) : option (seq instr_r) :=
-  let%opt (lvs, op, es, c) := lower_condition_pexpr e in
+  let vi := var_info_of_lval lv in
+  let%opt (lvs, op, es, c) := lower_condition_pexpr vi e in
   Some [:: Copn lvs tag op es; Cassgn lv AT_inline sbool c ].
 
 (* -------------------------------------------------------------------- *)
@@ -468,7 +474,7 @@ Fixpoint lower_i (i : instr) : cmd :=
       [:: MkI ii ir' ]
 
   | Cif e c1 c2  =>
-      let '(pre, e') := lower_condition e in
+      let '(pre, e') := lower_condition (var_info_of_ii ii) e in
       let c1' := conc_map lower_i c1 in
       let c2' := conc_map lower_i c2 in
       map (MkI ii) (pre ++ [:: Cif e' c1' c2' ])
@@ -478,7 +484,7 @@ Fixpoint lower_i (i : instr) : cmd :=
       [:: MkI ii (Cfor v r c') ]
 
   | Cwhile a c0 e c1 =>
-      let '(pre, e') := lower_condition e in
+      let '(pre, e') := lower_condition (var_info_of_ii ii) e in
       let c0' := conc_map lower_i c0 in
       let c1' := conc_map lower_i c1 in
       [:: MkI ii (Cwhile a (c0' ++ map (MkI ii) pre) e' c1') ]

proofs/compiler/arm_lowering_proof.v

@@ -176,15 +176,15 @@ Proof.
   all: by move: fvars_NF fvars_ZF fvars_CF fvars_VF.
 Qed.
 
-Lemma sem_condition_mn ii tag mn s es ws0 ws1 (w0 : word ws0) (w1 : word ws1) :
+Lemma sem_condition_mn ii vi tag mn s es ws0 ws1 (w0 : word ws0) (w1 : word ws1) :
   mn \in condition_mnemonics
   -> (reg_size <= ws0)%CMP
   -> (reg_size <= ws1)%CMP
   -> sem_pexprs true (p_globs p) s es = ok [:: Vword w0; Vword w1 ]
   -> let w0' := zero_extend reg_size w0 in
      let w1' := zero_extend reg_size w1 in
      let aop := Oarm (ARM_op mn default_opts) in
-     let i := Copn (lflags_of_mn fv mn) tag aop es in
+     let i := Copn (lflags_of_mn fv vi mn) tag aop es in
      sem p' ev s [:: MkI ii i ] (estate_of_condition_mn mn s w0' w1').
 Proof.
   move=> hmn hws0 hws1 hsemes /=.
@@ -211,8 +211,8 @@ Proof.
     reflexivity.
 Qed.
 
-Lemma lower_condition_Papp2P s op e0 e1 mn e es v0 v1 v :
-  lower_condition_Papp2 fv op e0 e1 = Some (mn, e, es)
+Lemma lower_condition_Papp2P vi s op e0 e1 mn e es v0 v1 v :
+  lower_condition_Papp2 fv vi op e0 e1 = Some (mn, e, es)
   -> sem_pexpr true (p_globs p) s e0 = ok v0
   -> sem_pexpr true (p_globs p) s e1 = ok v1
   -> sem_sop2 op v0 v1 = ok v
@@ -334,8 +334,8 @@ Proof.
   by rewrite -word.wltuE leNgt.
 Qed.
 
-Lemma sem_lower_condition_pexpr tag s0 s0' ii e v lvs aop es c :
-  lower_condition_pexpr fv e = Some (lvs, aop, es, c)
+Lemma sem_lower_condition_pexpr vi tag s0 s0' ii e v lvs aop es c :
+  lower_condition_pexpr fv vi e = Some (lvs, aop, es, c)
   -> eq_fv s0' s0
   -> disj_fvars (read_e e)
   -> sem_pexpr true (p_globs p) s0 e = ok v
@@ -359,7 +359,7 @@ Proof.
     lower_condition_Papp2P h hsem0' hsem1' hsemop.
   clear h hsemop hsem0' hsem1'.
 
-  have /= hsem' := sem_condition_mn ii tag hmn hws0 hws1 hsemes.
+  have /= hsem' := sem_condition_mn ii vi tag hmn hws0 hws1 hsemes.
   clear hws0 hws1 hsemes.
 
   eexists;
@@ -370,8 +370,8 @@ Proof.
   exact: (estate_of_condition_mn_eq_fv s0' _ _ hmn).
 Qed.
 
-Lemma sem_lower_condition s0 s0' ii e v pre e' :
-  lower_condition fv e = (pre, e')
+Lemma sem_lower_condition vi s0 s0' ii e v pre e' :
+  lower_condition fv vi e = (pre, e')
   -> eq_fv s0' s0
   -> disj_fvars (read_e e)
   -> sem_pexpr true (p_globs p) s0 e = ok v
@@ -1048,8 +1048,8 @@ Lemma no_preP o pre aop es :
 Proof. case: o => //. by move=> [? ?] [<- <- <-]. Qed.
 
 Lemma sem_lower_pexpr
-  s0 s1 s0' ii ws ws' e pre aop es (w : word ws') lv tag :
-  lower_pexpr ws e = Some (pre, aop, es)
+  s0 s1 s0' ii vi ws ws' e pre aop es (w : word ws') lv tag :
+  lower_pexpr vi ws e = Some (pre, aop, es)
   -> eq_fv s0' s0
   -> (ws <= ws')%CMP
   -> disj_fvars (read_e e)

proofs/compiler/arm_stack_zeroization_proof.v

@@ -811,7 +811,7 @@ Proof.
       have hlinear: [elaborate
         is_linear_of lp fn
           (lc
-          ++ stack_zero_loop (mk_var_i (vid rspn)) lbl ws_align ws stk_max
+          ++ stack_zero_loop (vid rspn) lbl ws_align ws stk_max
           ++ [::])].
       + by rewrite cats0; exists lfd.
         subst top.
@@ -823,7 +823,7 @@ Proof.
       have hlinear: [elaborate
         is_linear_of lp fn
           (lc
-          ++ stack_zero_unrolled (mk_var_i (vid rspn)) ws_align ws stk_max
+          ++ stack_zero_unrolled (vid rspn) ws_align ws stk_max
           ++ [::])].
       + by rewrite cats0; exists lfd.
       have := stack_zero_unrolledP

proofs/compiler/array_init.v

@@ -91,7 +91,7 @@ Definition add_init_aux ii x c :=
   match x.(vtype) with
   | sarr n =>
     if ~~ is_ptr x then
-      let x := VarI x dummy_var_info in
+      let x := VarI x (var_info_of_ii ii) in
       MkI ii (Cassgn (Lvar x) AT_none (sarr n) (Parr_init n)) :: c
     else c
   | _ => c

proofs/compiler/x86_lowering.v

@@ -69,12 +69,6 @@ Definition fvars_correct p :=
       fv_cf != fv_zf &
       fv_sf != fv_zf].
 
-Definition var_info_of_lval (x: lval) : var_info :=
-  match x with
-  | Lnone i t => i
-  | Lvar x | Lmem _ x _ | Laset _ _ x _ | Lasub _ _ _ x _ => v_info x
-  end.
-
 Definition stype_of_lval (x: lval) : stype :=
   match x with
   | Lnone _ t => t
@@ -111,7 +105,7 @@ Definition lower_cond_classify vi (e: pexpr) :=
 
   let%opt (op, e0, e1) := is_Papp2 e in
   let%opt (cf, ws) := cf_of_condition op in
-  Some (lflags, ws, pexpr_of_cf cf vflags, e0, e1).
+  Some (lflags, ws, pexpr_of_cf cf vi vflags, e0, e1).
 
 Definition lower_condition vi (pe: pexpr) : seq instr_r * pexpr :=
   match lower_cond_classify vi pe with
@@ -601,12 +595,12 @@ Fixpoint lower_i (i:instr) : cmd :=
   | Cassgn l tg ty e => lower_cassgn ii l tg ty e
   | Copn l t o e => map (MkI ii) (lower_copn l t o e)
   | Cif e c1 c2  =>
-     let '(pre, e) := lower_condition dummy_var_info e in
+     let '(pre, e) := lower_condition (var_info_of_ii ii) e in
        map (MkI ii) (rcons pre (Cif e (conc_map lower_i c1) (conc_map lower_i c2)))
   | Cfor v (d, lo, hi) c =>
      [:: MkI ii (Cfor v (d, lo, hi) (conc_map lower_i c))]
   | Cwhile a c e c' =>
-     let '(pre, e) := lower_condition dummy_var_info e in
+     let '(pre, e) := lower_condition (var_info_of_ii ii) e in
        map (MkI ii) [:: Cwhile a ((conc_map lower_i c) ++ map (MkI dummy_instr_info) pre) e (conc_map lower_i c')]
   | _ =>   map (MkI ii) [:: ir]
   end.

proofs/compiler/x86_lowering_proof.v

@@ -282,7 +282,7 @@ Section PROOF.
     to_word ws v1 = ok w1 ->
     exists s',
       let: i := Copn lflags AT_none (Ox86 (CMP ws)) [:: e0; e1 ] in
-      let: e := pexpr_of_cf cf [:: vof; vcf; vsf; vzf ] in
+      let: e := pexpr_of_cf cf vi [:: vof; vcf; vsf; vzf ] in
       let: b := sem_combine_flags cf bof bcf bsf bzf in
       [/\ sem p' ev s [:: MkI ii i ] s'
         , eq_exc_fresh s' s
@@ -1358,7 +1358,8 @@ Section PROOF.
       move: x Hcond=> [i e'] Hcond.
       clear s2' Hw' Hs2'.
       move: Hv' => /=; t_xrbindP=> b bv Hbv Hb trv1 v1 Hv1 Htr1 trv2 v2 Hv2 Htr2 ?;subst v.
-      have [s2' [Hs2'1 Hs2'2 Hs2'3]] := lower_condition_corr ii Hcond Hs1' Hbv.
+      have [s2' [Hs2'1 Hs2'2 Hs2'3]] :=
+        lower_condition_corr ii Hcond Hs1' Hbv.
       have [s3' Hw' Hs3'] := eeq_exc_write_lval Hdisjl Hs2'2 Hw.
       exists s3'; split=> //.
       rewrite map_cat.
@@ -1746,7 +1747,7 @@ Section PROOF.
     move=> s1 s2 e c1 c2 Hz _ Hc ii /= Hdisj s1' Hs1' /=.
     move: Hdisj; rewrite /disj_fvars /x86_lowering.disj_fvars vars_I_if=> /disjoint_union [Hdisje /disjoint_union [Hc1 Hc2]].
     set x := lower_condition _ _ _.
-    have Hcond: x = lower_condition fv dummy_var_info e by [].
+    have Hcond: x = lower_condition fv (var_info_of_ii ii) e by [].
     move: x Hcond=> [i e'] Hcond.
     have [s2' [Hs2'1 Hs2'2 Hs2'3]] :=
       lower_condition_corr ii Hcond Hs1' (eeq_exc_sem_pexpr Hdisje Hs1' Hz).
@@ -1765,7 +1766,7 @@ Section PROOF.
     move=> s1 s2 e c1 c2 Hz _ Hc ii /= Hdisj s1' Hs1' /=.
     move: Hdisj; rewrite /disj_fvars /x86_lowering.disj_fvars vars_I_if=> /disjoint_union [Hdisje /disjoint_union [Hc1 Hc2]].
     set x := lower_condition _ _ _.
-    have Hcond: x = lower_condition fv dummy_var_info e by [].
+    have Hcond: x = lower_condition fv (var_info_of_ii ii) e by [].
     move: x Hcond=> [i e'] Hcond.
     have [s2' [Hs2'1 Hs2'2 Hs2'3]] :=
       lower_condition_corr ii Hcond Hs1' (eeq_exc_sem_pexpr Hdisje Hs1' Hz).
@@ -1784,7 +1785,7 @@ Section PROOF.
     move=> s1 s2 s3 s4 a c e c' _ Hc Hz _ Hc' _ Hwhile ii Hdisj s1' Hs1' /=.
     have := Hdisj; rewrite /disj_fvars /x86_lowering.disj_fvars vars_I_while=> /disjoint_union [Hdisje /disjoint_union [Hc1 Hc2]].
     set x := lower_condition _ _ _.
-    have Hcond: x = lower_condition fv dummy_var_info e by [].
+    have Hcond: x = lower_condition fv (var_info_of_ii ii) e by [].
     move: x Hcond=> [i e'] Hcond.
     have [s2' [Hs2'1 Hs2'2]] := Hc Hc1 _ Hs1'.
     have [s3' [Hs3'1 Hs3'2 Hs3'3]] :=
@@ -1811,7 +1812,7 @@ Section PROOF.
     move=> s1 s2 a c e c' _ Hc Hz ii Hdisj s1' Hs1' /=.
     move: Hdisj; rewrite /disj_fvars /x86_lowering.disj_fvars vars_I_while=> /disjoint_union [Hdisje /disjoint_union [Hc1 Hc2]].
     set x := lower_condition _ _ _.
-    have Hcond: x = lower_condition fv dummy_var_info e by [].
+    have Hcond: x = lower_condition fv (var_info_of_ii ii) e by [].
     move: x Hcond=> [i e'] Hcond.
     have [s2' [Hs2'1 Hs2'2]] := Hc Hc1 _ Hs1'.
     have [s3' [Hs3'1 Hs3'2 Hs3'3]] :=

proofs/lang/expr.v

@@ -269,8 +269,8 @@ Definition cf_of_condition (op : sop2) : option (combine_flags * wsize) :=
   | _ => None
   end.
 
-Definition pexpr_of_cf (cf : combine_flags) (flags : seq var) : pexpr :=
-  let eflags := [seq Plvar (mk_var_i x) | x <- flags ] in
+Definition pexpr_of_cf (cf : combine_flags) (vi : var_info) (flags : seq var) : pexpr :=
+  let eflags := [seq Plvar {| v_var := x; v_info := vi |} | x <- flags ] in
   PappN (Ocombine_flags cf) eflags.
 
 
@@ -296,6 +296,12 @@ Definition get_lvar (x: lval) : exec var :=
 
 Definition Lnone_b (vi : var_info) : lval := Lnone vi sbool.
 
+Definition var_info_of_lval (x: lval) : var_info :=
+  match x with
+  | Lnone i t => i
+  | Lvar x | Lmem _ x _ | Laset _ _ x _ | Lasub _ _ _ x _ => v_info x
+  end.
+
 (* ** Instructions
  * -------------------------------------------------------------------- *)
 
@@ -324,20 +330,23 @@ Module Type InstrInfoT <: TAG.
   Include TAG.
   Parameter with_location : t -> t.
   Parameter is_inline : t -> bool.
+  Parameter var_info_of_ii : t -> var_info.
 End InstrInfoT.
 
 Module InstrInfo : InstrInfoT.
   Definition t := positive.
   Definition witness : t := 1%positive.
   Definition with_location (ii : t) := ii.
   Definition is_inline (_ : t) : bool := false.
+  Definition var_info_of_ii (_ : t) : var_info := dummy_var_info.
 End InstrInfo.
 
 Definition instr_info := InstrInfo.t.
 Definition dummy_instr_info : instr_info := InstrInfo.witness.
 Definition ii_with_location (ii : instr_info) : instr_info :=
   InstrInfo.with_location ii.
 Definition ii_is_inline (ii : instr_info) : bool := InstrInfo.is_inline ii.
+Definition var_info_of_ii (ii : instr_info) : var_info := InstrInfo.var_info_of_ii ii.
 
 Variant assgn_tag :=
   | AT_none       (* assignment introduced by the developer that can be removed *)

proofs/lang/extraction.v

@@ -29,6 +29,7 @@ Extract Constant expr.InstrInfo.t => "IInfo.t".
 Extract Constant expr.InstrInfo.witness => "IInfo.dummy".
 Extract Constant expr.InstrInfo.with_location => "IInfo.with_location".
 Extract Constant expr.InstrInfo.is_inline => "IInfo.is_inline".
+Extract Constant expr.InstrInfo.var_info_of_ii => "IInfo.var_info_of_ii".
 Extract Constant expr.instr_info => "IInfo.t".
 Extract Constant expr.fun_info => "FInfo.t".
 Extract Constant waes.MixColumns => "(fun _ -> failwith ""MixColumns is not implemented"")".