Compiler: emit DWARF2 line number information

CHANGELOG.md

@@ -43,6 +43,10 @@
   against Spectre).
   ([PR #631](https://github.com/jasmin-lang/jasmin/pull/631)).
 
+- Interleave references to source-code positions within the assembly listings
+  when the `-g` command-line flag is given (off by default).
+  ([PR #684](https://github.com/jasmin-lang/jasmin/pull/684)).
+
 ## Bug fixes
 
 - Type-checking rejects invalid variants of primitive operators

compiler/scripts/check-arm-m4

@@ -10,6 +10,6 @@ trap "rm -r ${DIR}" EXIT
 
 set -x
 
-$(dirname $0)/../jasminc -arch arm-m4 -o ${ASM} "$@"
+$(dirname $0)/../jasminc -g -arch arm-m4 -o ${ASM} "$@"
 
 llvm-mc --triple=armv7m --mcpu=cortex-m4 --filetype=obj -o ${OBJ} ${ASM}

compiler/scripts/check-x86-64

@@ -11,7 +11,7 @@ trap "rm -r ${DIR}" EXIT
 
 set -x
 
-$(dirname $0)/../jasminc -o ${ASM} "$@"
+$(dirname $0)/../jasminc -g -o ${ASM} "$@"
 # Negative test cases should have failed by now
 # Succeed early if it’s not the case (i.e., do not try to assemble the result)
 (echo $@ | grep -q fail) && exit 0

compiler/src/debugInfo.ml

@@ -0,0 +1,26 @@
+open Utils
+open Location
+open Format
+
+(** Give a unique number to the given file name.
+    Second return value is true the first time this file name is seed. *)
+let internFile =
+  (* TODO: remove global mutable state *)
+  let count = ref 0 in
+  let internedFiles = Hashtbl.create 17 in
+  fun s ->
+    match Hashtbl.find internedFiles s with
+    | v -> (v, false)
+    | exception Not_found ->
+        incr count;
+        let v = !count in
+        Hashtbl.add internedFiles s v;
+        (v, true)
+
+let source_positions ii =
+  if (not !Glob_options.dwarf) || Location.isdummy ii then []
+  else
+    let n, isFresh = internFile ii.loc_fname in
+    let line, col = ii.loc_start in
+    let loc = [ asprintf ".loc %d %d %d\n" n line col ] in
+    if isFresh then asprintf ".file %d %S\n" n ii.loc_fname :: loc else loc

compiler/src/debugInfo.mli

@@ -0,0 +1,2 @@
+val source_positions : Location.t -> string list
+(** List of .file and .loc directives to decorate assembly listings. *)

compiler/src/glob_options.ml

@@ -4,6 +4,7 @@ let version_string = "Jasmin Compiler @VERSION@"
 (*--------------------------------------------------------------------- *)
 let outfile = ref ""
 let latexfile = ref ""
+let dwarf = ref false
 let debug = ref false
 let timings = ref false
 let print_list = ref []
@@ -196,6 +197,7 @@ let stop_after_option p =
 let options = [
     "-version" , Arg.Set help_version  , "display version information about this compiler (and exits)";
     "-o"       , Arg.Set_string outfile, "[filename]: name of the output file";
+    "-g"       , Arg.Set dwarf         , "emit DWARF2 line number information";
     "-debug"   , Arg.Set debug         , ": print debug information";
     "-timings" , Arg.Set timings       , ": print a timestamp and elapsed time after each pass";
     "-I"       , Arg.String set_idirs  , "[ident:path]: bind ident to path for from ident require ...";

compiler/src/pp_arm_m4.ml

@@ -294,7 +294,12 @@ let pp_instr fn _ i =
 
 (* -------------------------------------------------------------------- *)
 
-let pp_body fn fmt cmd = List.concat_map (pp_instr fn fmt) cmd
+let pp_body fn fmt =
+  let open List in
+  concat_map @@ fun { asmi_i = i ; asmi_ii = (ii, _) } ->
+  append
+    (map (fun i -> LInstr (i, [])) (DebugInfo.source_positions ii.base_loc))
+    (pp_instr fn fmt i)
 
 (* -------------------------------------------------------------------- *)
 (* TODO_ARM: This is architecture-independent. *)

compiler/src/pp_arm_m4.mli

@@ -10,7 +10,7 @@ val print_instr :
      , Arm_decl_core.rflag
      , Arm_decl.condt
      , Arm_instr_decl.arm_op )
-     Arch_decl.asm_i
+     Arch_decl.asm_i_r
   -> unit
 
 val print_prog :

compiler/src/ppasm.ml

@@ -407,7 +407,7 @@ module Printer (BP:BPrinter) = struct
     | Syscall_t.RandomBytes _ -> "__jasmin_syscall_randombytes__"
 
   (* -------------------------------------------------------------------- *)
-  let pp_instr name (i : (_, _, _, _, _, _) Arch_decl.asm_i) =
+  let pp_instr name (i : (_, _, _, _, _, _) Arch_decl.asm_i_r) =
     match i with
     | ALIGN ->
       `Instr (".p2align", ["5"])
@@ -445,11 +445,17 @@ module Printer (BP:BPrinter) = struct
       let name = pp_name_ext pp in
       let args = pp_asm_args pp.pp_aop_args in
       `Instr(name, args)
-
+
+  (* -------------------------------------------------------------------- *)
+  let pp_ii ({ Location.base_loc = ii; _}, _) =
+    List.map (fun i -> `Instr(i, [])) (DebugInfo.source_positions ii)
+
   (* -------------------------------------------------------------------- *)
   let pp_instr name (fmt : Format.formatter) (i : (_, _, _, _, _, _) Arch_decl.asm_i) =
+    let Arch_decl.({ asmi_i = i ; asmi_ii = ii }) = i in
+    List.iter (pp_gen fmt) (pp_ii ii);
     pp_gen fmt (pp_instr name i)
-  
+
   (* -------------------------------------------------------------------- *)
   let pp_instrs name (fmt : Format.formatter) (is : (_, _, _, _, _, _) Arch_decl.asm_i list) =
     List.iter (Format.fprintf fmt "%a\n%!" (pp_instr name)) is

proofs/arch/arch_decl.v

@@ -14,6 +14,7 @@ Require Import
   strings
   syscall
   utils
+  expr
   word.
 Require Import
   sopn
@@ -521,7 +522,7 @@ Definition instr_desc (o:asm_op_msb_t) : instr_desc_t :=
 
 (* -------------------------------------------------------------------- *)
 (* Assembly language. *)
-Variant asm_i : Type :=
+Variant asm_i_r : Type :=
   | ALIGN
   | LABEL of label_kind & label
   | STORELABEL of reg_t & label (* Store the address of a local label *)
@@ -537,6 +538,8 @@ Variant asm_i : Type :=
   | AsmOp  of asm_op_t' & asm_args
   | SysCall of syscall_t.
 
+Record asm_i : Type := MkAI { asmi_ii : instr_info; asmi_i : asm_i_r }.
+
 Definition asm_code := seq asm_i.
 
 (* Any register, used for function arguments and returned values. *)

proofs/arch/arch_sem.v

@@ -154,7 +154,7 @@ Definition st_update_next (m:asmmem) (s : asm_state) :=
 
 (* -------------------------------------------------------------------- *)
 Definition is_label (lbl: label) (i: asm_i) : bool :=
-  match i with
+  match asmi_i i with
   | LABEL _ lbl' => lbl == lbl'
   | _ => false
   end.
@@ -407,7 +407,7 @@ Section PROG.
 Context  (p: asm_prog).
 
 Definition label_in_asm (body: asm_code) : seq label :=
-  pmap (λ i, if i is LABEL ExternalLabel lbl then Some lbl else None) body.
+  pmap (λ i, if asmi_i i is LABEL ExternalLabel lbl then Some lbl else None) body.
 
 Definition label_in_asm_prog : seq remote_label :=
   [seq (f.1, lbl) | f <- asm_funcs p, lbl <- label_in_asm (asm_fd_body f.2) ].
@@ -416,11 +416,11 @@ Definition label_in_asm_prog : seq remote_label :=
 Notation labels := label_in_asm_prog.
 
 Definition return_address_from (s: asm_state) : option (word Uptr) :=
-  if oseq.onth s.(asm_c) s.(asm_ip).+1 is Some (LABEL ExternalLabel lbl) then
+  if oseq.onth s.(asm_c) s.(asm_ip).+1 is Some {| asmi_i := LABEL ExternalLabel lbl |} then
     encode_label labels (asm_f s, lbl)
   else None.
 
-Definition eval_instr (i : asm_i) (s: asm_state) : exec asm_state :=
+Definition eval_instr (i : asm_i_r) (s: asm_state) : exec asm_state :=
   match i with
   | ALIGN
   | LABEL _ _    => ok (st_write_ip (asm_ip s).+1 s)
@@ -461,7 +461,7 @@ Definition eval_instr (i : asm_i) (s: asm_state) : exec asm_state :=
 (* -------------------------------------------------------------------- *)
 Definition fetch_and_eval (s: asm_state) :=
   if oseq.onth s.(asm_c) s.(asm_ip) is Some i then
-    eval_instr i s
+    eval_instr i.(asmi_i) s
   else type_error.
 
 Definition asmsem1 (s1 s2: asm_state) : Prop :=
@@ -532,7 +532,7 @@ Proof.
   by transitivity s1.
 Qed.
 
-Lemma eval_instr_invariant (i: asm_i) (s s': asm_state) :
+Lemma eval_instr_invariant (i: asm_i_r) (s s': asm_state) :
   eval_instr i s = ok s' →
   s ≡ s'.
 Proof.

proofs/arch/asm_gen.v

@@ -497,47 +497,48 @@ Definition is_not_app1 e : bool :=
 
 Definition assemble_i (rip : var) (i : linstr) : cexec (seq asm_i) :=
   let '{| li_ii := ii; li_i := ir; |} := i in
+  let mk i := {| asmi_i := i ; asmi_ii := ii |} in
   match ir with
   | Lopn ds op es =>
       Let args := assemble_sopn rip ii op ds es in
-      ok (map (fun x => AsmOp x.1 x.2) args)
+      ok (map (fun x => mk (AsmOp x.1 x.2)) args)
 
   | Lalign =>
-      ok [:: ALIGN ]
+      ok [:: mk ALIGN ]
 
   | Llabel k lbl =>
-      ok [:: LABEL k lbl ]
+      ok [:: mk (LABEL k lbl) ]
 
   | Lgoto lbl =>
-      ok [:: JMP lbl ]
+      ok [:: mk (JMP lbl) ]
 
   | Ligoto e =>
       Let _ := assert (is_not_app1 e) (E.werror ii e "Ligoto/JMPI") in
       Let arg := assemble_word AK_mem rip ii Uptr e in
-      ok [:: JMPI arg ]
+      ok [:: mk (JMPI arg) ]
 
   | LstoreLabel x lbl =>
       Let dst := if of_var x is Some r then ok r else Error (fail ii "bad var") in
-      ok [:: STORELABEL dst lbl ]
+      ok [:: mk (STORELABEL dst lbl) ]
 
   | Lcond e l =>
       Let cond := assemble_cond ii e in
-      ok [:: Jcc l cond ]
+      ok [:: mk (Jcc l cond) ]
 
   | Lsyscall o =>
-      ok [:: SysCall o ]
+      ok [:: mk (SysCall o) ]
 
   | Lcall None l =>
-      ok [:: CALL l ]
+      ok [:: mk (CALL l) ]
 
   | Lcall (Some r) l =>
-    Let r := 
+    Let r :=
       if to_reg r is Some r then ok r
       else Error (E.verror true "Not a register" ii r) in
-      ok [:: JAL r l ]
+      ok [:: mk (JAL r l) ]
 
   | Lret =>
-      ok [:: POPPC ]
+      ok [:: mk POPPC ]
 
   end.
 

proofs/arch/asm_gen_proof.v

@@ -1213,7 +1213,7 @@ Proof.
   rewrite -(cat1s i1) flatten_cat find_cat.
   rewrite -(cat1s i) find_cat /= cats0 -(assemble_i_is_label lbl hi1).
   case heq: linear.is_label => /=.
-  + by case: i hi1 heq => [? []] //= lk l [<-]; rewrite /linear.is_label /= => ->.
+  + by case: i hi1 heq => [? []] //= lk l [<-]; rewrite /linear.is_label /is_label /= => ->.
   rewrite /assemble_c /= hi1 /=.
   have heq1 := mapM_take (find (linear.is_label lbl) lc) hlc.
   by have := hrec _ hlc; rewrite /assemble_c heq1 /= size_cat => ->.
@@ -1445,7 +1445,8 @@ Lemma assemble_get_label_after_pc i ai lc xs ls l:
   → lfn ls = asm_f xs
   → asm_pos rip (lpc ls) lc = asm_ip xs
   → ssrfun.omap lfd_body (get_fundef (lp_funcs p) (lfn ls)) = Some lc
-  → get_label_after_pc p ls = ok l → onth (asm_c xs) (asm_ip xs).+1 = Some (LABEL ExternalLabel l).
+  → get_label_after_pc p ls = ok l
+  → ∃ ii, onth (asm_c xs) (asm_ip xs).+1 = Some {| asmi_i := LABEL ExternalLabel l ; asmi_ii := ii |}.
 Proof.
   move=> eqc honth hassi eqfn eqpc omap_lc; rewrite /get_label_after_pc /find_instr /= -eqpc.
   case: get_fundef omap_lc => // _ [->] {eqpc}; move: eqc.
@@ -1455,12 +1456,12 @@ Proof.
   case: (ltnP (lpc ls) (size lc)) honth => [hn ok_i| /onth_default -> //].
   rewrite !ltnn !subnn take0 cats0 hc1 /= -cat_rcons flatten_cat onth_cat.
   rewrite flatten_rcons size_cat /= addn1 ltnn subnn.
-  by case: drop hc2 => //= -[ii []//=] []// lbl c2'; t_xrbindP => ? _ <- <-.
+  by case: drop hc2 => //= -[ii []//=] []// lbl c2'; t_xrbindP => ? _ <- <-; eexists.
 Qed.
 
 Lemma match_state_step1 xs ls' i:
   onth (asm_c xs) (asm_ip xs) = Some i ->
-  (exists2 xs', arch_sem.eval_instr p' i xs = ok xs'
+  (exists2 xs', arch_sem.eval_instr p' i.(asmi_i) xs = ok xs'
      & exists2 lc', ssrfun.omap lfd_body (get_fundef (lp_funcs p) (lfn ls')) = Some lc'
          & match_state rip ls' lc' xs') ->
   (exists2 xs', asmsem p' xs xs'
@@ -1487,9 +1488,9 @@ Proof.
     by rewrite cats0 flatten_cat /= cats0 size_cat size_map.
 Qed.
 
-Lemma step_AsmOp fd ac0 ac1 c c' ls s xm xm' :
+Lemma step_AsmOp fd ii ac0 ac1 c c' ls s xm xm' :
   let: xbody :=
-    flatten ac0 ++ [seq AsmOp x.1 x.2 | x <- c' ++ c] ++ flatten ac1
+    flatten ac0 ++ [seq {| asmi_ii := ii ; asmi_i := AsmOp x.1 x.2 |} | x <- c' ++ c] ++ flatten ac1
   in
   let: pc := (size (flatten ac0) + size c')%nat in
   let: xs :=
@@ -1545,9 +1546,9 @@ Lemma match_state_SysCall fd ls ls' ii sc ac0 ac1 xs :
   lfn ls = asm_f xs ->
   assemble_c agparams rip (lfd_body fd) = ok (asm_c xs) ->
   mapM (assemble_i agparams rip) (take (lpc ls) (lfd_body fd)) = ok ac0 ->
-  flatten ac0 ++ [:: SysCall sc ] ++ flatten ac1 = asm_c xs ->
+  flatten ac0 ++ [:: {| asmi_ii := ii ; asmi_i := SysCall sc |} ] ++ flatten ac1 = asm_c xs ->
   asm_pos rip (lpc ls) (lfd_body fd) = asm_ip xs ->
-  onth (asm_c xs) (asm_ip xs) = onth (SysCall sc :: flatten ac1) 0 ->
+  onth (asm_c xs) (asm_ip xs) = onth ({| asmi_ii := ii ; asmi_i := SysCall sc |} :: flatten ac1) 0 ->
   onth (lfd_body fd) (lpc ls) = Some li ->
   linear_sem.eval_instr p li ls = ok ls' ->
   exists2 xs',
@@ -1750,7 +1751,7 @@ Proof.
       apply (match_state_step1 (ls' := ls') hnth) => /=.
       rewrite /return_address_from.
       have /= := assemble_get_label_after_pc hass ok_i _ heqf hip _ hgetpc.
-      rewrite heqlr ok_fd /= => /(_ _ erefl erefl) ->.
+      rewrite heqlr ok_fd /= => /(_ _ erefl erefl) [] _ ->.
       rewrite -assemble_prog_labels -heqf ptr_eq.
       apply: eval_jumpP; last by apply hjump.
       rewrite /st_update_next /=.
@@ -1765,7 +1766,7 @@ Proof.
     apply (match_state_step1 (ls' := ls') hnth) => /=.
     rewrite /return_address_from.
     have /= := assemble_get_label_after_pc hass ok_i _ heqf hip _ hgetpc.
-    rewrite ok_fd /= => /(_ _ erefl erefl) ->.
+    rewrite ok_fd /= => /(_ _ erefl erefl) [] _ ->.
     rewrite -assemble_prog_labels ptr_eq.
     rewrite /eval_PUSH truncate_word_u /=.
     rewrite to_var_rsp in hsp.