Podischarge

CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml

@@ -592,7 +592,8 @@ let arm_vfp_params
            __FILE__ __LINE__
            ["fmtstringtype: "
             ^ (BCHFtsParameter.formatstring_type_to_string fmtstringtype);
-            "attr count: "  ^ (string_of_int (List.length attrs))] in
+            "attr count: "  ^ (string_of_int (List.length attrs));
+            "varargs: " ^ (if varargs then "yes" else "no")] in
        fmtstringtype
     | _ -> NoFormat in
   let (_, _, params) =
@@ -611,11 +612,7 @@ let arm_vfp_params
         | Ok btype, Ok tysize ->
            (* assume no packing at the argument top level *)
            let size = if tysize < 4 then 4 else tysize in
-           let fmt =
-             if varargs then
-               fmt index
-             else
-               NoFormat in
+           let fmt = fmt index in
            let (param, new_state) =
              if (is_int btype || is_pointer btype || is_enum btype) && size = 4 then
                get_arm_int_param_next_state ~fmt size name btype aa_state index

CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml

@@ -351,6 +351,22 @@ let get_trusted_os_cmd_fmt_string_precondition
             attrparams_to_string "argparams" argparams]
 
 
+let get_trusted_os_cmd_fmt_arg_string_precondition
+      (fparams: fts_parameter_t list)
+      (tagparams: b_attrparam_t list)
+      (argparams: b_attrparam_t list): xxpredicate_t traceresult =
+  match (tagparams, argparams) with
+  | ([ACons ("no_quotes", [])], [AInt refindex]) ->
+    let* par = get_par fparams refindex in
+    Ok (XXTrustedOsCmdFmtArgString (ArgValue par, NO_QUOTES, None))
+
+  | _ ->
+     Error [(elocm __LINE__) ^ "trusted_os_cmd_fmt_arg_string params not recognized";
+            fparams_to_string fparams;
+            attrparams_to_string "tagparams" tagparams;
+            attrparams_to_string "argparams" argparams]
+
+
 let string_to_relational_op (s: string): relational_op_t traceresult =
   match s with
   | "eq"  -> Ok PEquals
@@ -490,6 +506,21 @@ let get_chk_pre_conditions
       (fparams: fts_parameter_t list)
       (attrparams: b_attrparam_t list): xxpredicate_t list =
   match attrparams with
+
+  | (ACons ("allocation_base", tagparams)) :: argparams ->
+     TR.tfold
+       ~ok:(fun xpre -> [xpre])
+       ~error:(fun e ->
+         begin
+           log_error_result
+             ~tag:"get_chk_preconditions:allocation_base"
+             ~msg:name
+             __FILE__ __LINE__
+             [String.concat ", " e];
+           []
+         end)
+       (get_allocation_base_precondition fparams tagparams argparams)
+
   | (ACons ("deref_read", tagparams)) :: argparams ->
      TR.tfold
        ~ok:(fun xpre -> [xpre])
@@ -532,173 +563,173 @@ let get_chk_pre_conditions
          end)
        (get_initialized_range_precondition fparams tagparams argparams)
 
-  | (ACons ("not_null", tagparams)) :: argparams ->
+  | (ACons ("input_format_string", tagparams)) :: argparams ->
      TR.tfold
        ~ok:(fun xpre -> [xpre])
        ~error:(fun e ->
          begin
            log_error_result
-             ~tag:"get_chk_preconditions:not_null"
+             ~tag:"get_chk_preconditions:input_format_string"
              ~msg:name
              __FILE__ __LINE__
              [String.concat ", " e];
            []
          end)
-       (get_not_null_precondition fparams tagparams argparams)
+       (get_input_format_string_precondition fparams tagparams argparams)
 
-  | (ACons ("null_terminated", tagparams)) :: argparams ->
+  | (ACons ("non_negative", tagparams)) :: argparams ->
      TR.tfold
        ~ok:(fun xpre -> [xpre])
        ~error:(fun e ->
          begin
            log_error_result
-             ~tag:"get_chk_preconditions:null_terminated"
+             ~tag:"get_chk_preconditions:non_negative"
              ~msg:name
              __FILE__ __LINE__
              [String.concat ", " e];
            []
          end)
-       (get_null_terminated_precondition fparams tagparams argparams)
+       (get_non_negative_precondition fparams tagparams argparams)
 
-  | (ACons ("output_format_string", tagparams)) :: argparams ->
+  | (ACons ("no_overlap", tagparams)) :: argparams ->
      TR.tfold
        ~ok:(fun xpre -> [xpre])
        ~error:(fun e ->
          begin
            log_error_result
-             ~tag:"get_chk_preconditions:output_format_string"
+             ~tag:"get_chk_preconditions:no_overlap"
              ~msg:name
              __FILE__ __LINE__
              [String.concat ", " e];
            []
          end)
-       (get_output_format_string_precondition fparams tagparams argparams)
+       (get_no_overlap_precondition fparams tagparams argparams)
 
-  | (ACons ("restricted_output_format_string", tagparams)) :: argparams ->
+  | (ACons ("not_null", tagparams)) :: argparams ->
      TR.tfold
        ~ok:(fun xpre -> [xpre])
        ~error:(fun e ->
          begin
            log_error_result
-             ~tag:"get_chk_preconditions:restricted_output_format_string"
+             ~tag:"get_chk_preconditions:not_null"
              ~msg:name
              __FILE__ __LINE__
              [String.concat ", " e];
            []
          end)
-       (get_restricted_output_format_string_precondition fparams tagparams argparams)
+       (get_not_null_precondition fparams tagparams argparams)
 
-  | (ACons ("trusted_os_cmd_fmt_string", tagparams)) :: argparams ->
+  | (ACons ("not_zero", tagparams)) :: argparams ->
      TR.tfold
        ~ok:(fun xpre -> [xpre])
        ~error:(fun e ->
          begin
            log_error_result
-             ~tag:"get_chk_preconditions:trusted_os_cmd_fmt_string"
+             ~tag:"get_chk_preconditions:not_zero"
              ~msg:name
              __FILE__ __LINE__
              [String.concat ", " e];
            []
          end)
-       (get_trusted_os_cmd_fmt_string_precondition fparams tagparams argparams)
+       (get_not_zero_precondition fparams tagparams argparams)
 
-  | (ACons ("input_format_string", tagparams)) :: argparams ->
+  | (ACons ("null_terminated", tagparams)) :: argparams ->
      TR.tfold
        ~ok:(fun xpre -> [xpre])
        ~error:(fun e ->
          begin
            log_error_result
-             ~tag:"get_chk_preconditions:input_format_string"
+             ~tag:"get_chk_preconditions:null_terminated"
              ~msg:name
              __FILE__ __LINE__
              [String.concat ", " e];
            []
          end)
-       (get_input_format_string_precondition fparams tagparams argparams)
+       (get_null_terminated_precondition fparams tagparams argparams)
 
-  | (ACons ("not_zero", tagparams)) :: argparams ->
+  | (ACons ("output_format_string", tagparams)) :: argparams ->
      TR.tfold
        ~ok:(fun xpre -> [xpre])
        ~error:(fun e ->
          begin
            log_error_result
-             ~tag:"get_chk_preconditions:not_zero"
+             ~tag:"get_chk_preconditions:output_format_string"
              ~msg:name
              __FILE__ __LINE__
              [String.concat ", " e];
            []
          end)
-       (get_not_zero_precondition fparams tagparams argparams)
+       (get_output_format_string_precondition fparams tagparams argparams)
 
-  | (ACons ("non_negative", tagparams)) :: argparams ->
+  | (ACons ("relational_expr", tagparams)) :: argparams ->
      TR.tfold
        ~ok:(fun xpre -> [xpre])
        ~error:(fun e ->
          begin
            log_error_result
-             ~tag:"get_chk_preconditions:non_negative"
+             ~tag:"get_chk_preconditions:relational_expr"
              ~msg:name
              __FILE__ __LINE__
              [String.concat ", " e];
            []
          end)
-       (get_non_negative_precondition fparams tagparams argparams)
+       (get_relational_expr_precondition fparams tagparams argparams)
 
-  | (ACons ("relational_expr", tagparams)) :: argparams ->
+  | (ACons ("restricted_output_format_string", tagparams)) :: argparams ->
      TR.tfold
        ~ok:(fun xpre -> [xpre])
        ~error:(fun e ->
          begin
            log_error_result
-             ~tag:"get_chk_preconditions:relational_expr"
+             ~tag:"get_chk_preconditions:restricted_output_format_string"
              ~msg:name
              __FILE__ __LINE__
              [String.concat ", " e];
            []
          end)
-       (get_relational_expr_precondition fparams tagparams argparams)
+       (get_restricted_output_format_string_precondition fparams tagparams argparams)
 
-  | (ACons ("no_overlap", tagparams)) :: argparams ->
+  | (ACons ("trusted_string", tagparams)) :: argparams ->
      TR.tfold
        ~ok:(fun xpre -> [xpre])
        ~error:(fun e ->
          begin
            log_error_result
-             ~tag:"get_chk_preconditions:no_overlap"
+             ~tag:"get_chk_preconditions:trusted_string"
              ~msg:name
              __FILE__ __LINE__
              [String.concat ", " e];
            []
          end)
-       (get_no_overlap_precondition fparams tagparams argparams)
+       (get_trusted_string_precondition fparams tagparams argparams)
 
-  | (ACons ("allocation_base", tagparams)) :: argparams ->
+  | (ACons ("trusted_os_cmd_fmt_arg_string", tagparams)) :: argparams ->
      TR.tfold
        ~ok:(fun xpre -> [xpre])
        ~error:(fun e ->
          begin
            log_error_result
-             ~tag:"get_chk_preconditions:allocation_base"
+             ~tag:"get_chk_preconditions:trusted_os_cmd_fmt_arg_string"
              ~msg:name
              __FILE__ __LINE__
              [String.concat ", " e];
            []
          end)
-       (get_allocation_base_precondition fparams tagparams argparams)
+       (get_trusted_os_cmd_fmt_arg_string_precondition fparams tagparams argparams)
 
-  | (ACons ("trusted_string", tagparams)) :: argparams ->
+  | (ACons ("trusted_os_cmd_fmt_string", tagparams)) :: argparams ->
      TR.tfold
        ~ok:(fun xpre -> [xpre])
        ~error:(fun e ->
          begin
            log_error_result
-             ~tag:"get_chk_preconditions:trusted_string"
+             ~tag:"get_chk_preconditions:trusted_os_cmd_fmt_string"
              ~msg:name
              __FILE__ __LINE__
              [String.concat ", " e];
            []
          end)
-       (get_trusted_string_precondition fparams tagparams argparams)
+       (get_trusted_os_cmd_fmt_string_precondition fparams tagparams argparams)
 
   | (ACons ("trusted_os_cmd_string", tagparams)) :: argparams ->
      TR.tfold

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -208,6 +208,35 @@ object (self)
              None
            end)
          (finfo#env#get_initial_register_value_register v)
+    | XVar v when finfo#env#is_stack_parameter_value v ->
+       let indexopt = finfo#env#get_stack_parameter_index v in
+       (match indexopt with
+        | Some index ->
+           let _ =
+             finfo#update_summary
+               (finfo#get_summary#add_stack_parameter_location
+                  (4 * index) btype 4) in
+           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);
+                    "index: " ^ (string_of_int index);
+                    String.concat ", " e];
+                 None
+               end)
+             (finfo#get_summary#get_parameter_at_stack_offset (4 * index))
+        | _ ->
+           begin
+             log_diagnostics_result
+               ~tag:"xpr_to_bterm:stack-parameter"
+               __FILE__ __LINE__
+               ["xpr: " ^ (x2s xpr)];
+             None
+           end)
     | XOp ((Xf "indexsize"), [xx]) ->
        let optt = self#xpr_to_bterm t_int xx in
        (match optt with
@@ -268,9 +297,15 @@ object (self)
             self#finfo#update_summary
               (self#finfo#get_summary#add_stack_parameter_location
                  (4 * index) btype 4) in
-          let ftspar =
-            self#finfo#get_summary#get_parameter_at_stack_offset (4 * index) in
-          Some (ArgValue ftspar)
+          TR.tfold
+            ~ok:(fun ftspar -> Some (ArgValue ftspar))
+            ~error:(fun e ->
+              log_error_result
+                ~tag:"xpr_to_bterm"
+                __FILE__ __LINE__
+                ["v: " ^ (p2s v#toPretty); String.concat ", " e];
+              None)
+            (self#finfo#get_summary#get_parameter_at_stack_offset (4 * index))
        | _ -> None)
     | XOp ((Xf "indexsize"), [xx]) ->
        let optt = self#xpr_to_bterm t_int xx in
@@ -835,12 +870,12 @@ object (self)
                  let fmtargs = fmtspec#get_arguments in
                  let orig_npar = List.length (get_fts_parameters fintf) in
                  let newfintf = add_format_spec_parameters fintf isinput fmtargs in
+                 let new_pars =
+                   List.filteri
+                     (fun i _ -> i >= orig_npar)
+                     (get_fts_parameters newfintf) in
                  let new_sem =
                    if isinput then
-                     let new_pars =
-                       List.filteri
-                         (fun i _ -> i >= orig_npar)
-                         (get_fts_parameters newfintf) in
                      let new_ses =
                        List.map (fun p ->
                            match p.apar_type with
@@ -856,7 +891,20 @@ object (self)
                      {sem with
                        fsem_sideeffects = sem.fsem_sideeffects @ new_ses}
                    else
-                     sem in
+                     let new_preconditions =
+                       List.fold_left (fun acc p ->
+                           if is_char_pointer p.apar_type then
+                             let argval = ArgValue p in
+                             let ntp = ArgNullTerminatorPos argval in
+                             let newpres =
+                               [XXBuffer (t_char, argval, ntp);
+                                XXInitializedRange (t_char, argval, ntp);
+                                XXNullTerminated argval;
+                                XXNotNull argval] in
+                             newpres @ acc
+                           else
+                             acc) [] new_pars in
+                     {sem with fsem_pre = sem.fsem_pre @ new_preconditions} in
                  Some (newfintf, new_sem)
                else
                  None

CodeHawk/CHB/bchlib/bCHFunctionInterface.ml

@@ -960,13 +960,13 @@ let add_function_stack_parameter_location
          loc :: fintf.fintf_parameter_locations in
      {fintf with fintf_parameter_locations = newlocations}
   | Some bctype ->
-     let _ =
-       chlog#add
-         "add-function-stack-parameter-location"
-         (LBLOCK [
-              STR "Location not added; bctype is fixed: ";
-              STR (btype_to_string bctype)]) in
-     fintf
+     begin
+       log_diagnostics_result
+         ~tag:"add_function_stack_parameter_location: not added"
+         __FILE__ __LINE__
+         ["fixed function type: " ^ (btype_to_string bctype)];
+       fintf
+     end
 
 
 let add_function_global_parameter_location