Libcreplacement

CodeHawk/CHB/bchcmdline/bCHXMakeLibSummary.ml

@@ -80,14 +80,14 @@ let speclist = [
 
 let ccNode =
   xml_string
-    "copyright-notice" "Copyright 2012-2024, Henny Sipma, Palo Alto, CA 94304"
+    "copyright-notice" "Copyright 2012-2026, Henny Sipma, Palo Alto, CA 94304"
 
 let usage_msg = "mktemplate name"
 let read_args () = Arg.parse speclist (fun s -> name := s) usage_msg
 
 let post_shortcuts = [
   "notzero-zero"; "nonzero-zero"; "one-zero"; "zero-negone";
-  "notnull"; "notnull-null";
+  "notnull"; "notnull-null"; "nonnegative-negone";
   "nonnegative-negative"; "positive-nonpositive"; "positive-zero"]
 
 

CodeHawk/CHB/bchlib/bCHBCAttributes.ml

@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2024-2025  Aarno Labs LLC
+   Copyright (c) 2024-2026  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
@@ -88,17 +88,27 @@ let convert_b_attributes_to_function_conditions
             | [ACons (("write_only" | "read_write"), []); AInt refindex] ->
                let par = get_par refindex in
                let ty = get_derefty par in
-               ([XXBuffer (ty, ArgValue par, RunTimeValue)],
+               ([XXBuffer (ty, ArgValue par, RunTimeValue);
+                 XXBlockWrite (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)],
+               ([XXBuffer (ty, ArgValue rpar, ArgValue spar);
+                 XXBlockWrite (ty, ArgValue rpar, RunTimeValue)],
                 [XXBlockWrite (ty, ArgValue rpar, ArgValue spar)])
 
+            | [ACons ("write_only", [AInt buffersize]); AInt refindex] ->
+               let par = get_par refindex in
+               let ty = get_derefty par in
+               let bytesize = CHNumerical.mkNumerical buffersize in
+               ([XXBuffer (ty, ArgValue par, NumConstant bytesize);
+                 XXBlockWrite (ty, ArgValue par, NumConstant bytesize)],
+                [XXBlockWrite (ty, ArgValue par, NumConstant bytesize)])
+
             | _ ->
                begin
                  log_error_result
@@ -111,5 +121,72 @@ let convert_b_attributes_to_function_conditions
                  ([], [])
                end) in
          (pre @ xpre, side @ xside, xpost)
+      | Attr ("chk_pre", params) ->
+         let pre =
+           (match params with
+            | [ACons ("deref_read", []); AInt refindex] ->
+               let par = get_par refindex in
+               let ty = get_derefty par in
+               [XXBuffer (ty, ArgValue par, RunTimeValue)]
+
+            | [ACons ("deref_read", []); AInt refindex; AInt sizeindex] ->
+               let par1 = get_par refindex in
+               let par2 = get_par sizeindex in
+               let ty = get_derefty par1 in
+               [XXBuffer (ty, ArgValue par1, ArgValue par2)]
+
+            | [ACons ("deref_read", [AInt size]); AInt refindex] ->
+               let par = get_par refindex in
+               let ty = get_derefty par in
+               let c = CHNumerical.mkNumerical size in
+               [XXBuffer (ty, ArgValue par, NumConstant c)]
+
+            | [ACons ("deref_read", [ACons ("ntp", [])]); AInt refindex] ->
+               let par = get_par refindex in
+               let ty = get_derefty par in
+               [XXBuffer (ty, ArgValue par, ArgNullTerminatorPos (ArgValue par))]
+
+            | [ACons ("deref_write", []); AInt refindex] ->
+               let par = get_par refindex in
+               let ty = get_derefty par in
+               [XXBlockWrite (ty, ArgValue par, RunTimeValue)]
+
+            | [ACons ("deref_write", []); AInt refindex; AInt sizeindex] ->
+               let par1 = get_par refindex in
+               let par2 = get_par sizeindex in
+               let ty = get_derefty par1 in
+               [XXBlockWrite (ty, ArgValue par1, ArgValue par2)]
+
+            | [ACons ("deref_write", [AInt size]); AInt refindex] ->
+               let par = get_par refindex in
+               let ty = get_derefty par in
+               let c = CHNumerical.mkNumerical size in
+               [XXBlockWrite (ty, ArgValue par, NumConstant c)]
+
+            | [ACons ("not_null", []); AInt refindex] ->
+               let par = get_par refindex in
+               [XXNotNull (ArgValue par)]
+
+            | [ACons ("null_terminated", []); AInt refindex] ->
+               let par = get_par refindex in
+               [XXNullTerminated (ArgValue par)]
+
+            | [ACons ("initialized_range", [ACons ("ntp", [])]); AInt refindex] ->
+               let par = get_par refindex in
+               let ty = get_derefty par in
+               [XXInitializedRange (
+                    ty, ArgValue par, ArgNullTerminatorPos (ArgValue par))]
+
+            | _ ->
+               begin
+                 log_error_result
+                   ~tag:"convert_b_attributes_to_function_conditions"
+                   ~msg:(name ^ ":chk_pre")
+                   __FILE__ __LINE__
+                   [String.concat ", " (List.map b_attrparam_to_string params)];
+                 []
+               end) in
+         (pre @ xpre, xside, xpost)
+
       | _ ->
          acc) ([], [], []) attrs

CodeHawk/CHB/bchlib/bCHBCTypeUtil.ml

@@ -83,6 +83,7 @@ let t_ptrto t = TPtr (t,[])
 
 let ptr_deref (t: btype_t): btype_t =
   match t with
+  | TPtr (TVoid _, _) -> t_uchar
   | TPtr (dty, _) -> dty
   | _ ->
      raise

CodeHawk/CHB/bchlib/bCHBCTypeXml.ml

@@ -60,7 +60,40 @@ let raise_error (node: xml_element_int) (msg: pretty_t) =
 
 
 let ch_named_struct_types = [
-    "ch_FILE"
+    "ch__addrinfo";
+    "ch__DIR";
+    "ch__dirent";
+    "ch__fd_set";    (* used in select *)
+    "ch__FILE";
+    "ch__fpos_t";    (* this may or may not be a struct, depending on arch *)
+    "ch__group";     (* used in getgrgid *)
+    "ch__hostent";
+    "ch__in_addr";
+    "ch__iovec";     (* used in writev *)
+    "ch__msghdr";    (* used in recvmsg, sendmsg *)
+    "ch__netent";
+    "ch__passwd";    (* used in getpwnam *)
+    "ch__pollfd";
+    "ch__pthread_attr_t";
+    "ch__pthread_cond_t";
+    "ch__pthread_mutex_t";
+    "ch__pthread_mutexattr_t";
+    "ch__pthread_start_routine";
+    "ch__pthread_t";
+    "ch__rlimit";    (* used in getrlimit *)
+    "ch__rusage";    (* used in getrusage *)
+    "ch__sigaction"; (* used in sigaction *)
+    "ch__sigset_t";  (* used in sigaddset *)
+    "ch__sockaddr";
+    "ch__spwd";      (* used in getspname *)
+    "ch__stat";
+    "ch__statfs";
+    "ch__sysinfo";
+    "ch__termios";   (* used in tcgetattr *)
+    "ch__timespec";  (* used in nanosleep *)
+    "ch__timeval";
+    "ch__timezone";
+    "ch__tm"
   ]
 
 let register_ch_named_struct_types () =
@@ -71,28 +104,59 @@ let register_ch_named_struct_types () =
    btype enumerations*)
 let get_standard_txt_type (t: string): btype_t option =
   match t with
+  | "__uClibc_main_fptr" ->
+     Some (TPtr (TFun (TInt (IInt, []),
+                       Some [("argc", TInt (IInt, []), []);
+                             ("argv", TPtr (TPtr (TInt (IUChar, []), []),  []), [])],
+                             false, []), []))
+  | "atexit_fptr" -> Some (TPtr (TFun (TVoid [], Some [], false, []), []))
   | "BOOL" -> Some (TInt (IBool, []))
   | "Boolean" -> Some (TInt (IBool, []))
   | "BSTR" -> Some (TPtr (TInt (IWChar, []), []))
   | "byte" -> Some (TInt (IUChar, []))
   | "BYTE" -> Some (TInt (IUChar, []))
   | "char" -> Some (TInt (IChar, []))
+  | "clock_t" -> Some (TInt (IInt, []))
+  | "comparison_fptr" ->                       (* used in bsearch *)
+     Some (TFun (TInt (IInt, []),
+                 Some [("x1", TPtr (TVoid [], []), []);
+                       ("x2", TPtr (TVoid [], []), [])],
+                 false, []))
+  | "dir_select_fptr" ->
+     Some (TFun (TInt (IInt, []),
+                       Some [("direntry", TPtr (TNamed ("ch__dirent", []), []), [])],
+                              false, []))
   | "float" -> Some (TFloat (FFloat, FScalar, []))
   | "double" -> Some (TFloat (FDouble, FScalar, []))
   | "DWORD" -> Some (TInt (IUInt, []))
+  | "gid_t" -> Some (TInt (IUInt, []))
+  | "id_t" -> Some (TInt (IUInt, []))     (* used in getpriority *)
   | "int" -> Some (TInt (IInt, []))
   | "Integer" -> Some (TInt (IInt, []))
   | "long" -> Some (TInt (ILong, []))
   | "LONG" -> Some (TInt (ILong, []))
+  | "long_long" -> Some (TInt (ILongLong, []))
+  | "long long" -> Some (TInt (ILongLong, []))
+  | "mode_t" -> Some (TInt (IInt, []))    (* used in chmod *)
+  | "nfds_t" -> Some (TInt (IUInt, []))   (* used in poll *)
   | "off_t" -> Some (TInt (IULong, []))
   | "OLECHAR" -> Some (TInt (IWChar, []))
+  | "pid_t" -> Some (TInt (IUInt, []))
+  | "pthread_start_routine" ->
+     Some (TPtr (TFun (TVoid [], Some [], false, []), []))
+  | "sem_t" -> Some (TInt (IInt, []))     (* used in semaphore functions *)
   | "size_t" -> Some (TInt (IUInt, []))
   | "SIZE_T" -> Some (TInt (IUInt, []))
+  | "socklen_t" -> Some (TInt (IInt, []))  (* may also be unsigned *)
+  | "speed_t" -> Some (TInt (IUInt, []))   (* used in cfgetispeed *)
   | "ssize_t" -> Some (TInt (ILong, []))
   | "time_t" -> Some (TInt (ILong, []))
+  | "uid_t" -> Some (TInt (IUInt, []))
   | "UINT" -> Some (TInt (IUInt, []))
   | "uint16_t" -> Some (TInt (IUShort, []))
   | "uint32_t" -> Some (TInt (IUInt, []))
+  | "u_long" -> Some (TInt (IULong, []))
+  | "u_long_long" -> Some (TInt (IULongLong, []))
   | "unknown" -> Some (TUnknown [])
   | "UNKNOWN" -> Some (TUnknown [])
   | "void" -> Some (TVoid ([]))

CodeHawk/CHB/bchlib/bCHFunctionInfo.ml

@@ -6,7 +6,7 @@
 
    Copyright (c) 2005-2020 Kestrel Technology LLC
    Copyright (c) 2020      Henny Sipma
-   Copyright (c) 2021-2025 Aarno Labs LLC
+   Copyright (c) 2021-2026 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
@@ -75,6 +75,7 @@ open BCHUtilities
 open BCHVariable
 open BCHVariableNames
 open BCHXPODictionary
+open BCHXPOPredicate
 
 module H = Hashtbl
 module LF = CHOnlineCodeSet.LanguageFactory
@@ -1710,6 +1711,88 @@ object (self)
 
   method proofobligations = proofobligations
 
+  method discharge_proofobligations =
+    let openpos = self#proofobligations#open_proofobligations in
+    List.iter (fun po ->
+        let newstatus =
+          match po#xpo with
+          | XPOBuffer (
+              _ty,
+              XOp (XMinus, [XVar v; XConst (IntConst off)]),
+              XConst (IntConst size))
+            | XPOBlockWrite (
+              _ty,
+              XOp (XMinus, [XVar v; XConst (IntConst off)]),
+              XConst (IntConst size))
+               when self#env#is_initial_stackpointer_value v ->
+             let buffer = self#stackframe#get_max_slot_size off#neg#toInt in
+             (match buffer with
+              | Some slotsize ->
+                 if size#toInt <= slotsize then
+                   Discharged (
+                       "buffer size " ^ size#toString
+                       ^ " fits in available space of "
+                       ^ (string_of_int slotsize)
+                       ^ " bytes")
+                 else
+                   Violated (
+                       "buffer size "
+                       ^ size#toString ^ " is too large; available space is "
+                       ^ (string_of_int slotsize) ^ " bytes")
+              | _ ->
+                 let _ =
+                   log_diagnostics_result
+                     ~tag:"discharge_proofobligations:open"
+                     ~msg:(p2s po#loc#toPretty)
+                     __FILE__ __LINE__
+                     ["xpo: " ^ (p2s (xpo_predicate_to_pretty po#xpo));
+                      "Unable to determine buffer size at offset "
+                        ^ off#toString] in
+                 Open)
+          | XPOBlockWrite (ty, XVar v, bwlen) when
+                 self#env#is_initial_register_value v ->
+               TR.tfold
+                 ~ok:(fun reg ->
+                   let paramty = TPtr (ty, []) in
+                   let _ =
+                     self#update_summary
+                       (self#get_summary#add_register_parameter_location
+                          reg paramty 4) in
+                   let ftspar = self#get_summary#get_parameter_for_register reg in
+                   let dst = ArgValue ftspar in
+                   let lenterm =
+                     match bwlen with
+                     | XConst (IntConst size) -> NumConstant size
+                     | _ -> RunTimeValue in
+                   let xpred = XXBlockWrite (ty, dst, lenterm) in
+                   let updatedsummary = self#get_summary#add_precondition xpred in
+                   let updatedsummary = updatedsummary#add_sideeffect xpred in
+                   let _ = self#update_summary updatedsummary in
+                   Delegated xpred)
+                 ~error:(fun e ->
+                   begin
+                     log_error_result
+                       ~tag:"delegate_proofobligation"
+                       __FILE__ __LINE__
+                       ["v: " ^ (p2s v#toPretty);
+                        String.concat ", " e];
+                     Open
+                   end)
+                 (self#env#get_initial_register_value_register v)
+          | _ -> Open in
+        match newstatus with
+        | Open -> ()
+        | _ ->
+           begin
+             log_diagnostics_result
+               ~tag:"discharge_proofobligations"
+               ~msg:(p2s po#loc#toPretty)
+               __FILE__ __LINE__
+               ["xpo: " ^ (p2s (xpo_predicate_to_pretty po#xpo));
+                "status: " ^ (p2s (po_status_to_pretty newstatus))];
+             po#update_status newstatus
+           end) openpos
+
   method set_instruction_bytes (ia:ctxt_iaddress_t) (b:string) =
     H.add instrbytes ia b
 

CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml

@@ -538,6 +538,27 @@ object (self)
     else
       None
 
+  method get_max_slot_size (offset: int): int option =
+    if H.mem stackslots offset then
+      let keys = H.fold (fun k _ a -> k :: a) stackslots [] in
+      let keys = List.sort Stdlib.compare keys in
+      List.fold_left (fun acc i ->
+          match acc with
+          | Some _ -> acc
+          | _ ->
+             if i > offset then
+               Some (i - offset)
+             else
+               None) None keys
+    else
+      begin
+        log_diagnostics_result
+          ~tag:"get_max_slot_size:stackslot not found"
+          __FILE__ __LINE__
+          ["offset: " ^ (string_of_int offset)];
+        None
+      end
+
   method add_stackslot
            ?(name = None)
            ?(btype = t_unknown)