Improve and simplify error messages.

The checks on the argument and format arguments are now performed
during C2C translation by calling the validate_ais_annotations
function and result in an error instead of a warning in the
backend to be more consistent with the rest of the builtin
functions.

1 files changed, 48 insertions, 29 deletions

diff --git a/backend/AisAnnot.ml b/backend/AisAnnot.ml
index f4dab4c9..afa7e50f 100644
--- a/backend/AisAnnot.ml
+++ b/backend/AisAnnot.ml
@@ -34,22 +34,35 @@ let addr_global id ofs =
   [String addr_o;Symbol id;String addr_e]
 
 exception Bad_parameter of string
-exception Unknown_parameter of string
-exception Unknown_type of char
 
-let ais_expr_arg lval preg_string sp_reg_name arg =
+let warn_lval_arg  pos arg =
+  let warn ty =
+    let msg = sprintf "expected register or memory cell but found %s for parameter '%s'" ty pos in
+      raise (Bad_parameter msg) in
+  match arg with
+  | BA_int _
+  | BA_long _ -> warn "constant"
+  | BA_float _
+  | BA_single _ -> assert false (* Should never occur and be avoided in C2C *)
+  | BA_addrstack ofs ->
+    warn "stack cell"
+  | BA_addrglobal(id, ofs) ->
+    warn "global address"
+  | BA_splitlong(hi, lo) ->
+    warn "register pair";
+  | BA_addptr(a1, a2) ->
+    warn "pointer computation"
+  | _ -> ()
+
+let ais_expr_arg pos preg_string sp_reg_name arg =
   let preg reg = sprintf "reg(\"%s\")" (preg_string reg)
   and sp = sprintf "reg(\"%s\")" sp_reg_name
   and simple s = [String s]
-  and lval ty =
-    if lval then
-      let msg = sprintf "expected register or memory cell but found %s" ty in
-      raise (Bad_parameter msg)
   in
   let rec ais_arg = function
   | BA x -> simple (preg x)
-  | BA_int n -> lval "constant"; simple (sprintf "%ld" (camlint_of_coqint n))
-  | BA_long n ->lval "constant"; simple (sprintf "%Ld" (camlint64_of_coqint n))
+  | BA_int n -> simple (sprintf "%ld" (camlint_of_coqint n))
+  | BA_long n -> simple (sprintf "%Ld" (camlint64_of_coqint n))
   | BA_float _
   | BA_single _ -> assert false (* Should never occur and be avoided in C2C *)
   | BA_loadstack(chunk, ofs) ->
@@ -58,7 +71,6 @@ let ais_expr_arg lval preg_string sp_reg_name arg =
                        (size_chunk chunk) in
     simple loadstack
   | BA_addrstack ofs ->
-    lval "stack cell";
     let addrstack  = sprintf "(%s%s)" sp (offset ofs) in
     simple addrstack
   | BA_loadglobal(chunk, id, ofs) ->
@@ -68,14 +80,12 @@ let ais_expr_arg lval preg_string sp_reg_name arg =
         (size_chunk chunk) in
     [String mem_o;Symbol id;String mem_e]
   | BA_addrglobal(id, ofs) ->
-    lval "global address";
     addr_global id ofs
   | BA_splitlong(hi, lo) ->
     combine " * 0x100000000 + " hi lo
   | BA_addptr(a1, a2) ->
     combine " + " a1 a2
   and combine mid arg1 arg2 =
-    lval "pointer computation";
     let op_br = simple "("
     and mid = simple mid
     and cl_br = simple ")"
@@ -106,7 +116,7 @@ let loc_of_txt txt =
   with _ ->
     no_loc
 
-let re_ais_annot_param = Str.regexp "%%\\|%[aelp][1-9][0-9]*\\|%here\\|\007"
+let re_ais_annot_param = Str.regexp "%%\\|%[el][1-9][0-9]*\\|%here\\|\007"
 
 let add_ais_annot lbl preg_string sp_reg_name txt args =
   let fragment = function
@@ -121,30 +131,20 @@ let add_ais_annot lbl preg_string sp_reg_name txt args =
     | Str.Delim s ->
       let typ = String.get s 1
       and n = int_of_string (String.sub s 2 (String.length s - 2)) in
-      let arg = try
-          List.nth args (n-1)
-        with _ ->
-           raise (Unknown_parameter s) in
+      let arg = List.nth args (n-1) in
       begin match typ with
-        | 'e' -> ais_expr_arg false preg_string sp_reg_name arg
-        | 'l' -> ais_expr_arg true preg_string sp_reg_name arg
-        | _ -> raise (Unknown_type typ)
+        | 'e' -> ais_expr_arg s preg_string sp_reg_name arg
+        | 'l' -> warn_lval_arg s arg; ais_expr_arg s preg_string sp_reg_name arg
+        | _ -> assert false
       end
   in
-  let loc = loc_of_txt txt in
-  let warn t s =
-    warning loc Wrong_ais_parameter "%s %s" t s; []
-  in
   let annot  =
     try
       List.concat (List.map fragment (Str.full_split re_ais_annot_param txt))
     with
     | Bad_parameter s ->
-      warn "wrong ais parameter" s
-    | Unknown_parameter s ->
-      warn "unknown parameter" s
-    | Unknown_type c ->
-      warn "unknown format argument" (String.make 1 c)
+      let loc = loc_of_txt txt in
+      warning loc Wrong_ais_parameter "wrong ais parameter %s" s; []
   in
   let rec merge acc = function
     | [] -> List.rev acc
@@ -157,3 +157,22 @@ let add_ais_annot lbl preg_string sp_reg_name txt args =
   let annot = merge [] annot in
   if annot <> [] then
     ais_annot_list := (annot)::!ais_annot_list
+
+let validate_ais_annot env loc txt args =
+  let fragment arg =
+    match arg with
+      | Str.Delim "%here"
+      | Str.Text _
+      | Str.Delim "%%"
+      | Str.Delim "\007" -> ()
+      | Str.Delim s ->
+        let n = int_of_string (String.sub s 2 (String.length s - 2)) in
+        try
+          let arg = List.nth args (n-1) in
+          if Cutil.is_float_type env arg.C.etyp then
+            error loc "floating point types are not supported in ais annotations"
+          else if Cutil.is_volatile_variable env arg then
+            error loc "access to volatile variable '%a' is not supported in ais annotations" Cprint.exp (0,arg)
+        with _ ->
+          error loc "unknown parameter '%s'" s
+  in List.iter fragment (Str.full_split re_ais_annot_param txt)