Preconditions

CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml

@@ -27,6 +27,7 @@
 
 (* chutil *)
 open CHFormatStringParser
+open CHLogger
 open CHTraceResult
 open CHUtil
 
@@ -584,7 +585,15 @@ let arm_vfp_params
       (funargs: bfunarg_t list): fts_parameter_t list =
   let fmt (index: int) =
     match BCHBCAttributesUtil.get_format_archetype attrs index with
-    | Some fmtstringtype -> fmtstringtype
+    | Some fmtstringtype ->
+       let _ =
+         log_diagnostics_result
+           ~tag:"arm_vfp_parameters"
+           __FILE__ __LINE__
+           ["fmtstringtype: "
+            ^ (BCHFtsParameter.formatstring_type_to_string fmtstringtype);
+            "attr count: "  ^ (string_of_int (List.length attrs))] in
+       fmtstringtype
     | _ -> NoFormat in
   let (_, _, params) =
     List.fold_left

CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml

@@ -1040,63 +1040,116 @@ let get_access_sideeffect
      end
 
 
-let get_chk_post_one
+let get_chk_post_conditions
       (name: string)
       (fparams: fts_parameter_t list)
       (attrparams: b_attrparam_t list): xxpredicate_t list =
   let thisf = NamedConstant name in
   let rv = ReturnValue thisf in
   let zero = NumConstant CHNumerical.numerical_zero in
-  (* Resolve target term: bare predicate → return value; predicate + AInt → parameter *)
-  let target_result =
-    match attrparams with
-    | [ACons (pred, [])] -> Ok (pred, rv)
-    | [ACons (pred, []); AInt refindex] ->
+  let negone = NumConstant (CHNumerical.mkNumerical (-1)) in
+  let get_param (pl: b_attrparam_t list): bterm_t traceresult =
+    match pl with
+    | [] -> Ok rv
+    | [AInt 0] -> Ok rv
+    | [AInt refindex] when refindex > 0 ->
        let* par = get_par fparams refindex in
-       Ok (pred, ArgValue par)
-    | (ACons (tag, _)) :: _ ->
-       Error [(elocm __LINE__) ^ "chk_post tag not recognized: " ^ tag]
+       Ok (ArgValue par)
     | _ ->
        Error [(elocm __LINE__) ^ "chk_post params not recognized";
-              attrparams_to_string "attrparams" attrparams] in
-  TR.tfold
-    ~error:(fun e ->
-      begin
-        log_diagnostics_result
-          ~tag:"get_chk_post_one:not recognized"
-          ~msg:name
-          __FILE__ __LINE__
-          e;
-        []
-      end)
-    ~ok:(fun (pred, target) ->
-      let negone = NumConstant (CHNumerical.mkNumerical (-1)) in
-      match pred with
-      | "not_null"            -> [XXNotNull target]
-      | "null"                -> [XXNull target]
-      | "non_negative"        -> [XXNonNegative target]
-      | "not_zero"            -> [XXNotZero target]
-      | "positive"            -> [XXPositive target]
-      | "null_terminated"     -> [XXNullTerminated target]
-      | "new_memory"          -> [XXNewMemory (target, RunTimeValue)]
-      | "allocation_base"     -> [XXAllocationBase target]
-      | "trusted_string"      -> [XXTrustedString target]
-      | "trusted_os_cmd_string" -> [XXTrustedOsCmdString target]
-      | "tainted"             -> [XXTainted target]
-      | "negone"              -> [XXRelationalExpr (PEquals, target, negone)]
-      | "zero"                -> [XXRelationalExpr (PEquals, target, zero)]
-      | "negative"            -> [XXRelationalExpr (PLessThan, target, zero)]
-      | "nonpositive"         -> [XXRelationalExpr (PLessEqual, target, zero)]
-      | tag ->
-         begin
-           log_diagnostics_result
-             ~tag:"get_chk_post_one:tag not recognized"
-             ~msg:name
-             __FILE__ __LINE__
-             ["tag: " ^ tag];
-           []
-         end)
-    target_result
+              attrparams_to_string "attrparams" pl] in
+  let get_two_params (pl: b_attrparam_t list): (bterm_t * bterm_t) traceresult =
+    match pl with
+    | [AInt 0; AInt p2] ->
+       let* par = get_par fparams p2 in
+       Ok (rv, ArgValue par)
+    | [AInt p1; AInt p2] ->
+       let* par1 = get_par fparams p1 in
+       let* par2 = get_par fparams p2 in
+       Ok (ArgValue par1, ArgValue par2)
+    | _ ->
+       Error [(elocm __LINE__) ^ "chk_post params not recognized";
+              attrparams_to_string "attrparams" pl] in
+  let xpred =
+    match attrparams with
+    | (ACons ("not_null", [])) :: refparams ->
+       TR.tmap (fun t -> [XXNotNull t]) (get_param refparams)
+    | (ACons ("null", [])) :: refparams ->
+       TR.tmap (fun t -> [XXNull t]) (get_param refparams)
+    | (ACons ("non_negative", [])) :: refparams ->
+       TR.tmap (fun t -> [XXNonNegative t]) (get_param refparams)
+    | (ACons ("not_zero", [])) :: refparams ->
+       TR.tmap (fun t -> [XXNotZero t]) (get_param refparams)
+    | (ACons ("positive", [])) :: refparams ->
+       TR.tmap (fun t -> [XXPositive t]) (get_param refparams)
+    | (ACons ("null_terminated", [])) :: refparams ->
+       TR.tmap (fun t -> [XXNullTerminated t]) (get_param refparams)
+    | (ACons ("new_memory", [])) :: ([_; _] as refparams) ->
+       TR.tmap
+         (fun (t, sizeparam) -> [XXNewMemory (t, sizeparam)])
+         (get_two_params refparams)
+    | (ACons ("new_memory", [])) :: refparams ->
+       TR.tmap (fun t -> [XXNewMemory (t, RunTimeValue)]) (get_param refparams)
+    | (ACons ("new_memory", [AInt size])) :: refparams ->
+       let asize = NumConstant (CHNumerical.mkNumerical size) in
+       TR.tmap (fun t -> [XXNewMemory (t, asize)]) (get_param refparams)
+    | (ACons ("allocation_base", [])) :: refparams ->
+       TR.tmap (fun t -> [XXAllocationBase t]) (get_param refparams)
+    | (ACons ("trusted_string", [])) :: refparams ->
+       TR.tmap (fun t -> [XXTrustedString t]) (get_param refparams)
+    | (ACons ("trusted_os_cmd_string", [])) :: refparams ->
+       TR.tmap (fun t -> [XXTrustedOsCmdString t]) (get_param refparams)
+    | (ACons ("trusted_os_cmd_fmt_arg_string", [])) :: refparams ->
+       TR.tmap
+         (fun t -> [XXTrustedOsCmdFmtArgString (t, NO_QUOTES, None)])
+         (get_param refparams)
+    | (ACons ("trusted_os_cmd_fmt_arg_string", [ACons ("no_quotes", [])]))
+      :: refparams ->
+       TR.tmap
+         (fun t -> [XXTrustedOsCmdFmtArgString (t, NO_QUOTES, None)])
+         (get_param refparams)
+    | (ACons ("trusted_os_cmd_fmt_arg_string",
+              [ACons ("no_quotes", []); AInt size])) :: refparams ->
+       TR.tmap
+         (fun t -> [XXTrustedOsCmdFmtArgString (t, NO_QUOTES, Some size)])
+         (get_param refparams)
+    | (ACons ("tainted", [])) :: refparams ->
+       TR.tmap (fun t -> [XXTainted t]) (get_param refparams)
+    | (ACons ("negone", [])) :: refparams ->
+       TR.tmap
+         (fun t -> [XXRelationalExpr (PEquals, t, negone)])
+         (get_param refparams)
+    | (ACons ("zero", [])) :: refparams ->
+       TR.tmap
+         (fun t -> [XXRelationalExpr (PEquals, t, zero)])
+         (get_param refparams)
+    | (ACons ("negative", [])) :: refparams ->
+       TR.tmap
+         (fun t -> [XXRelationalExpr (PLessThan, t, zero)])
+         (get_param refparams)
+    | (ACons ("nonpositive", [])) :: refparams ->
+       TR.tmap
+         (fun t -> [XXRelationalExpr (PLessEqual, t, zero)])
+         (get_param refparams)
+    | (ACons (tag, _)) :: _ ->
+       Error [(elocm __LINE__)
+              ^ "chk_post tag " ^ tag ^ " not recognized in "
+              ^ (attrparams_to_string "argparams" attrparams)]
+    | _ ->
+       Error [(elocm __LINE__)
+              ^ "chk_post attrparams not recognized: "
+              ^ (attrparams_to_string "argparams" attrparams)] in
+  match xpred with
+  | Ok xl -> xl
+  | Error e ->
+     begin
+       log_error_result
+         ~tag:"get_check_post_conditions"
+         ~msg:name
+         __FILE__ __LINE__
+         [String.concat "; " e];
+       []
+     end
 
 
 let get_chk_qual_conditions
@@ -1184,11 +1237,11 @@ let convert_b_attributes_to_function_conditions
          (xpre, side @ xside, xpost, xepost, xqual)
 
       | Attr ("chk_post", attrparams) ->
-         let post = get_chk_post_one name fparameters attrparams in
+         let post = get_chk_post_conditions name fparameters attrparams in
          (xpre, xside, post @ xpost, xepost, xqual)
 
       | Attr ("chk_epost", attrparams) ->
-         let epost = get_chk_post_one name fparameters attrparams in
+         let epost = get_chk_post_conditions name fparameters attrparams in
          (xpre, xside, xpost, epost @ xepost, xqual)
 
       | Attr ("chk_qual", attrparams) ->

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -188,8 +188,17 @@ object (self)
              finfo#update_summary
                (finfo#get_summary#add_register_parameter_location
                   reg btype 4) in
-           let ftspar = finfo#get_summary#get_parameter_for_register reg in
-           Some (ArgValue ftspar))
+           TR.tfold
+             ~ok:(fun ftspar -> Some (ArgValue ftspar))
+             ~error:(fun e ->
+               begin
+                 log_error_result
+                   ~tag:"xpr_to_bterm"
+                   __FILE__ __LINE__
+                   ["v: " ^ (p2s v#toPretty); String.concat ", " e];
+                 None
+               end)
+             (finfo#get_summary#get_parameter_for_register reg))
          ~error:(fun e ->
            begin
              log_error_result
@@ -232,15 +241,23 @@ object (self)
     match xpr with
     | XConst (IntConst n) -> Some (NumConstant n)
     | XVar v when self#finfo#env#is_initial_register_value v ->
-       log_tfold
-         (log_error "xpr_to_bterm" "invalid register")
+       TR.tfold
          ~ok:(fun reg ->
            let _ =
              self#finfo#update_summary
                (self#finfo#get_summary#add_register_parameter_location
                   reg btype 4) in
-           let ftspar = self#finfo#get_summary#get_parameter_for_register reg in
-           Some (ArgValue ftspar))
+           TR.tfold
+             ~ok:(fun ftspar -> Some (ArgValue ftspar))
+             ~error:(fun e ->
+               begin
+                 log_error_result
+                   ~tag:"xpr_to_bterm"
+                   __FILE__ __LINE__
+                   ["v: " ^ (p2s v#toPretty); String.concat ", " e];
+                 None
+               end)
+             (self#finfo#get_summary#get_parameter_for_register reg))
          ~error:(fun _ -> None)
          (self#finfo#env#get_initial_register_value_register v)
     | XVar v when self#finfo#env#is_stack_parameter_value v ->
@@ -378,6 +395,9 @@ object (self)
        | Some xpr ->
           match xpr with
           | XConst (IntConst n) ->
+             (* The callee is a variadic function. Retrieve the actual format
+                string and parse it to determine the number of variadic arguments
+                in the call.*)
              let dw = BCHDoubleword.numerical_mod_to_doubleword n in
              if BCHStrings.string_table#has_string dw then
                let fmtstring = BCHStrings.string_table#get_string dw in
@@ -417,6 +437,82 @@ object (self)
                    ["No constant format string found in string table"];
                  None
                end
+          | XVar v when self#finfo#env#is_initial_register_value v ->
+             (* There is no constant format string. Instead the format string
+                argument is received from the caller's parameter. Retrieve the
+                the specification of the parameter by externalizing the expression
+                to a parameter. If the parameter spec (as obtained from a
+                header file) is a retricted format string, reconstruct a minimal
+                format string from its argument spec list, and parse in the
+                same way as before.*)
+             let bterm_o =
+               (new arm_expression_externalizer_t finfo)#xpr_to_bterm
+                 t_charptr (XVar v) in
+             (match bterm_o with
+              | Some (ArgValue ftspar) ->
+                 (match ftspar.apar_fmt with
+                  | RestrictedPrintFormat sl when sl <> [] ->
+                     let fmtstring =
+                       String.concat " " (List.map (fun s -> "%" ^ s) sl) in
+                     let _ =
+                       log_diagnostics_result
+                         ~tag:"get_annotated_format_arguments:restricted_format"
+                         ~msg:finfo#get_name
+                         __FILE__ __LINE__
+                         ["restricted fmtstring: " ^ fmtstring] in
+                     let fmtspec = parse_formatstring fmtstring false in
+                     if fmtspec#has_arguments then
+                       let argspecs = fmtspec#get_arguments in
+                       let argxprs = List.map (fun (_, x) -> x) callargs in
+                       (match CHUtil.list_slice argxprs
+                                index (List.length argspecs) with
+                        | Some fmtargs ->
+                           Some
+                             (List.map2
+                                (fun argspec argxpr ->
+                                  let fw =
+                                    if argspec#has_fieldwidth then
+                                      argspec#get_fieldwidth
+                                    else
+                                      CHFormatStringParser.NoFieldwidth in
+                                  (argspec#get_conversion, fw, argxpr))
+                                argspecs fmtargs)
+                        | _ ->
+                           begin
+                             log_diagnostics_result
+                               ~tag:"get_annotated_format_arguments:no formatargs"
+                               ~msg:finfo#get_name
+                               __FILE__ __LINE__
+                               ["restricted fmtstring: no arguments: " ^ fmtstring];
+                             None
+                           end)
+                     else
+                       begin
+                         log_diagnostics_result
+                           ~tag:"get_annotated_format_arguments:restricted_format"
+                           ~msg:finfo#get_name
+                           __FILE__ __LINE__
+                           ["restricted fmtstring: no arguments: " ^ fmtstring];
+                         None
+                       end
+                  | _ ->
+                     begin
+                       log_diagnostics_result
+                         ~tag:"get_annotated_format_arguments: ftspar: no format"
+                         ~msg:finfo#get_name
+                         __FILE__ __LINE__
+                         ["param: " ^ (fts_parameter_to_string ftspar)];
+                       None
+                     end)
+              | _ ->
+                 begin
+                   log_diagnostics_result
+                     ~tag:"get_annotated_format_arguments:initial_register_value"
+                     ~msg:finfo#get_name
+                     __FILE__ __LINE__
+                     ["format string: " ^ (p2s v#toPretty)];
+                   None
+                 end)
           | _ ->
              begin
                log_diagnostics_result
@@ -2233,8 +2329,10 @@ object (self)
         ~msg:(eloc __LINE__)
         (fun reg ->
           if self#f#get_summary#has_parameter_for_register reg then
-            let param = self#f#get_summary#get_parameter_for_register reg in
-            Ok param.apar_type
+            TR.tbind
+              ~msg:(eloc __LINE__)
+              (fun param -> Ok param.apar_type)
+              (self#f#get_summary#get_parameter_for_register reg)
           else
             let ty = self#env#get_variable_type v in
             match ty with
@@ -3360,10 +3458,19 @@ object (self)
          [ABSTRACT_VARS [lhs]]
 
        else
+         let fndata = self#f#get_function_data in
          let rhs =
+           if fndata#has_regvar_freeze self#ia then
+             let _ =
+               log_diagnostics_result
+                 ~tag:"get_assign_commands_r:freeze"
+                 ~msg:self#cia
+                 __FILE__ __LINE__
+                 ["lhs: " ^ (p2s lhs#toPretty)] in
+             XVar (self#f#env#mk_frozen_value lhs self#cia)
            (* if rhs is a composite symbolic expression, create a new variable
             for it *)
-           if self#is_composite_symbolic_value rhs then
+           else if self#is_composite_symbolic_value rhs then
              XVar (self#env#mk_symbolic_value rhs)
            else
              rhs in
@@ -3372,7 +3479,7 @@ object (self)
          let (rhscmds, rhs_c) = xpr_to_numexpr reqN reqC rhs in
          let cmds = rhscmds @ [ASSIGN_NUM (lhs, rhs_c)] in
 
-         let fndata = self#f#get_function_data in
+
          match fndata#get_regvar_intro self#ia with
          | Some rvi when rvi.rvi_cast && Option.is_some rvi.rvi_vartype ->
             TR.tfold