Armoperands

CodeHawk/CHB/bchlib/Makefile

@@ -131,7 +131,6 @@ SOURCES := \
 	bCHBCDictionary \
 	bCHBCFunDeclarations \
 	bCHBCWriteXml \
-	bCHBCAttributes \
 	bCHBCFiles \
 	bCHBCTypeUtil \
 	bCHBCTypeXml \
@@ -174,6 +173,7 @@ SOURCES := \
 	bCHPrecondition \
 	bCHPostcondition \
 	bCHSideeffect \
+	bCHBCAttributes \
 	bCHFunctionSemantics \
 	bCHFunctionSummary \
 	bCHVariable \

CodeHawk/CHB/bchlib/bCHBCAttributes.ml

@@ -25,79 +25,91 @@
    SOFTWARE.
    ============================================================================= *)
 
-open BCHBCTypes
+(* chlib *)
+open CHPretty
+
+(* chutil *)
+open CHLogger
 
+(* bchlib *)
+open BCHBasicTypes
+open BCHBCTypes
+open BCHBCTypePretty
+open BCHBCTypeUtil
+open BCHFtsParameter
+open BCHFunctionInterface
+open BCHLibTypes
 
-let gcc_attributes_to_precondition_attributes
-      (attrs: b_attributes_t): precondition_attribute_t list =
-  List.fold_left (fun acc a ->
-      match a with
-      | Attr ("access", params) ->
-         (match params with
-          | [ACons ("read_only", []); AInt refindex] ->
-             (APCReadOnly (refindex, None)) :: acc
-          | [ACons ("read_only", []); AInt refindex; AInt sizeindex] ->
-             (APCReadOnly (refindex, Some sizeindex)) :: acc
-          | [ACons ("write_only", []); AInt refindex] ->
-             (APCWriteOnly (refindex, None)) :: acc
-          | [ACons ("write_only", []); AInt refindex; AInt sizeindex] ->
-             (APCWriteOnly (refindex, Some sizeindex)) :: acc
-          | [ACons ("read_write", []); AInt refindex] ->
-             (APCReadWrite (refindex, None)) :: acc
-          | [ACons ("read_write", []); AInt refindex; AInt sizeindex] ->
-             (APCReadWrite (refindex, Some sizeindex)) :: acc
-          | _ -> acc)
-      | _ -> acc) [] attrs
 
+let convert_b_attributes_to_function_conditions
+      (name: string)
+      (fintf: function_interface_t)
+      (attrs: b_attributes_t):
+      (xxpredicate_t list * xxpredicate_t list * xxpredicate_t list) =
+  let parameters = get_fts_parameters fintf in
+  let get_par (n: int) =
+    try
+      List.find (fun p ->
+          match p.apar_index with Some ix -> ix = n | _ -> false) parameters
+    with
+    | Not_found ->
+       raise
+         (BCH_failure
+            (LBLOCK [
+                 STR "No parameter with index ";
+                 INT n;
+                 pretty_print_list (List.map (fun p -> p.apar_name) parameters)
+                   (fun s -> STR s) "[" "," "]"])) in
+  let get_derefty (par: fts_parameter_t): btype_t =
+    if is_pointer par.apar_type then
+      ptr_deref par.apar_type
+    else
+      raise
+        (BCH_failure
+           (LBLOCK [
+                STR "parameter is not a pointer type: ";
+                fts_parameter_to_pretty par])) in
+  List.fold_left (fun ((xpre, xside, xpost) as acc) attr ->
+      match attr with
+      | Attr (("access" | "chk_access"), params) ->
+         let (pre, side) =
+           (match params with
+            | [ACons ("read_only", []); AInt refindex] ->
+               let par = get_par refindex in
+               let ty = get_derefty par in
+               ([XXBuffer (ty, ArgValue par, RunTimeValue)], [])
 
-let gcc_attributes_to_srcmapinfo
-      (attrs: b_attributes_t): srcmapinfo_t option =
-  let optsrcloc =
-    List.fold_left (fun acc a ->
-        match acc with
-        | Some _ -> acc
-        | _ ->
-           match a with
-           | Attr ("chkc_srcloc", params) ->
-              (match params with
-               | [AStr filename; AInt linenumber] ->
-                  Some {srcloc_filename=filename;
-                        srcloc_linenumber=linenumber;
-                        srcloc_notes=[]}
-               | _ -> None)
-           | _ -> None) None attrs in
-  match optsrcloc with
-  | Some srcloc ->
-     let binloc =
-       List.fold_left (fun acc a ->
-           match acc with
-           | Some _ -> acc
-           | _ ->
-              match a with
-              | Attr ("chkx_binloc", params) ->
-                 (match params with
-                  | [AStr address] -> Some address
-                  | _ -> None)
-              | _ -> None) None attrs in
-     Some {srcmap_srcloc = srcloc; srcmap_binloc = binloc}
-  | _ -> None
+            | [ACons ("read_only", []); AInt refindex; AInt sizeindex] ->
+               let rpar = get_par refindex in
+               let spar = get_par sizeindex in
+               let ty = get_derefty rpar in
+               ([XXBuffer (ty, ArgValue rpar, ArgValue spar)], [])
 
+            | [ACons (("write_only" | "read_write"), []); AInt refindex] ->
+               let par = get_par refindex in
+               let ty = get_derefty par in
+               ([XXBuffer (ty, ArgValue par, RunTimeValue)],
+                [XXBlockWrite (ty, ArgValue par, RunTimeValue)])
 
+            | [ACons (("write_only" | "read_write"), []);
+               AInt refindex; AInt sizeindex] ->
+               let rpar = get_par refindex in
+               let spar = get_par sizeindex in
+               let ty = get_derefty rpar in
+               ([XXBuffer (ty, ArgValue rpar, ArgValue spar)],
+                [XXBlockWrite (ty, ArgValue rpar, ArgValue spar)])
 
-let precondition_attributes_t_to_gcc_attributes
-      (preattrs: precondition_attribute_t list): b_attributes_t =
-  let get_params (refindex: int) (optsizeindex: int option) =
-    match optsizeindex with
-    | Some sizeindex -> [AInt refindex; AInt sizeindex]
-    | _ -> [AInt refindex] in
-  let get_access (mode: string) (params: b_attrparam_t list) =
-    Attr ("access", [ACons (mode, [])] @ params) in
-  List.fold_left (fun acc p ->
-      match p with
-      | APCReadOnly (refindex, optsizeindex) ->
-         (get_access "read_only" (get_params refindex optsizeindex)) :: acc
-      | APCWriteOnly (refindex, optsizeindex) ->
-         (get_access "write_only" (get_params refindex optsizeindex)) :: acc
-      | APCReadWrite (refindex, optsizeindex) ->
-         (get_access "read_write" (get_params refindex optsizeindex)) :: acc
-      | _ -> acc) [] preattrs
+            | _ ->
+               begin
+                 log_error_result
+                   ~msg:("attribute conversion for " ^ name ^ ": "
+                         ^ "attribute parameters "
+                         ^ (String.concat
+                              ", " (List.map b_attrparam_to_string params)))
+                   ~tag:"attribute conversion"
+                   __FILE__ __LINE__ [];
+                 ([], [])
+               end) in
+         (pre @ xpre, side @ xside, xpost)
+      | _ ->
+         acc) ([], [], []) attrs

CodeHawk/CHB/bchlib/bCHBCAttributes.mli

@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2024  Aarno Labs LLC
+   Copyright (c) 2024-2025  Aarno Labs LLC
 
    Permission is hereby granted, free of charge, to any person obtaining a copy
    of this software and associated documentation files (the "Software"), to deal
@@ -26,14 +26,64 @@
    ============================================================================= *)
 
 open BCHBCTypes
+open BCHLibTypes
 
 
-val gcc_attributes_to_precondition_attributes:
-  b_attributes_t -> precondition_attribute_t list
+(** {1 Function attributes} *)
 
-val gcc_attributes_to_srcmapinfo:
-  b_attributes_t -> srcmapinfo_t option
+(** Function declarations in C can be decorated with attributes. These attributes
+    are generally used to allow certain compiler optimizations
+    (https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attributes.html). Here
+    we use them to communicate preconditions about dynamically linked library
+    functions.
 
+    For many standard libc library functions the analyzer has comprehensive
+    collection of (hand-made) function summaries that include pre- and
+    postconditions, side effects, etc, represented in xml.
+    However, binaries may of course be dynamically linked to a wide variety of
+    other libraries, for which it is not directly feasible to create these
+    summaries (e.g., because suitable binaries are not available for analysis).
+    One possibility is for the user to manually create the xml function summaries
+    for all functions of interest. A more user-friendly means of providing
+    similar information is through function prototypes decorated with suitable
+    attributes, as described here.
 
-val precondition_attributes_t_to_gcc_attributes:
-  precondition_attribute_t list -> b_attributes_t
+    We use the same syntax as presented in
+    (https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attributes.html).
+    Currently the following attributes are supported:
+
+    {[
+    (access (access-mode, ref-index))
+    (access (access-mode, ref-index, size-index))
+    (nonnull (ref-indices))
+    ]}
+
+    Access modes supported are [read_only], [read_write], and [write_only]; the
+    [ref-index] is an integer denoting the (1-based) index of the pointer
+    argument being accessed, and [size-index] is an integer denoting the
+    (1-based) index of an argument that provides a maximum size (in bytes)
+    for the memory region accessed.
+
+    As an example, for [memcpy] this would be decorated as:
+
+    {[
+    __attribute__ ((access (read_only, 2, 3)),
+                   (access (write_only, 1, 3)), (nonnull (1, 2)))
+    void* memcpy (void *dst, const void *src, size_t len);
+    ]}
+
+    (Note that the analyzer has a comprehensive function summary for memcpy, so
+    it is only shown here as an example, because of its familiar semantics.)
+
+    A prototype thus decorated will automatically generate a function interface
+    with the function semantics that include the corresponding preconditions
+    (and, in case of write_only, the corresponding side effect) for the given
+    library function, resulting in the appropriate proof obligations at their
+    call sites.
+ *)
+
+val convert_b_attributes_to_function_conditions:
+  string
+  -> function_interface_t
+  -> b_attributes_t
+  -> (xxpredicate_t list * xxpredicate_t list * xxpredicate_t list)

CodeHawk/CHB/bchlib/bCHBCFiles.ml

@@ -47,6 +47,40 @@ module H = Hashtbl
 let bcd = BCHBCDictionary.bcdictionary
 
 
+let gcc_attributes_to_srcmapinfo
+      (attrs: b_attributes_t): srcmapinfo_t option =
+  let optsrcloc =
+    List.fold_left (fun acc a ->
+        match acc with
+        | Some _ -> acc
+        | _ ->
+           match a with
+           | Attr ("chkc_srcloc", params) ->
+              (match params with
+               | [AStr filename; AInt linenumber] ->
+                  Some {srcloc_filename=filename;
+                        srcloc_linenumber=linenumber;
+                        srcloc_notes=[]}
+               | _ -> None)
+           | _ -> None) None attrs in
+  match optsrcloc with
+  | Some srcloc ->
+     let binloc =
+       List.fold_left (fun acc a ->
+           match acc with
+           | Some _ -> acc
+           | _ ->
+              match a with
+              | Attr ("chkx_binloc", params) ->
+                 (match params with
+                  | [AStr address] -> Some address
+                  | _ -> None)
+              | _ -> None) None attrs in
+     Some {srcmap_srcloc = srcloc; srcmap_binloc = binloc}
+  | _ -> None
+
+
+
 class bcfiles_t: bcfiles_int =
 object (self)
 
@@ -75,7 +109,7 @@ object (self)
     let i = bcd#index_location in
 
     let add_srcmapinfo (vinfo: bvarinfo_t) =
-      match BCHBCAttributes.gcc_attributes_to_srcmapinfo vinfo.bvattr with
+      match gcc_attributes_to_srcmapinfo vinfo.bvattr with
       | Some srcmap ->
          let vix = bcd#index_varinfo vinfo in
          if H.mem vinfo_srcmap vix then

CodeHawk/CHB/bchlib/bCHBCTypePretty.ml

@@ -165,15 +165,87 @@ let constant_to_string (c: bconstant_t) =
   | _ -> cil_constant_to_string c
 
 
-let attributes_to_string attrs =
+let rec attributes_to_string (attrs: b_attributes_t) =
   match attrs with
   | [] -> ""
-  | l ->
+  | _ ->
      (String.concat
-        "," (List.map (fun attr -> match attr with Attr (s, _) -> s) l)) ^ " "
+        "\n"
+        (List.map
+           (fun attr ->
+             match attr with
+             | Attr (s, params) ->
+                "__attribute__((__" ^ s ^ "__,"
+                ^ (String.concat
+                     ", "
+                     (List.map b_attrparam_to_string params))
+                ^ "__))") attrs))
+
+and b_attrparam_to_string (param: b_attrparam_t) =
+  match param with
+  | AInt i -> string_of_int i
+  | AStr s -> s
+  | ACons (s, []) -> "__" ^ s ^ "__"
+  | ACons (s, params) ->
+     "__"
+     ^ s
+     ^ "__("
+     ^ (String.concat ", " (List.map b_attrparam_to_string params)) ^ ")"
+  | ASizeOf t -> "__sizeof__(" ^ (typ_to_string t) ^ ")"
+  | ASizeOfE p -> "__sizeofE__(" ^ (b_attrparam_to_string p) ^ ")"
+  | ASizeOfS ts -> "__sizeofS__(" ^ (btypsig_to_string ts) ^ ")"
+  | AAlignOf t -> "__alignof__(" ^ (typ_to_string t) ^ ")"
+  | AAlignOfE p -> "__alignofE__(" ^ (b_attrparam_to_string p) ^ ")"
+  | AAlignOfS ts -> "__alignofS__(" ^ (btypsig_to_string ts) ^ ")"
+  | AUnOp (unop, p) ->
+     (unop_to_print_string unop) ^ " " ^ (b_attrparam_to_string p)
+  | ABinOp (binop, p1, p2) ->
+     (b_attrparam_to_string p1)
+     ^ " "
+     ^ (binop_to_print_string binop)
+     ^ " "
+     ^ (b_attrparam_to_string p2)
+  | ADot (p, s) -> (b_attrparam_to_string p) ^ "." ^ s
+  | AStar p -> "*" ^ (b_attrparam_to_string p)
+  | AAddrOf p -> "&" ^ (b_attrparam_to_string p)
+  | AIndex (p1, p2) ->
+     (b_attrparam_to_string p1) ^ "[" ^ (b_attrparam_to_string p2) ^ "]"
+  | AQuestion (p1, p2, p3) ->
+     (b_attrparam_to_string p1)
+     ^ " ? "
+     ^ (b_attrparam_to_string p2)
+     ^ " : "
+     ^ (b_attrparam_to_string p3)
+  | AAssign (p1, p2) ->
+     (b_attrparam_to_string p1) ^ " = " ^ (b_attrparam_to_string p2)
+
+
+and btypsig_to_string (ts: btypsig_t) =
+  let s_attrs (attrs: b_attributes_t) =
+      match attrs with
+      | [] -> ""
+      | _ -> " " ^ (attributes_to_string attrs) in
+  match ts with
+  | TSArray (tts, Some i64, attrs) ->
+     (btypsig_to_string tts) ^ "[" ^ (Int64.to_string i64) ^ "]" ^ (s_attrs attrs)
+  | TSArray (tts, None, attrs) ->
+     (btypsig_to_string tts) ^ "[]" ^ (s_attrs attrs)
+  | TSPtr (tts, attrs) ->
+     "( " ^ (btypsig_to_string tts) ^ " *)" ^ (s_attrs attrs)
+  | TSComp (is_struct, name, attrs) ->
+     (if is_struct then "struct " else "union ") ^ name ^ (s_attrs attrs)
+  | TSFun (rts, Some tslist, _is_vararg, attrs) ->
+     (btypsig_to_string rts)
+     ^ " ("
+     ^ (String.concat ", " (List.map btypsig_to_string tslist))
+     ^ (s_attrs attrs)
+  | TSFun (rts, None, _is_vararg, attrs) ->
+     (btypsig_to_string rts) ^ "(?)" ^ (s_attrs attrs)
+  | TSEnum (name, attrs) -> "enum " ^ name ^ (s_attrs attrs)
+  | TSBase t -> typ_to_string t
 
 
-let rec typ_to_string (t: btype_t) =
+and typ_to_string (t: btype_t) =
   let ns_to_string ns =
     String.concat "" (List.map (fun n -> (tname_to_string n) ^ "::") ns) in
   let a = attributes_to_string in