New support for inserting ais-annotations.

The ais annotations can be inserted via the new ais variants of
the builtin annotation. They mainly differe in that they have an
address format specifier '%addr' which will be replaced by the
adress in the binary.

The implementation simply prints a label for the builtin call
alongside a the text of the annotation as comment and inserts the
annotation together as acii string in a separate section
'ais_annotations' and replaces the usages of the address format
specifiers by the address of the label of the builtin call.

1 files changed, 3 insertions, 3 deletions

diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index fef74706..8336d1bf 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -132,7 +132,7 @@ Inductive wt_instr : instruction -> Prop :=
   | wt_Ibuiltin:
       forall ef args res s,
       match ef with
-      | EF_annot _ _ | EF_debug _ _ _ => True
+      | EF_annot _ _ _ | EF_debug _ _ _ => True
       | _ => map type_of_builtin_arg args = (ef_sig ef).(sig_args)
       end ->
       type_of_builtin_res res = proj_sig_res (ef_sig ef) ->
@@ -308,7 +308,7 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv :=
       do x <- check_successor s;
       do e1 <-
         match ef with
-        | EF_annot _ _ | EF_debug _ _ _ => OK e
+        | EF_annot _ _ _ | EF_debug _ _ _ => OK e
         | _ => type_builtin_args e args sig.(sig_args)
         end;
       type_builtin_res e1 res (proj_sig_res sig)
@@ -702,7 +702,7 @@ Proof.
   exploit type_builtin_res_complete; eauto. instantiate (1 := res). intros [e2 [C D]].
   exploit type_builtin_res_complete. eexact H. instantiate (1 := res). intros [e3 [E F]].
   rewrite check_successor_complete by auto. simpl.
-  exists (match ef with EF_annot _ _ | EF_debug _ _ _ => e3 | _ => e2 end); split.
+  exists (match ef with EF_annot _ _ _ | EF_debug _ _ _ => e3 | _ => e2 end); split.
   rewrite H1 in C, E.
   destruct ef; try (rewrite <- H0; rewrite A); simpl; auto.
   destruct ef; auto.