Skip to content

Commit 1648018

Browse files
sipmasipma
committed
CHB: align attribute handling with that in C analyzer
1 parent bf45bca commit 1648018

16 files changed

+273
-298
lines changed

‎CodeHawk/CHB/bchlib/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -131,7 +131,6 @@ SOURCES := \
131131
bCHBCDictionary \
132132
bCHBCFunDeclarations \
133133
bCHBCWriteXml \
134-
bCHBCAttributes \
135134
bCHBCFiles \
136135
bCHBCTypeUtil \
137136
bCHBCTypeXml \
@@ -174,6 +173,7 @@ SOURCES := \
174173
bCHPrecondition \
175174
bCHPostcondition \
176175
bCHSideeffect \
176+
bCHBCAttributes \
177177
bCHFunctionSemantics \
178178
bCHFunctionSummary \
179179
bCHVariable \

‎CodeHawk/CHB/bchlib/bCHBCAttributes.ml‎

Lines changed: 81 additions & 69 deletions
Original file line numberDiff line numberDiff line change
@@ -25,79 +25,91 @@
2525
SOFTWARE.
2626
============================================================================= *)
2727

28-
open BCHBCTypes
28+
(* chlib *)
29+
open CHPretty
30+
31+
(* chutil *)
32+
open CHLogger
2933

34+
(* bchlib *)
35+
open BCHBasicTypes
36+
open BCHBCTypes
37+
open BCHBCTypePretty
38+
open BCHBCTypeUtil
39+
open BCHFtsParameter
40+
open BCHFunctionInterface
41+
open BCHLibTypes
3042

31-
let gcc_attributes_to_precondition_attributes
32-
(attrs: b_attributes_t): precondition_attribute_t list =
33-
List.fold_left (fun acc a ->
34-
match a with
35-
| Attr ("access", params) ->
36-
(match params with
37-
| [ACons ("read_only", []); AInt refindex] ->
38-
(APCReadOnly (refindex, None)) :: acc
39-
| [ACons ("read_only", []); AInt refindex; AInt sizeindex] ->
40-
(APCReadOnly (refindex, Some sizeindex)) :: acc
41-
| [ACons ("write_only", []); AInt refindex] ->
42-
(APCWriteOnly (refindex, None)) :: acc
43-
| [ACons ("write_only", []); AInt refindex; AInt sizeindex] ->
44-
(APCWriteOnly (refindex, Some sizeindex)) :: acc
45-
| [ACons ("read_write", []); AInt refindex] ->
46-
(APCReadWrite (refindex, None)) :: acc
47-
| [ACons ("read_write", []); AInt refindex; AInt sizeindex] ->
48-
(APCReadWrite (refindex, Some sizeindex)) :: acc
49-
| _ -> acc)
50-
| _ -> acc) [] attrs
5143

44+
let convert_b_attributes_to_function_conditions
45+
(name: string)
46+
(fintf: function_interface_t)
47+
(attrs: b_attributes_t):
48+
(xxpredicate_t list * xxpredicate_t list * xxpredicate_t list) =
49+
let parameters = get_fts_parameters fintf in
50+
let get_par (n: int) =
51+
try
52+
List.find (fun p ->
53+
match p.apar_index with Some ix -> ix = n | _ -> false) parameters
54+
with
55+
| Not_found ->
56+
raise
57+
(BCH_failure
58+
(LBLOCK [
59+
STR "No parameter with index ";
60+
INT n;
61+
pretty_print_list (List.map (fun p -> p.apar_name) parameters)
62+
(fun s -> STR s) "[" "," "]"])) in
63+
let get_derefty (par: fts_parameter_t): btype_t =
64+
if is_pointer par.apar_type then
65+
ptr_deref par.apar_type
66+
else
67+
raise
68+
(BCH_failure
69+
(LBLOCK [
70+
STR "parameter is not a pointer type: ";
71+
fts_parameter_to_pretty par])) in
72+
List.fold_left (fun ((xpre, xside, xpost) as acc) attr ->
73+
match attr with
74+
| Attr (("access" | "chk_access"), params) ->
75+
let (pre, side) =
76+
(match params with
77+
| [ACons ("read_only", []); AInt refindex] ->
78+
let par = get_par refindex in
79+
let ty = get_derefty par in
80+
([XXBuffer (ty, ArgValue par, RunTimeValue)], [])
5281

53-
let gcc_attributes_to_srcmapinfo
54-
(attrs: b_attributes_t): srcmapinfo_t option =
55-
let optsrcloc =
56-
List.fold_left (fun acc a ->
57-
match acc with
58-
| Some _ -> acc
59-
| _ ->
60-
match a with
61-
| Attr ("chkc_srcloc", params) ->
62-
(match params with
63-
| [AStr filename; AInt linenumber] ->
64-
Some {srcloc_filename=filename;
65-
srcloc_linenumber=linenumber;
66-
srcloc_notes=[]}
67-
| _ -> None)
68-
| _ -> None) None attrs in
69-
match optsrcloc with
70-
| Some srcloc ->
71-
let binloc =
72-
List.fold_left (fun acc a ->
73-
match acc with
74-
| Some _ -> acc
75-
| _ ->
76-
match a with
77-
| Attr ("chkx_binloc", params) ->
78-
(match params with
79-
| [AStr address] -> Some address
80-
| _ -> None)
81-
| _ -> None) None attrs in
82-
Some {srcmap_srcloc = srcloc; srcmap_binloc = binloc}
83-
| _ -> None
82+
| [ACons ("read_only", []); AInt refindex; AInt sizeindex] ->
83+
let rpar = get_par refindex in
84+
let spar = get_par sizeindex in
85+
let ty = get_derefty rpar in
86+
([XXBuffer (ty, ArgValue rpar, ArgValue spar)], [])
8487

88+
| [ACons (("write_only" | "read_write"), []); AInt refindex] ->
89+
let par = get_par refindex in
90+
let ty = get_derefty par in
91+
([XXBuffer (ty, ArgValue par, RunTimeValue)],
92+
[XXBlockWrite (ty, ArgValue par, RunTimeValue)])
8593

94+
| [ACons (("write_only" | "read_write"), []);
95+
AInt refindex; AInt sizeindex] ->
96+
let rpar = get_par refindex in
97+
let spar = get_par sizeindex in
98+
let ty = get_derefty rpar in
99+
([XXBuffer (ty, ArgValue rpar, ArgValue spar)],
100+
[XXBlockWrite (ty, ArgValue rpar, ArgValue spar)])
86101

87-
let precondition_attributes_t_to_gcc_attributes
88-
(preattrs: precondition_attribute_t list): b_attributes_t =
89-
let get_params (refindex: int) (optsizeindex: int option) =
90-
match optsizeindex with
91-
| Some sizeindex -> [AInt refindex; AInt sizeindex]
92-
| _ -> [AInt refindex] in
93-
let get_access (mode: string) (params: b_attrparam_t list) =
94-
Attr ("access", [ACons (mode, [])] @ params) in
95-
List.fold_left (fun acc p ->
96-
match p with
97-
| APCReadOnly (refindex, optsizeindex) ->
98-
(get_access "read_only" (get_params refindex optsizeindex)) :: acc
99-
| APCWriteOnly (refindex, optsizeindex) ->
100-
(get_access "write_only" (get_params refindex optsizeindex)) :: acc
101-
| APCReadWrite (refindex, optsizeindex) ->
102-
(get_access "read_write" (get_params refindex optsizeindex)) :: acc
103-
| _ -> acc) [] preattrs
102+
| _ ->
103+
begin
104+
log_error_result
105+
~msg:("attribute conversion for " ^ name ^ ": "
106+
^ "attribute parameters "
107+
^ (String.concat
108+
", " (List.map b_attrparam_to_string params)))
109+
~tag:"attribute conversion"
110+
__FILE__ __LINE__ [];
111+
([], [])
112+
end) in
113+
(pre @ xpre, side @ xside, xpost)
114+
| _ ->
115+
acc) ([], [], []) attrs

‎CodeHawk/CHB/bchlib/bCHBCAttributes.mli‎

Lines changed: 57 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
------------------------------------------------------------------------------
55
The MIT License (MIT)
66
7-
Copyright (c) 2024 Aarno Labs LLC
7+
Copyright (c) 2024-2025 Aarno Labs LLC
88
99
Permission is hereby granted, free of charge, to any person obtaining a copy
1010
of this software and associated documentation files (the "Software"), to deal
@@ -26,14 +26,64 @@
2626
============================================================================= *)
2727

2828
open BCHBCTypes
29+
open BCHLibTypes
2930

3031

31-
val gcc_attributes_to_precondition_attributes:
32-
b_attributes_t -> precondition_attribute_t list
32+
(** {1 Function attributes} *)
3333

34-
val gcc_attributes_to_srcmapinfo:
35-
b_attributes_t -> srcmapinfo_t option
34+
(** Function declarations in C can be decorated with attributes. These attributes
35+
are generally used to allow certain compiler optimizations
36+
(https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attributes.html). Here
37+
we use them to communicate preconditions about dynamically linked library
38+
functions.
3639
40+
For many standard libc library functions the analyzer has comprehensive
41+
collection of (hand-made) function summaries that include pre- and
42+
postconditions, side effects, etc, represented in xml.
43+
However, binaries may of course be dynamically linked to a wide variety of
44+
other libraries, for which it is not directly feasible to create these
45+
summaries (e.g., because suitable binaries are not available for analysis).
46+
One possibility is for the user to manually create the xml function summaries
47+
for all functions of interest. A more user-friendly means of providing
48+
similar information is through function prototypes decorated with suitable
49+
attributes, as described here.
3750
38-
val precondition_attributes_t_to_gcc_attributes:
39-
precondition_attribute_t list -> b_attributes_t
51+
We use the same syntax as presented in
52+
(https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attributes.html).
53+
Currently the following attributes are supported:
54+
55+
{[
56+
(access (access-mode, ref-index))
57+
(access (access-mode, ref-index, size-index))
58+
(nonnull (ref-indices))
59+
]}
60+
61+
Access modes supported are [read_only], [read_write], and [write_only]; the
62+
[ref-index] is an integer denoting the (1-based) index of the pointer
63+
argument being accessed, and [size-index] is an integer denoting the
64+
(1-based) index of an argument that provides a maximum size (in bytes)
65+
for the memory region accessed.
66+
67+
As an example, for [memcpy] this would be decorated as:
68+
69+
{[
70+
__attribute__ ((access (read_only, 2, 3)),
71+
(access (write_only, 1, 3)), (nonnull (1, 2)))
72+
void* memcpy (void *dst, const void *src, size_t len);
73+
]}
74+
75+
(Note that the analyzer has a comprehensive function summary for memcpy, so
76+
it is only shown here as an example, because of its familiar semantics.)
77+
78+
A prototype thus decorated will automatically generate a function interface
79+
with the function semantics that include the corresponding preconditions
80+
(and, in case of write_only, the corresponding side effect) for the given
81+
library function, resulting in the appropriate proof obligations at their
82+
call sites.
83+
*)
84+
85+
val convert_b_attributes_to_function_conditions:
86+
string
87+
-> function_interface_t
88+
-> b_attributes_t
89+
-> (xxpredicate_t list * xxpredicate_t list * xxpredicate_t list)

‎CodeHawk/CHB/bchlib/bCHBCFiles.ml‎

Lines changed: 35 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,40 @@ module H = Hashtbl
4747
let bcd = BCHBCDictionary.bcdictionary
4848

4949

50+
let gcc_attributes_to_srcmapinfo
51+
(attrs: b_attributes_t): srcmapinfo_t option =
52+
let optsrcloc =
53+
List.fold_left (fun acc a ->
54+
match acc with
55+
| Some _ -> acc
56+
| _ ->
57+
match a with
58+
| Attr ("chkc_srcloc", params) ->
59+
(match params with
60+
| [AStr filename; AInt linenumber] ->
61+
Some {srcloc_filename=filename;
62+
srcloc_linenumber=linenumber;
63+
srcloc_notes=[]}
64+
| _ -> None)
65+
| _ -> None) None attrs in
66+
match optsrcloc with
67+
| Some srcloc ->
68+
let binloc =
69+
List.fold_left (fun acc a ->
70+
match acc with
71+
| Some _ -> acc
72+
| _ ->
73+
match a with
74+
| Attr ("chkx_binloc", params) ->
75+
(match params with
76+
| [AStr address] -> Some address
77+
| _ -> None)
78+
| _ -> None) None attrs in
79+
Some {srcmap_srcloc = srcloc; srcmap_binloc = binloc}
80+
| _ -> None
81+
82+
83+
5084
class bcfiles_t: bcfiles_int =
5185
object (self)
5286

@@ -75,7 +109,7 @@ object (self)
75109
let i = bcd#index_location in
76110

77111
let add_srcmapinfo (vinfo: bvarinfo_t) =
78-
match BCHBCAttributes.gcc_attributes_to_srcmapinfo vinfo.bvattr with
112+
match gcc_attributes_to_srcmapinfo vinfo.bvattr with
79113
| Some srcmap ->
80114
let vix = bcd#index_varinfo vinfo in
81115
if H.mem vinfo_srcmap vix then

‎CodeHawk/CHB/bchlib/bCHBCTypes.mli‎

Lines changed: 1 addition & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -120,67 +120,7 @@ type type_transformer_t = string -> string
120120

121121
(** {1 Types and attributes} *)
122122

123-
(** {2 Precondition attributes}
124-
125-
Function declarations in C can be decorated with attributes. These attributes
126-
are generally used to allow certain compiler optimizations
127-
(https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attributes.html). Here
128-
we use them to communicate preconditions about dynamically linked library
129-
functions.
130-
131-
For many standard libc library functions the analyzer has comprehensive
132-
collection of (hand-made) function summaries that include pre- and
133-
postconditions, side effects, etc, represented in xml.
134-
However, binaries may of course be dynamically linked to a wide variety of
135-
other libraries, for which it is not directly feasible to create these
136-
summaries (e.g., because suitable binaries are not available for analysis).
137-
One possibility is for the user to manually create the xml function summaries
138-
for all functions of interest. A more user-friendly means of providing
139-
similar information is through function prototypes decorated with suitable
140-
attributes, as described here.
141-
142-
We use the same syntax as presented in
143-
(https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attributes.html).
144-
Currently the following attributes are supported:
145-
146-
{[
147-
(access (access-mode, ref-index))
148-
(access (access-mode, ref-index, size-index))
149-
(nonnull (ref-indices))
150-
]}
151-
152-
Access modes supported are [read_only], [read_write], and [write_only]; the
153-
[ref-index] is an integer denoting the (1-based) index of the pointer
154-
argument being accessed, and [size-index] is an integer denoting the
155-
(1-based) index of an argument that provides a maximum size (in bytes)
156-
for the memory region accessed.
157-
158-
As an example, for [memcpy] this would be decorated as:
159-
160-
{[
161-
__attribute__ ((access (read_only, 2, 3)),
162-
(access (write_only, 1, 3)), (nonnull (1, 2)))
163-
void* memcpy (void *dst, const void *src, size_t len);
164-
]}
165-
166-
(Note that the analyzer has a comprehensive function summary for memcpy, so
167-
it is only shown here as an example, because of its familiar semantics.)
168-
169-
A prototype thus decorated will automatically generate a function interface
170-
with the function semantics that include the corresponding preconditions
171-
(and, in case of write_only, the corresponding side effect) for the given
172-
library function, resulting in the appropriate proof obligations at their
173-
call sites.
174-
*)
175-
176-
type precondition_attribute_t =
177-
| APCReadOnly of int * int option (* ref-index, size-index, both 1-based *)
178-
| APCWriteOnly of int * int option (* ref-index, size-index, (both 1-based) *)
179-
| APCReadWrite of int * int option (* ref-index, size-index, (both 1-based) *)
180-
| APCNull of int list (* parameter indices, 1-based *)
181-
182-
183-
and btype_t =
123+
type btype_t =
184124
| TVoid of b_attributes_t
185125
| TInt of ikind_t * b_attributes_t
186126
| TFloat of fkind_t * frepresentation_t * b_attributes_t

0 commit comments

Comments
 (0)