Restrictedformat

CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml

@@ -315,6 +315,24 @@ let get_output_format_string_precondition
             attrparams_to_string "argparams" argparams]
 
 
+let get_restricted_output_format_string_precondition
+      (fparams: fts_parameter_t list)
+      (tagparams: b_attrparam_t list)
+      (argparams: b_attrparam_t list): xxpredicate_t traceresult =
+  match (tagparams, argparams) with
+  | ([], (AInt refindex) :: rest)
+    when List.for_all (function AStr _ -> true | _ -> false) rest
+         && rest <> [] ->
+     let* par = get_par fparams refindex in
+     let specs = List.map (function AStr s -> s | _ -> assert false) rest in
+     Ok (XXRestrictedOutputFormatString (ArgValue par, specs))
+  | _ ->
+     Error [(elocm __LINE__) ^ "restricted_output_format_string params not recognized";
+            fparams_to_string fparams;
+            attrparams_to_string "tagparams" tagparams;
+            attrparams_to_string "argparams" argparams]
+
+
 let get_trusted_os_cmd_fmt_string_precondition
       (fparams: fts_parameter_t list)
       (tagparams: b_attrparam_t list)
@@ -556,6 +574,20 @@ let get_chk_pre_conditions
          end)
        (get_output_format_string_precondition fparams 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:restricted_output_format_string"
+             ~msg:name
+             __FILE__ __LINE__
+             [String.concat ", " e];
+           []
+         end)
+       (get_restricted_output_format_string_precondition fparams tagparams argparams)
+
   | (ACons ("trusted_os_cmd_fmt_string", tagparams)) :: argparams ->
      TR.tfold
        ~ok:(fun xpre -> [xpre])

CodeHawk/CHB/bchlib/bCHBCAttributesUtil.ml

@@ -40,6 +40,15 @@ let get_format_archetype
          match attr with
          | Attr ("format", params) ->
             (match params with
+             | ACons ("printf", []) :: AInt fmtrefindex :: AInt _ :: rest
+               when List.for_all (function AStr _ -> true | _ -> false) rest
+                    && rest <> [] ->
+                if index = fmtrefindex then
+                  let specs =
+                    List.map (function AStr s -> s | _ -> assert false) rest in
+                  Some (BCHLibTypes.RestrictedPrintFormat specs)
+                else
+                  None
              | [ACons ("printf", []); AInt fmtrefindex; AInt _]
                | [ACons ("printf", []); AInt fmtrefindex] ->
                 if index = fmtrefindex then

CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml

@@ -30,6 +30,7 @@
 open CHNumerical
 
 (* chutil *)
+open CHFormatStringParser
 open CHLogger
 open CHPrettyUtil
 
@@ -59,6 +60,27 @@ let log_error (tag: string) (msg: string): tracelogspec_t =
   mk_tracelog_spec ~tag:("callsemanticsrecorder:" ^ tag) msg
 
 
+let specifier_of_conversion (c: conversion_t): string =
+  match c with
+  | StringConverter -> "s"
+  | IntConverter | DecimalConverter -> "d"
+  | UnsignedDecimalConverter -> "u"
+  | UnsignedOctalConverter -> "o"
+  | UnsignedHexConverter false -> "x"
+  | UnsignedHexConverter true -> "X"
+  | FixedDoubleConverter false -> "f"
+  | FixedDoubleConverter true -> "F"
+  | ExpDoubleConverter false -> "e"
+  | ExpDoubleConverter true -> "E"
+  | FlexDoubleConverter false -> "g"
+  | FlexDoubleConverter true -> "G"
+  | HexDoubleConverter false -> "a"
+  | HexDoubleConverter true -> "A"
+  | UnsignedCharConverter -> "c"
+  | PointerConverter -> "p"
+  | OutputArgument -> "n"
+
+
 class call_semantics_recorder_t
         (loc: location_int)
         (finfo: function_info_int)
@@ -153,6 +175,32 @@ object (self)
            else
              Open
         | _ -> Open)
+    | XPORestrictedOutputFormatString (x, sl) ->
+       (match x with
+        | XConst (IntConst n) ->
+           let dw = numerical_mod_to_doubleword n in
+           if string_table#has_string dw then
+             let s = string_table#get_string dw in
+             let fmtspec = CHFormatStringParser.parse_formatstring s false in
+             let actual =
+               List.map
+                 (fun a -> specifier_of_conversion a#get_conversion)
+                 fmtspec#get_arguments in
+             if actual = sl then
+               Discharged (
+                   "format specifiers ["
+                   ^ (String.concat "," sl)
+                   ^ "] match: " ^ s)
+             else
+               Violated (
+                   "format specifiers ["
+                   ^ (String.concat "," actual)
+                   ^ "] do not match required ["
+                   ^ (String.concat "," sl)
+                   ^ "]: " ^ s)
+           else
+             Open
+        | _ -> Open)
     | XPOAllocationBase x ->
        (match x with
         | XVar v when self#finfo#env#is_return_value v ->

CodeHawk/CHB/bchlib/bCHExternalPredicate.ml

@@ -157,6 +157,10 @@ let rec xxpredicate_compare (p1: xxpredicate_t) (p2: xxpredicate_t): int =
   | (XXOutputFormatString t1, XXOutputFormatString t2) -> btc t1 t2
   | (XXOutputFormatString _, _) -> -1
   | (_, XXOutputFormatString _) -> 1
+  | (XXRestrictedOutputFormatString (t1, sl1), XXRestrictedOutputFormatString (t2, sl2)) ->
+     let l0 = btc t1 t2 in if l0 = 0 then Stdlib.compare sl1 sl2 else l0
+  | (XXRestrictedOutputFormatString _, _) -> -1
+  | (_, XXRestrictedOutputFormatString _) -> 1
   | (XXPositive t1, XXPositive t2) -> btc t1 t2
   | (XXPositive _, _) -> -1
   | (_, XXPositive _) -> 1
@@ -242,6 +246,7 @@ let rec xxpredicate_terms (p: xxpredicate_t): bterm_t list =
   | XXNonNegative t -> [t]
   | XXNullTerminated t -> [t]
   | XXOutputFormatString t -> [t]
+  | XXRestrictedOutputFormatString (t, _) -> [t]
   | XXPositive t -> [t]
   | XXRelationalExpr (_, t1, t2) -> [t1; t2]
   | XXStartsThread (t, tt) -> t :: tt
@@ -392,6 +397,13 @@ let rec xxpredicate_to_pretty (p: xxpredicate_t) =
   | XXNonNegative t -> default "non-negative" [t]
   | XXNullTerminated t -> default "null-terminated" [t]
   | XXOutputFormatString t -> default "output-format-string" [t]
+  | XXRestrictedOutputFormatString (t, sl) ->
+     LBLOCK [
+         STR "output-format-string-restricted(";
+         btp t;
+         STR ", [";
+         STR (String.concat "," sl);
+         STR "])"]
   | XXPositive t -> default "positive" [t]
   | XXRelationalExpr (op, t1, t2) ->
      LBLOCK [btp t1; STR (relational_op_to_string op); btp t2]
@@ -465,6 +477,7 @@ let rec modify_types_xxp
   | XXPositive t -> XXPositive (mbt t)
   | XXNullTerminated t -> XXNullTerminated (mbt t)
   | XXOutputFormatString t -> XXOutputFormatString (mbt t)
+  | XXRestrictedOutputFormatString (t, sl) -> XXRestrictedOutputFormatString (mbt t, sl)
   | XXRelationalExpr (op, t1, t2) -> XXRelationalExpr (op, mbt t1, mbt t2)
   | XXStartsThread (t, tt) -> XXStartsThread (mbt t, List.map mbt tt)
   | XXTainted t -> XXTainted (mbt t)

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -767,14 +767,80 @@ object (self)
                None)
            None
            (numerical_to_doubleword n)
-      | _ ->
+      | Some (XVar v) when self#f#env#is_initial_register_value v ->
+         let bterm_o =
+           (new arm_expression_externalizer_t self#f)#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:("update-arm-varargs:restricted format specifiers "
+                           ^ "from enclosing function")
+                     ~msg:self#cia
+                     __FILE__ __LINE__
+                     ["using restricted format specifiers: " ^ fmtstring] in
+                 let fmtspec = parse_formatstring fmtstring false in
+                 if fmtspec#has_arguments then
+                   let fmtargs = fmtspec#get_arguments in
+                   let newfintf = add_format_spec_parameters fintf false fmtargs in
+                   Some (newfintf, sem)
+                 else
+                   None
+              | _ ->
+                 let _ =
+                   log_diagnostics_result
+                     ~tag:"update_arm_varargs:no format arg info available"
+                     ~msg:self#cia
+                     __FILE__ __LINE__
+                     ["argxpr: " ^ (x2s (XVar v))] in
+                 None)
+          | _ ->
+             let _ =
+               log_diagnostics_result
+                 ~tag:"update_arm_varargs:unable to externalize argument"
+                 ~msg:self#cia
+                 __FILE__ __LINE__
+                 ["argxpr: " ^ (x2s (XVar v))] in
+             None)
+      | Some argxpr ->
          let _ =
            log_diagnostics_result
-             ~tag:"update-arm-varargs"
+             ~tag:"update_arm_varargs"
              ~msg:self#cia
              __FILE__ __LINE__
-             ["format string address is not a constant"] in
+             ["argxpr: " ^ (x2s argxpr)] in
          None
+      | _ ->
+         (match lastpar.apar_fmt with
+          | RestrictedPrintFormat sl when sl <> [] ->
+             let fmtstring =
+               String.concat " " (List.map (fun s -> "%" ^ s) sl) in
+             let _ =
+               log_diagnostics_result
+                 ~tag:"update-arm-varargs"
+                 ~msg:self#cia
+                 __FILE__ __LINE__
+                 ["using restricted format specifiers: " ^ fmtstring] in
+             let fmtspec = parse_formatstring fmtstring false in
+             if fmtspec#has_arguments then
+               let fmtargs = fmtspec#get_arguments in
+               let newfintf = add_format_spec_parameters fintf false fmtargs in
+               Some (newfintf, sem)
+             else
+               None
+          | _ ->
+             let _ =
+               log_diagnostics_result
+                 ~tag:"update-arm-varargs"
+                 ~msg:self#cia
+                 __FILE__ __LINE__
+                 ["format string address is not a constant"] in
+             None)
 
   method private update_mips_varargs
         (fintf: function_interface_t)
@@ -861,13 +927,31 @@ object (self)
            None
            (numerical_to_doubleword n)
       | _ ->
-         let _ =
-           log_diagnostics_result
-             ~tag:"update-mips-varargs"
-             ~msg:self#cia
-             __FILE__ __LINE__
-             ["format string address is not a constant"] in
-         None
+         (match lastpar.apar_fmt with
+          | RestrictedPrintFormat sl when sl <> [] ->
+             let fmtstring =
+               String.concat " " (List.map (fun s -> "%" ^ s) sl) in
+             let _ =
+               log_diagnostics_result
+                 ~tag:"update-mips-varargs"
+                 ~msg:self#cia
+                 __FILE__ __LINE__
+                 ["using restricted format specifiers: " ^ fmtstring] in
+             let fmtspec = parse_formatstring fmtstring false in
+             if fmtspec#has_arguments then
+               let fmtargs = fmtspec#get_arguments in
+               let newfintf = add_format_spec_parameters fintf false fmtargs in
+               Some (newfintf, sem)
+             else
+               None
+          | _ ->
+             let _ =
+               log_diagnostics_result
+                 ~tag:"update-mips-varargs"
+                 ~msg:self#cia
+                 __FILE__ __LINE__
+                 ["format string address is not a constant"] in
+             None)
 
   method private update_varargs
         (fintf: function_interface_t)

CodeHawk/CHB/bchlib/bCHFtsParameter.ml

@@ -91,6 +91,7 @@ let formatstring_type_to_string (t:formatstring_type_t) =
   | NoFormat -> "no"
   | PrintFormat -> "print"
   | ScanFormat -> "scan"
+  | RestrictedPrintFormat sl -> "print(" ^ (String.concat "," sl) ^ ")"
 
 
 let pld_position_to_string (p: pld_position_t) =
@@ -273,7 +274,11 @@ let read_xml_formatstring_type (s:string): formatstring_type_t traceresult =
   | "no" -> Ok NoFormat
   | "print" -> Ok PrintFormat
   | "scan" -> Ok ScanFormat
-  | _ -> Error ["Formatstring type: " ^ s ^ " not recognized"]
+  | _ ->
+     Error [
+         "Formatstring type: "
+         ^ s
+         ^ " not recognized (note: RestrictedPrintFormat is not supported in xml)"]
 
 
 let read_xml_roles (node:xml_element_int) =