diff options
| -rw-r--r-- | backend/AisAnnot.ml | 77 | ||||
| -rw-r--r-- | backend/AisAnnot.mli | 8 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 6 |
3 files changed, 55 insertions, 36 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) diff --git a/backend/AisAnnot.mli b/backend/AisAnnot.mli index 7219369c..59676b26 100644 --- a/backend/AisAnnot.mli +++ b/backend/AisAnnot.mli @@ -18,10 +18,8 @@ type t = val add_ais_annot : int -> ('a -> string) -> string -> string -> 'a AST.builtin_arg list -> unit (** [add_ais_annot lbl preg spreg txt args] adds the ais annotation [txt] were the format specifiers are replace according to their type: - -a: area definitions -e: general expressions -l: l-value expressions - -p: program location -here: the address of the ais annotation [lbl] and [preg] is used to get the names of the registers, as well as [spreg] the name of the stack pointer and [args] the arguments reference in the replacements @@ -29,3 +27,9 @@ val add_ais_annot : int -> ('a -> string) -> string -> string -> 'a AST.builtin_ val get_ais_annots: unit -> (t list) list (** [get_ais_annots ()] return the list of all ais annotations and reset it *) + +val validate_ais_annot: Env.t -> string * int -> string -> C.exp list -> unit +(** [validate_ais env loc txt args] validates the ais annotation text and arguments, checking + that no volatile variables or float expressions are used as well as that no illegal format + specifier is used in the [txt] +*) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index c18a6e03..c4772688 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -882,11 +882,7 @@ let rec convertExpr env e = let fun_name = !currentFunction in let loc_string = Printf.sprintf "# file:%s line:%d function:%s\n" file line fun_name in let targs1 = convertTypArgs env [] args1 in - List.iter (fun exp -> if Cutil.is_float_type env exp.etyp then begin - error "floating point types are not supported in ais annotations" - end else if Cutil.is_volatile_variable env exp then begin - error "access to volatile variables are not supported in ais annotations" - end) args1; + AisAnnot.validate_ais_annot env !currentLocation txt args1; Ebuiltin( AST.EF_annot(P.of_int 2,coqstring_of_camlstring (loc_string ^ txt), typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) |