fixed annotations on assembly output for assembly-checker (#1357)

* fixed assembly annotation bug

* included line numbers in assembly parsing errors.  changed type of line number from nat to N.

src/Assembly/Equality.v

@@ -296,7 +296,8 @@ Definition Line_beq (x y : Line) : bool
   := ((x.(indent) =? y.(indent))%string
       && (x.(rawline) =? y.(rawline))%RawLine
       && (x.(pre_comment_whitespace) =? y.(pre_comment_whitespace))%string
-      && option_beq String.eqb x.(comment) y.(comment))%bool.
+      && option_beq String.eqb x.(comment) y.(comment))%bool
+      && (x.(line_number) =? y.(line_number))%N.
 Global Arguments Line_beq !_ !_ / .
 
 Infix "=?" := Line_beq : Line_scope.

src/Assembly/Equivalence.v

@@ -212,8 +212,9 @@ Definition AnnotatedLines := (Lines * symbolic_state)%type.
 
 Definition show_annotated_Line : Show AnnotatedLine
   := fun '(l, d)
-     => let l := show l in
-        (l ++ match dag.eager.description_lookup d l with
+     => let l_n := show_Line_with_line_number l in
+        let l := show l in
+        (l ++ match dag.eager.description_lookup d l_n with
               | [] => ""
               | new_idxs
                 => String.Tab ++ "; " ++ String.concat ", " (List.map (fun i => "#" ++ show i) new_idxs)

src/Assembly/Parse.v

@@ -354,7 +354,7 @@ Definition parse_RawLine : ParserAction RawLine
                       parsed_prefix
                end.
 
-Definition parse_Line : ParserAction Line
+Definition parse_Line (line_num : N) : ParserAction Line
   := fun s
      => let '(indentv, rest_linev) := take_while_drop_while Ascii.is_whitespace s in
         let '(precommentv, commentv)
@@ -367,23 +367,24 @@ Definition parse_Line : ParserAction Line
         let rawlinev := String.rev rev_rawlinev in
         let trailing_whitespacev := String.rev rev_trailing_whitespacev in
         List.map
-          (fun '(r, rem) => ({| indent := indentv ; rawline := r ; pre_comment_whitespace := trailing_whitespacev ; comment := commentv |}, rem))
+          (fun '(r, rem) => ({| indent := indentv ; rawline := r ; pre_comment_whitespace := trailing_whitespacev ; comment := commentv ; line_number := line_num |}, rem))
           (parse_RawLine rawlinev).
 
 (* the error is the unparsable lines *)
-Fixpoint parse_Lines' (l : list string) : ErrorT (list string) Lines
+Fixpoint parse_Lines' (l : list string) (line_num : N) : ErrorT (list string) Lines
   := match l with
      | [] => Success []
      | l :: ls
-       => match finalize parse_Line l, parse_Lines' ls with
-          | None, Error ls => Error (l :: ls)
-          | None, Success _ => Error (l :: nil)
+       => match finalize (parse_Line line_num) l, parse_Lines' ls (line_num + 1) with
+          | None, Error ls => Error (("Line " ++ show line_num ++ ": " ++ l) :: ls)
+          | None, Success _ => Error (("Line " ++ show line_num ++ ": " ++ l) :: nil)
           | Some _, Error ls => Error ls
           | Some l, Success ls => Success (l :: ls)
           end
      end.
 
-Definition parse_Lines (l : list string) := parse_Lines' (String.split_newlines l).
+Definition parse_Lines (l : list string) : ErrorT (list string) Lines
+  := parse_Lines' (String.split_newlines l) 1.
 
 Notation parse := parse_Lines (only parsing).
 
@@ -465,6 +466,10 @@ Global Instance show_Line : Show Line
                                                                         | Some c => ";" ++ c
                                                                         | None => ""
                                                                         end.
+
+Definition show_Line_with_line_number : Show Line
+  := fun l => show l ++ "; (line " ++ show l.(line_number) ++ ")".
+
 Global Instance show_lines_Lines : ShowLines Lines
   := fun ls => List.map show ls.
 

src/Assembly/Symbolic.v

@@ -3484,7 +3484,7 @@ Definition SymexRawLine {descr:description} (rawline : RawLine) : M unit :=
   end.
 
 Definition SymexLine line :=
-  let descr:description := Build_description (show line) false in
+  let descr:description := Build_description (Parse.show_Line_with_line_number line) false in
   SymexRawLine line.(rawline).
 
 Fixpoint SymexLines (lines : Lines) : M unit

src/Assembly/Syntax.v

@@ -112,7 +112,7 @@ Inductive RawLine :=
 | INSTR (instr : NormalInstruction)
 .
 Coercion INSTR : NormalInstruction >-> RawLine.
-Record Line := { indent : string ; rawline :> RawLine ; pre_comment_whitespace : string ; comment : option string }.
+Record Line := { indent : string ; rawline :> RawLine ; pre_comment_whitespace : string ; comment : option string ; line_number : N}.
 Definition Lines := list Line.
 
 Definition reg_size (r : REG) : N :=