From e71bd08304f4eec5f834a25dc3091173214cdac2 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 27 Sep 2024 20:15:20 +0200
Subject: [PATCH] [kernel] Register known Frama-C attributes
---
src/kernel_internals/typing/cabs2cil.ml | 45 +++++++++---
src/kernel_services/ast_queries/cil.ml | 70 +++++++++++++------
src/kernel_services/ast_queries/cil.mli | 20 ++++--
tests/syntax/oracle/inline_calls.0.res.oracle | 63 ++++++++---------
4 files changed, 126 insertions(+), 72 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4d639ed255a..bee1560f737 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -93,6 +93,19 @@ let unsupported_attributes = ["vector_size"]
(* Attributes which must be erased to avoid issues (e.g., GCC 'malloc'
attributes can refer to erased functions and make the code un-reparsable *)
let erased_attributes = ["malloc"]
+let () =
+ List.iter
+ (fun a -> Cil.registerAttribute a AttrIgnored)
+ erased_attributes
+
+(* JS: return [Some s] if the attribute string is the attribute annotation [s]
+ and [None] if it is not an annotation. *)
+let attrAnnot s =
+ let r = Str.regexp "~attrannot:\\(.+\\)" in
+ if Str.string_match r s 0 then
+ try Some (Str.matched_group 1 s) with Not_found -> assert false
+ else
+ None
let stripUnderscore ?(checkUnsupported=true) s =
if String.length s = 1 then begin
@@ -110,17 +123,33 @@ let stripUnderscore ?(checkUnsupported=true) s =
let frama_c_keep_block = "FRAMA_C_KEEP_BLOCK"
let () = Cil_printer.register_shallow_attribute frama_c_keep_block
+let () = Cil.registerAttribute frama_c_keep_block AttrIgnored
let fc_stdlib = "fc_stdlib"
let fc_stdlib_generated = "fc_stdlib_generated"
let () = Cil_printer.register_shallow_attribute fc_stdlib
let () = Cil_printer.register_shallow_attribute fc_stdlib_generated
+(* fc_stdlib attribute already registered in cil.ml *)
+let () = Cil.registerAttribute fc_stdlib_generated AttrIgnored
let fc_local_static = "fc_local_static"
let () = Cil_printer.register_shallow_attribute fc_local_static
+let () = Cil.registerAttribute fc_local_static AttrIgnored
-let frama_c_destructor = "__fc_destructor"
+let frama_c_destructor = "fc_destructor"
let () = Cil_printer.register_shallow_attribute frama_c_destructor
+let () = Cil.registerAttribute frama_c_destructor (AttrName false)
+
+let () =
+ Cil.registerAttribute "packed" AttrIgnored;
+ Cil.registerAttribute "aligned" AttrIgnored;
+ Cil.registerAttribute "fc_float" (AttrName false);
+ Cil.registerAttribute "fc_assign" AttrIgnored;
+ Cil.registerAttribute "warn_unused_result" (AttrFunType false);
+ Cil.registerAttribute "FC_OLDSTYLEPROTO" AttrIgnored;
+ Cil.registerAttribute "static" AttrIgnored;
+ Cil.registerAttribute "missingproto" AttrIgnored;
+ Cil.registerAttribute "dummy" AttrIgnored
(** A hook into the code that creates temporary local vars. By default this
is the identity function, but you can overwrite it if you need to change the
@@ -3672,15 +3701,6 @@ let continueUsed () =
(****** TYPE SPECIFIERS *******)
-(* JS: return [Some s] if the attribute string is the attribute annotation [s]
- and [None] if it is not an annotation. *)
-let attrAnnot s =
- let r = Str.regexp "~attrannot:\\(.+\\)" in
- if Str.string_match r s 0 then
- try Some (Str.matched_group 1 s) with Not_found -> assert false
- else
- None
-
type local_env =
{ authorized_reads: Lval.Set.t;
@@ -4628,12 +4648,15 @@ and cabsPartitionAttributes
let kind = match doAttr ghost a with
| [] -> default
| (Attr(an, _) | AttrAnnot an)::_ ->
- (try attributeClass an with Not_found -> default)
+ (* doAttr already strip underscores of the attribute if necessary so
+ we do not need to strip then before calling attributeClass here. *)
+ attributeClass ~default an
in
match kind with
| AttrName _ -> loop (a::n, f, t) rest
| AttrFunType _ -> loop (n, a::f, t) rest
| AttrType -> loop (n, f, a::t) rest
+ | AttrIgnored -> loop (n, f, t) rest
in
loop ([], [], []) attrs
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index f67e99e8860..37545129fd0 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -160,7 +160,7 @@ let stmt_of_instr_list ?(loc=Location.unknown) = function
let bitfield_attribute_name = "FRAMA_C_BITFIELD_SIZE"
-let anonymous_attribute_name = "__fc_anonymous"
+let anonymous_attribute_name = "fc_anonymous"
let anonymous_attribute = Attr(anonymous_attribute_name, [])
(** Construct sorted lists of attributes ***)
@@ -408,7 +408,11 @@ type attributeClass =
(* Attribute of a function type. If argument is true and we are on
* MSVC then the attribute is printed just before the function name *)
- | AttrType (* Attribute of a type *)
+ | AttrType
+ (* Attribute of a type *)
+
+ | AttrIgnored
+ (** Attribute that does not correspond to either of the above classes. *)
(* This table contains the mapping of predefined attributes to classes.
* Extend this table with more attributes as you need. This table is used to
@@ -420,8 +424,8 @@ let attributeHash: (string, attributeClass) Hashtbl.t =
[ "section"; "constructor"; "destructor"; "unused"; "used"; "weak";
"no_instrument_function"; "alias"; "no_check_memory_usage";
"exception"; "model"; (* "restrict"; *)
- "aconst"; "__asm__" (* Gcc uses this to specify the name to be used in
- * assembly for a global *)];
+ "aconst"; "asm" (* Gcc uses this to specify the name to be used in
+ * assembly for a global *)];
(* Now come the MSVC declspec attributes *)
List.iter (fun a -> Hashtbl.add table a (AttrName true))
[ "thread"; "naked"; "dllimport"; "dllexport";
@@ -432,12 +436,31 @@ let attributeHash: (string, attributeClass) Hashtbl.t =
List.iter (fun a -> Hashtbl.add table a (AttrFunType true))
[ "stdcall";"cdecl"; "fastcall"; "noreturn"];
List.iter (fun a -> Hashtbl.add table a AttrType)
- [ "const"; "volatile"; "restrict"; "mode" ];
+ ("mode" :: qualifier_attributes);
table
-let attributeClass = Hashtbl.find attributeHash
-
-let registerAttribute = Hashtbl.add attributeHash
+let isKnownAttribute = Hashtbl.mem attributeHash
+
+let attributeClass ~default name =
+ match Hashtbl.find attributeHash name with
+ | exception Not_found -> default
+ | AttrIgnored -> default
+ | ac -> ac
+
+let registerAttribute an ac =
+ if Hashtbl.mem attributeHash an then begin
+ let pp fmt c =
+ match c with
+ | AttrName b -> Format.fprintf fmt "(AttrName %B)" b
+ | AttrFunType b -> Format.fprintf fmt "(AttrFunType %B)" b
+ | AttrType -> Format.fprintf fmt "AttrType"
+ | AttrIgnored -> Format.fprintf fmt "AttrIgnored"
+ in
+ Kernel.warning
+ "Replacing existing class for attribute %s: was %a, now %a"
+ an pp (Hashtbl.find attributeHash an) pp ac
+ end;
+ Hashtbl.replace attributeHash an ac
let removeAttribute = Hashtbl.remove attributeHash
(** Partition the attributes into classes *)
@@ -448,38 +471,39 @@ let partitionAttributes
let rec loop (n,f,t) = function
[] -> n, f, t
| (Attr(an, _) | AttrAnnot an as a) :: rest ->
- match (try Hashtbl.find attributeHash an with Not_found -> default) with
+ match attributeClass ~default an with
AttrName _ -> loop (addAttribute a n, f, t) rest
| AttrFunType _ ->
loop (n, addAttribute a f, t) rest
| AttrType -> loop (n, f, addAttribute a t) rest
+ | AttrIgnored -> loop (n, f, t) rest
in
loop ([], [], []) attrs
-let frama_c_ghost_else = "__fc_ghost_else"
+let frama_c_ghost_else = "fc_ghost_else"
let () = registerAttribute frama_c_ghost_else (AttrName false)
-let () =
- registerAttribute (Extlib.strip_underscore frama_c_ghost_else) (AttrName false)
-let frama_c_ghost_formal = "__fc_ghost_formal"
+let frama_c_ghost_formal = "fc_ghost_formal"
let () = registerAttribute frama_c_ghost_formal (AttrName false)
-let () =
- registerAttribute (Extlib.strip_underscore frama_c_ghost_formal) (AttrName false)
-let frama_c_init_obj = "__fc_initialized_object"
+let frama_c_init_obj = "fc_initialized_object"
let () = registerAttribute frama_c_init_obj (AttrName false)
-let () =
- registerAttribute (Extlib.strip_underscore frama_c_init_obj) (AttrName false)
-let frama_c_mutable = "__fc_mutable"
+let frama_c_mutable = "fc_mutable"
let () = registerAttribute frama_c_mutable (AttrName false)
-let () =
- registerAttribute (Extlib.strip_underscore frama_c_mutable) (AttrName false)
-let frama_c_inlined = "__fc_inlined"
+let frama_c_inlined = "fc_inlined"
let () = registerAttribute frama_c_inlined (AttrName false)
+
let () =
- registerAttribute (Extlib.strip_underscore frama_c_inlined) (AttrName false)
+ registerAttribute bitfield_attribute_name AttrType;
+ registerAttribute anonymous_attribute_name AttrIgnored;
+ List.iter
+ (fun a -> registerAttribute a AttrIgnored)
+ fc_internal_attributes;
+ List.iter
+ (fun a -> registerAttribute a AttrType)
+ cast_irrelevant_attributes
let unrollType (t: typ) : typ =
let rec withAttrs (al: attributes) (t: typ) : typ =
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 89ed0c7b2e4..0382c255746 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1340,7 +1340,11 @@ type attributeClass =
| AttrFunType of bool
(** Attribute of a function type. If argument is true and we are on
MSVC then the attribute is printed just before the function name *)
- | AttrType (** Attribute of a type *)
+ | AttrType
+ (** Attribute of a type *)
+ | AttrIgnored
+ (** Attribute that does not correspond to either of the above classes and is
+ ignored by functions [attributeClass] and [partitionAttributes]. *)
val registerAttribute: string -> attributeClass -> unit
(** Add a new attribute with a specified class *)
@@ -1348,11 +1352,17 @@ val registerAttribute: string -> attributeClass -> unit
val removeAttribute: string -> unit
(** Remove an attribute previously registered. *)
-val attributeClass: string -> attributeClass
-(** Return the class of an attributes. *)
+val isKnownAttribute: string -> bool
+(** [isKnownAttribute attrname] returns true if the attribute named [attrname]
+ is known by Frama-C. *)
-(** Partition the attributes into classes:name attributes, function type,
- and type attributes *)
+val attributeClass: default:attributeClass -> string -> attributeClass
+(** Return the class of an attributes. The class `default' is returned for
+ unknown and ignored attributes. *)
+
+(** Partition the attributes into classes: name attributes, function type and
+ type attributes. Unknown and ignored attributes are returned in the
+ `default` attribute class. *)
val partitionAttributes: default:attributeClass ->
attributes -> attribute list * (* AttrName *)
attribute list * (* AttrFunType *)
diff --git a/tests/syntax/oracle/inline_calls.0.res.oracle b/tests/syntax/oracle/inline_calls.0.res.oracle
index 18da0e0c968..ecb5321e2e7 100644
--- a/tests/syntax/oracle/inline_calls.0.res.oracle
+++ b/tests/syntax/oracle/inline_calls.0.res.oracle
@@ -23,7 +23,7 @@ int g(void)
if (v) {
int tmp;
{
- /* __blockattribute__(____fc_inlined__("f")) */int __retres_5;
+ /* __blockattribute__(__fc_inlined__("f")) */int __retres_5;
__retres_5 = 2;
tmp = __retres_5;
}
@@ -33,7 +33,7 @@ int g(void)
else {
int tmp_0;
{
- /* __blockattribute__(____fc_inlined__("in_f__fc_inline")) */int __retres_6;
+ /* __blockattribute__(__fc_inlined__("in_f__fc_inline")) */int __retres_6;
__retres_6 = 3;
tmp_0 = __retres_6;
}
@@ -47,11 +47,11 @@ int h(void)
{
int tmp;
{
- /* __blockattribute__(____fc_inlined__("g")) */int __retres;
+ /* __blockattribute__(__fc_inlined__("g")) */int __retres;
if (v) {
int tmp_3;
{
- /* __blockattribute__(____fc_inlined__("f")) */int __retres_5;
+ /* __blockattribute__(__fc_inlined__("f")) */int __retres_5;
__retres_5 = 2;
tmp_3 = __retres_5;
}
@@ -61,8 +61,7 @@ int h(void)
else {
int tmp_0;
{
- /* __blockattribute__(____fc_inlined__("in_f__fc_inline")) */
- int __retres_6;
+ /* __blockattribute__(__fc_inlined__("in_f__fc_inline")) */int __retres_6;
__retres_6 = 3;
tmp_0 = __retres_6;
}
@@ -91,8 +90,8 @@ int rec(int x_0)
goto return_label;
}
{
- /* __blockattribute__(____fc_inlined__("rec")) */int __retres_7;
- int tmp_6;
+ /* __blockattribute__(__fc_inlined__("rec")) */int __retres_7;
+ int tmp_6;
int x_0_5 = x_0 - 1;
if (x_0_5 < 0) {
__retres_7 = x_0_5;
@@ -117,7 +116,7 @@ int f1(int a)
if (nondet) {
int __inline_tmp;
{
- /* __blockattribute__(____fc_inlined__("g1")) */int a_5 = 1;
+ /* __blockattribute__(__fc_inlined__("g1")) */int a_5 = 1;
if (nondet) g1(4);
__inline_tmp = a_5;
}
@@ -126,12 +125,12 @@ int f1(int a)
if (nondet) {
int __inline_tmp_6;
{
- /* __blockattribute__(____fc_inlined__("f1")) */int __retres_9;
+ /* __blockattribute__(__fc_inlined__("f1")) */int __retres_9;
int a_8 = 2;
if (nondet) {
int __inline_tmp_10;
{
- /* __blockattribute__(____fc_inlined__("g1")) */int a_5_11 = 1;
+ /* __blockattribute__(__fc_inlined__("g1")) */int a_5_11 = 1;
if (nondet) g1(4);
__inline_tmp_10 = a_5_11;
}
@@ -156,7 +155,7 @@ int g1(int a)
if (nondet) {
int __inline_tmp;
{
- /* __blockattribute__(____fc_inlined__("g1")) */int a_4 = 4;
+ /* __blockattribute__(__fc_inlined__("g1")) */int a_4 = 4;
if (nondet) {
int __inline_tmp_5;
g1(4);
@@ -174,23 +173,23 @@ int main(void)
int __inline_tmp;
int tmp_1;
{
- /* __blockattribute__(____fc_inlined__("i")) */int __retres;
+ /* __blockattribute__(__fc_inlined__("i")) */int __retres;
/*@ assert i: \true; */ ;
__retres = 0;
__inline_tmp = __retres;
}
int local_init = __inline_tmp;
{
- /* __blockattribute__(____fc_inlined__("rec")) */int __retres_10;
- int tmp;
+ /* __blockattribute__(__fc_inlined__("rec")) */int __retres_10;
+ int tmp;
int x_0 = local_init;
if (x_0 < 0) {
__retres_10 = x_0;
goto return_label;
}
{
- /* __blockattribute__(____fc_inlined__("rec")) */int __retres_7;
- int tmp_6;
+ /* __blockattribute__(__fc_inlined__("rec")) */int __retres_7;
+ int tmp_6;
int x_0_5 = x_0 - 1;
if (x_0_5 < 0) {
__retres_7 = x_0_5;
@@ -205,12 +204,12 @@ int main(void)
}
int t = __inline_tmp_8;
{
- /* __blockattribute__(____fc_inlined__("f1")) */int __retres_13;
+ /* __blockattribute__(__fc_inlined__("f1")) */int __retres_13;
int a = 2;
if (nondet) {
int __inline_tmp_14;
{
- /* __blockattribute__(____fc_inlined__("g1")) */int a_5 = 1;
+ /* __blockattribute__(__fc_inlined__("g1")) */int a_5 = 1;
if (nondet) g1(4);
__inline_tmp_14 = a_5;
}
@@ -219,13 +218,12 @@ int main(void)
if (nondet) {
int __inline_tmp_6;
{
- /* __blockattribute__(____fc_inlined__("f1")) */int __retres_9;
+ /* __blockattribute__(__fc_inlined__("f1")) */int __retres_9;
int a_8 = 2;
if (nondet) {
int __inline_tmp_10;
{
- /* __blockattribute__(____fc_inlined__("g1")) */int a_5_11 =
- 1;
+ /* __blockattribute__(__fc_inlined__("g1")) */int a_5_11 = 1;
if (nondet) g1(4);
__inline_tmp_10 = a_5_11;
}
@@ -245,13 +243,13 @@ int main(void)
__inline_tmp_11 = __retres_13;
}
{
- /* __blockattribute__(____fc_inlined__("h")) */int tmp_15;
+ /* __blockattribute__(__fc_inlined__("h")) */int tmp_15;
{
- /* __blockattribute__(____fc_inlined__("g")) */int __retres_16;
+ /* __blockattribute__(__fc_inlined__("g")) */int __retres_16;
if (v) {
int tmp_3;
{
- /* __blockattribute__(____fc_inlined__("f")) */int __retres_5;
+ /* __blockattribute__(__fc_inlined__("f")) */int __retres_5;
__retres_5 = 2;
tmp_3 = __retres_5;
}
@@ -261,7 +259,7 @@ int main(void)
else {
int tmp_0;
{
- /* __blockattribute__(____fc_inlined__("in_f__fc_inline")) */
+ /* __blockattribute__(__fc_inlined__("in_f__fc_inline")) */
int __retres_6;
__retres_6 = 3;
tmp_0 = __retres_6;
@@ -289,7 +287,7 @@ int call_with_static(void)
{
int tmp;
{
- /* __blockattribute__(____fc_inlined__("with_static")) */with_static_count ++;
+ /* __blockattribute__(__fc_inlined__("with_static")) */with_static_count ++;
tmp = with_static_count;
}
return tmp;
@@ -305,8 +303,7 @@ void builtin_acsl(void)
void call_builtin_acsl(void)
{
{
- /* __blockattribute__(____fc_inlined__("builtin_acsl")) */float g_0 =
- 0.f;
+ /* __blockattribute__(__fc_inlined__("builtin_acsl")) */float g_0 = 0.f;
/*@ assert ¬\is_NaN(g_0); */ ;
;
}
@@ -322,9 +319,9 @@ void f_slevel(void)
void call_f_slevel(void)
{
{
- /* __blockattribute__(____fc_inlined__("f_slevel")) *//*@
- \eva::slevel 0; */
- ;
+ /* __blockattribute__(__fc_inlined__("f_slevel")) *//*@ \eva::slevel 0;
+ */
+ ;
;
}
return;
@@ -341,7 +338,7 @@ void post_decl(void);
void middle_decl(void)
{
{
- /* __blockattribute__(____fc_inlined__("pre_decl")) */x ++;
+ /* __blockattribute__(__fc_inlined__("pre_decl")) */x ++;
y ++;
post_decl();
;
--
GitLab