diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml index 592b7065..6751f135 100644 --- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml +++ b/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]) diff --git a/CodeHawk/CHB/bchlib/bCHBCAttributesUtil.ml b/CodeHawk/CHB/bchlib/bCHBCAttributesUtil.ml index cff55f8f..bf7b83e4 100644 --- a/CodeHawk/CHB/bchlib/bCHBCAttributesUtil.ml +++ b/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 diff --git a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml index 1c9269d2..ca140f4d 100644 --- a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml +++ b/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 -> diff --git a/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml b/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml index 1f4820d8..6c09f12c 100644 --- a/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml +++ b/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) diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index c51944dc..9c7902f4 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/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) diff --git a/CodeHawk/CHB/bchlib/bCHFtsParameter.ml b/CodeHawk/CHB/bchlib/bCHFtsParameter.ml index 2dd2a8a7..7060ad88 100644 --- a/CodeHawk/CHB/bchlib/bCHFtsParameter.ml +++ b/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) = diff --git a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml index 0bfeffdd..5dfa668d 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml @@ -29,6 +29,7 @@ open CHLanguage (* chutil *) +open CHFormatStringParser open CHLogger (* xprlib *) @@ -507,6 +508,96 @@ let discharge_output_format_string status +(* ------------------------------------------------------------------------- + XPORestrictedOutputFormatString + ------------------------------------------------------------------------- *) + +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" + + +let restricted_output_format_string_constant_string_stmt + (loc: location_int) (x: xpr_t) (sl: string list): po_status_t = + match get_constant_string loc x with + | Some s -> + let fmtspec = 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) + | _ -> Open + + +let restricted_output_format_string_delegate + (finfo: function_info_int) + (loc: location_int) + (x: xpr_t) + (sl: string list): po_status_t = + match x with + | XVar v when finfo#env#is_initial_register_value v -> + TR.tfold + ~ok:(fun reg -> + let _ = + finfo#add_register_parameter_location reg BCHBCTypeUtil.t_charptr 4 in + let ftspar = finfo#get_summary#get_parameter_for_register reg in + let dst = ArgValue ftspar in + let xpred = XXRestrictedOutputFormatString (dst, sl) in + let _ = finfo#add_precondition xpred in + Delegated xpred) + ~error:(fun e -> + begin + log_error_result + ~tag:"discharge_restricted_output_format_string" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["v: " ^ (p2s v#toPretty); String.concat ", " e]; + Open + end) + (finfo#env#get_initial_register_value_register v) + | _ -> + Open + + +let discharge_restricted_output_format_string + (finfo: function_info_int) + (loc: location_int) + (x: xpr_t) + (sl: string list): po_status_t = + let status = restricted_output_format_string_constant_string_stmt loc x sl in + match status with + | Open -> restricted_output_format_string_delegate finfo loc x sl + | _ -> status + + (* ------------------------------------------------------------------------- XPOBuffer / XPOBlockWrite (stack size check) ------------------------------------------------------------------------- *) @@ -1063,6 +1154,9 @@ let discharge_one | XPOOutputFormatString x -> discharge_output_format_string finfo po#loc x + | XPORestrictedOutputFormatString (x, sl) -> + discharge_restricted_output_format_string finfo po#loc x sl + | XPOBlockWrite (ty, x, bwlen) -> discharge_blockwrite finfo po#loc ty x bwlen diff --git a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml index 7e4e40fc..5106a003 100644 --- a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml @@ -69,6 +69,7 @@ let raise_tag_error (name:string) (tag:string) (accepted:string list) = class interface_dictionary_t:interface_dictionary_int = object (self) + val formatstring_type_table = mk_index_table "formatstring-type-table" val pld_position_table = mk_index_table "pld-position-table" val pld_position_list_table = mk_index_table "pld-position-table-list" val parameter_location_detail_table = @@ -102,6 +103,7 @@ object (self) initializer tables <- [ + formatstring_type_table; pld_position_table; pld_position_list_table; parameter_location_detail_table; @@ -134,6 +136,25 @@ object (self) List.iter (fun t -> t#reset) tables end + method index_formatstring_type (f: formatstring_type_t) = + let tags = [formatstring_type_mcts#ts f] in + let key = + match f with + | NoFormat | PrintFormat | ScanFormat -> (tags, []) + | RestrictedPrintFormat sl -> (tags @ sl, []) in + formatstring_type_table#add key + + method get_formatstring_type (index: int): formatstring_type_t = + let name = "formatstring_type" in + let (tags, _) = formatstring_type_table#retrieve index in + let t = t name tags in + match (t 0) with + | "n" -> NoFormat + | "p" -> PrintFormat + | "s" -> ScanFormat + | "rp" -> RestrictedPrintFormat (List.tl tags) + | s -> raise_tag_error name s formatstring_type_mcts#tags + method index_pld_position (p: pld_position_t) = let tags = [pld_position_mcts#ts p] in let key = @@ -266,9 +287,7 @@ object (self) method index_fts_parameter (p:fts_parameter_t) = let iopt (i: int option) = match i with Some i -> i | _ -> (-1) in - let tags = [ - arg_io_mfts#ts p.apar_io; - formatstring_type_mfts#ts p.apar_fmt] in + let tags = [arg_io_mfts#ts p.apar_io] in let args = [ iopt p.apar_index; bd#index_string p.apar_name; @@ -277,7 +296,8 @@ object (self) self#index_roles p.apar_roles; p.apar_size; self#index_parameter_location_list p.apar_location; - self#index_parameter_destination_list p.apar_destinations + self#index_parameter_destination_list p.apar_destinations; + self#index_formatstring_type p.apar_fmt; ] in fts_parameter_table#add (tags, args) @@ -292,7 +312,7 @@ object (self) apar_desc = bd#get_string (a 3); apar_roles = self#get_roles (a 4); apar_io = arg_io_mfts#fs (t 0); - apar_fmt = formatstring_type_mfts#fs (t 1); + apar_fmt = self#get_formatstring_type (a 8); apar_size = a 5; apar_location = self#get_parameter_location_list (a 6); apar_destinations = self#get_parameter_destination_list (a 7) @@ -541,6 +561,8 @@ object (self) | XXNonNegative t -> (tags, [it t]) | XXNullTerminated t -> (tags, [it t]) | XXOutputFormatString t -> (tags, [it t]) + | XXRestrictedOutputFormatString (t, sl) -> + (tags, (it t) :: (List.map bd#index_string sl)) | XXPositive t -> (tags, [it t]) | XXRelationalExpr (op, t1, t2) -> (tags @ [relational_op_mfts#ts op], [it t1; it t2]) @@ -602,6 +624,8 @@ object (self) | "nng" -> XXNonNegative (gt (a 0)) | "nt" -> XXNullTerminated (gt (a 0)) | "ofs" -> XXOutputFormatString (gt (a 0)) + | "rofs" -> + XXRestrictedOutputFormatString (gt (a 0), List.map bd#get_string (List.tl args)) | "pos" -> XXPositive (gt (a 0)) | "x" -> XXRelationalExpr (relational_op_mfts#fs (t 1), gt (a 0), gt (a 1)) | "st" -> XXStartsThread (gt (a 0), List.map gt (List.tl args)) diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 1320314c..14241959 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -2127,6 +2127,7 @@ type formatstring_type_t = | NoFormat | PrintFormat | ScanFormat + | RestrictedPrintFormat of string list (** Function type signature parameter. @@ -2411,6 +2412,9 @@ type xxpredicate_t = | XXNullTerminated of bterm_t (** term points to null-terminated string *) | XXOutputFormatString of bterm_t (** term points to format string for output (e.g., sprintf) *) + | XXRestrictedOutputFormatString of bterm_t * string list + (** term points to a restricted output format string; the string list gives + the allowed format specifiers in order (e.g., ["s";"s";"s";"s"]) *) | XXRelationalExpr of relational_op_t * bterm_t * bterm_t (** relational expression *) @@ -2650,6 +2654,7 @@ type xpo_predicate_t = | XPOPositive of xpr_t | XPONullTerminated of xpr_t | XPOOutputFormatString of xpr_t + | XPORestrictedOutputFormatString of xpr_t * string list | XPORelationalExpr of relational_op_t * xpr_t * xpr_t | XPOStartsThread of xpr_t * xpr_t list | XPOTainted of xpr_t @@ -2793,6 +2798,9 @@ class type interface_dictionary_int = (** {1 Parameter location}*) + method index_formatstring_type: formatstring_type_t -> int + method get_formatstring_type: int -> formatstring_type_t + method index_pld_position: pld_position_t -> int method get_pld_position: int -> pld_position_t diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml index 58a398aa..45eedab3 100644 --- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml +++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml @@ -80,11 +80,12 @@ let arg_io_mfts: arg_io_t mfts_int = mk_mfts "arg_io_t" [ (ArgRead, "r"); (ArgReadWrite, "rw"); (ArgWrite, "w") ] +(* let formatstring_type_mfts: formatstring_type_t mfts_int = mk_mfts "formatstring_type_t" [ (NoFormat, "n"); (PrintFormat, "p"); (ScanFormat, "s") ] - + *) let eflag_mfts: eflag_t mfts_int = mk_mfts @@ -252,6 +253,27 @@ end let register_mcts: register_t mfts_int = new register_mcts_t + +class formatstring_type_mcts_t: [formatstring_type_t] mfts_int = + object + + inherit [formatstring_type_t] mcts_t "formatstring_type" + + method !ts (f: formatstring_type_t) = + match f with + | ScanFormat -> "s" + | PrintFormat -> "p" + | NoFormat -> "n" + | RestrictedPrintFormat _ -> "rp" + + method !tags = ["n"; "p"; "rp"; "s"] + + end + +let formatstring_type_mcts: formatstring_type_t mfts_int = +new formatstring_type_mcts_t + + class pld_position_mcts_t: [pld_position_t] mfts_int = object @@ -450,6 +472,7 @@ object | XXPositive _ -> "pos" | XXNullTerminated _ -> "nt" | XXOutputFormatString _ -> "ofs" + | XXRestrictedOutputFormatString _ -> "rofs" | XXRelationalExpr _ -> "x" | XXStartsThread _ -> "st" | XXTainted _ -> "t" @@ -465,7 +488,7 @@ object method !tags = [ "ab"; "b"; "bw"; "con"; "dis"; "e"; "fp"; "fr"; "ga"; "ha"; "i"; "ifs"; "inc"; "inv"; "ir"; "m"; - "nm"; "nn"; "nng"; "no"; "nt"; "nu"; "nz"; "ofs"; + "nm"; "nn"; "nng"; "no"; "nt"; "nu"; "nz"; "ofs"; "rofs"; "pos"; "sa"; "st"; "t"; "tc"; "tfa"; "tfs"; "ts"; "v"; "wfs"; "x" ] @@ -505,6 +528,7 @@ object | XPOPositive _ -> "pos" | XPONullTerminated _ -> "nt" | XPOOutputFormatString _ -> "ofs" + | XPORestrictedOutputFormatString _ -> "rofs" | XPORelationalExpr _ -> "x" | XPOStartsThread _ -> "st" | XPOTainted _ -> "t" @@ -520,7 +544,7 @@ object method !tags = [ "ab"; "b"; "bw"; "con"; "dis"; "e"; "fp"; "fr"; "ga"; "ha"; "i"; "ifs"; "inc"; "inv"; "ir"; "m"; - "nm"; "nn"; "nng"; "no"; "nt"; "nu"; "nz"; "ofs"; + "nm"; "nn"; "nng"; "no"; "nt"; "nu"; "nz"; "ofs"; "rofs"; "pos"; "sa"; "st"; "t"; "tc"; "tfa"; "tfs"; "ts"; "v"; "wfs"; "x" ] diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli index 670d7f08..ddf42b81 100644 --- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli +++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli @@ -41,7 +41,7 @@ val quote_status_mfts: quote_status_t mfts_int val format_args_kind_mfts: format_args_kind_t mfts_int val arg_io_mfts: arg_io_t mfts_int -val formatstring_type_mfts: formatstring_type_t mfts_int +(* val formatstring_type_mfts: formatstring_type_t mfts_int *) (** {1 Architecture-related} *) @@ -75,6 +75,8 @@ val register_mcts: register_t mfts_int (** {1 Interface types} *) +val formatstring_type_mcts: formatstring_type_t mfts_int + val parameter_destination_mcts: parameter_destination_t mfts_int val pld_position_mcts: pld_position_t mfts_int val parameter_location_mcts: parameter_location_t mfts_int diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index ff5e0060..42057930 100644 --- a/CodeHawk/CHB/bchlib/bCHVersion.ml +++ b/CodeHawk/CHB/bchlib/bCHVersion.ml @@ -95,8 +95,8 @@ end let version = new version_info_t - ~version:"0.6.0_20260611" - ~date:"2026-06-11" + ~version:"0.6.0_20260614" + ~date:"2026-06-14" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlib/bCHXPODictionary.ml b/CodeHawk/CHB/bchlib/bCHXPODictionary.ml index 94149ec7..fce49b1d 100644 --- a/CodeHawk/CHB/bchlib/bCHXPODictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHXPODictionary.ml @@ -120,6 +120,8 @@ object (self) | XPOPositive x -> (tags, [ix x]) | XPONullTerminated x -> (tags, [ix x]) | XPOOutputFormatString x -> (tags, [ix x]) + | XPORestrictedOutputFormatString (x, sl) -> + (tags, (ix x) :: (List.map bd#index_string sl)) | XPORelationalExpr (op, x1, x2) -> (tags @ [relational_op_mfts#ts op], [ix x1; ix x2]) | XPOStartsThread (x, xl) -> (tags, (ix x) :: (List.map ix xl)) diff --git a/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml b/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml index 23df214f..e1e5b1d3 100644 --- a/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml +++ b/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml @@ -89,6 +89,7 @@ let rec xxp_to_xpo_predicate | XXPositive t -> XPOPositive (btx t) | XXNullTerminated t -> XPONullTerminated (btx t) | XXOutputFormatString t -> XPOOutputFormatString (btx t) + | XXRestrictedOutputFormatString (t, sl) -> XPORestrictedOutputFormatString (btx t, sl) | XXRelationalExpr (op, t1, t2) -> XPORelationalExpr (op, btx t1, btx t2) | XXStartsThread (t1, t2) -> XPOStartsThread (btx t1, List.map btx t2) | XXTainted t -> XPOTainted (btx t) @@ -169,6 +170,13 @@ let rec xpo_predicate_to_pretty (p: xpo_predicate_t) = | XPONonNegative t -> default "non-negative" [t] | XPONullTerminated t -> default "null-terminated" [t] | XPOOutputFormatString t -> default "output-format-string" [t] + | XPORestrictedOutputFormatString (t, sl) -> + LBLOCK [ + STR "output-format-string-restricted("; + x2p t; + STR ", ["; + STR (String.concat "," sl); + STR "])"] | XPOPositive t -> default "positive" [t] | XPORelationalExpr (op, t1, t2) -> LBLOCK [x2p t1; STR (relational_op_to_string op); x2p t2]