From 8f750f2d4d68192d92b6363490e8a8e577f55584 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Fri, 5 Jun 2020 16:43:43 +0200
Subject: clightgen: fix the printing of annotations

The printing of EF_annot and EF_annot_val was missing the extra "kind"
parameter introduced in commit 6a010b4.

Also: the automatic translation of annotations into Coq assertions
was confusing and prevented other uses of __builtin_annot statements
in conjunction with clightgen.  I believe it was never used.
This commit removes this translation.

Closes: #360
---
 exportclight/ExportClight.ml | 67 ++++++--------------------------------------
 1 file changed, 8 insertions(+), 59 deletions(-)

(limited to 'exportclight')

diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 96947545..321ed8c9 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -253,8 +253,6 @@ let signatur p sg =
      astrettype sg.sig_res
      callconv sg.sig_cc
 
-let assertions = ref ([]: (string * typ list) list)
-
 let external_function p = function
   | EF_external(name, sg) ->
       fprintf p "@[<hov 2>(EF_external %a@ %a)@]" coqstring name signatur sg
@@ -270,14 +268,15 @@ let external_function p = function
   | EF_free -> fprintf p "EF_free"
   | EF_memcpy(sz, al) ->
       fprintf p "(EF_memcpy %ld %ld)" (Z.to_int32 sz) (Z.to_int32 al)
-  | EF_annot(kind,text, targs) ->
-      assertions := (camlstring_of_coqstring text, targs) :: !assertions;
-      fprintf p "(EF_annot %a %a)" coqstring text (print_list asttype) targs
-  | EF_annot_val(kind,text, targ) ->
-      assertions := (camlstring_of_coqstring text, [targ]) :: !assertions;
-      fprintf p "(EF_annot_val %a %a)" coqstring text asttype targ
+  | EF_annot(kind, text, targs) ->
+      fprintf p "(EF_annot %ld%%positive %a %a)"
+                (P.to_int32 kind) coqstring text (print_list asttype) targs
+  | EF_annot_val(kind, text, targ) ->
+      fprintf p "(EF_annot_val %ld%%positive %a %a)"
+                (P.to_int32 kind) coqstring text asttype targ
   | EF_debug(kind, text, targs) ->
-      fprintf p "(EF_debug %ld%%positive %ld%%positive %a)" (P.to_int32 kind) (P.to_int32 text) (print_list asttype) targs
+      fprintf p "(EF_debug %ld%%positive %ld%%positive %a)"
+                (P.to_int32 kind) (P.to_int32 text) (print_list asttype) targs
   | EF_inline_asm(text, sg, clob) ->
       fprintf p "@[<hov 2>(EF_inline_asm %a@ %a@ %a)@]"
               coqstring text
@@ -447,55 +446,6 @@ let print_composite_definition p (Composite(id, su, m, a)) =
     (print_list (print_pair ident typ)) m
     attribute a
 
-(* Assertion processing *)
-
-let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
-
-type fragment = Text of string | Param of int
-
-(* For compatibility with OCaml < 4.00 *)
-let list_iteri f l =
-  let rec iteri i = function
-  | [] -> ()
-  | a::l -> f i a; iteri (i + 1) l
-  in iteri 0 l
-
-let print_assertion p (txt, targs) =
-  let frags =
-    List.map
-      (function
-       | Str.Text s -> Text s
-       | Str.Delim "%%" -> Text "%"
-       | Str.Delim s -> Param(int_of_string(String.sub s 1 (String.length s - 1))))
-      (Str.full_split re_annot_param txt) in
-  let max_param = ref 0 in
-  List.iter
-    (function
-     | Text _ -> ()
-     | Param n -> max_param := max n !max_param)
-    frags;
-  fprintf p "  | \"%s\", " txt;
-  list_iteri
-    (fun i targ -> fprintf p "_x%d :: " (i + 1))
-    targs;
-  fprintf p "nil =>@ ";
-  fprintf p "    ";
-  List.iter
-    (function
-     | Text s -> fprintf p "%s" s
-     | Param n -> fprintf p "_x%d" n)
-    frags;
-  fprintf p "@ "
-
-let print_assertions p =
-  if !assertions <> [] then begin
-    fprintf p "Definition assertions (txt: string) args : Prop :=@ ";
-    fprintf p "  match txt, args with@ ";
-    List.iter (print_assertion p) !assertions;
-    fprintf p "  | _, _ => False@ ";
-    fprintf p "  end.@ @ "
-  end
-
 (* The prologue *)
 
 let prologue = "\
@@ -595,5 +545,4 @@ let print_program p prog sourcefile normalized =
   fprintf p "Definition prog : Clight.program := @ ";
   fprintf p "  mkprogram composites global_definitions public_idents %a Logic.I.@ @ "
             ident prog.Ctypes.prog_main;
-  print_assertions p;
   fprintf p "@]@."
-- 
cgit