diff --git a/CodeHawk/CH/xprlib/xprUtil.ml b/CodeHawk/CH/xprlib/xprUtil.ml index fe1ba310..7e34b143 100644 --- a/CodeHawk/CH/xprlib/xprUtil.ml +++ b/CodeHawk/CH/xprlib/xprUtil.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2022 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 @@ -31,6 +31,7 @@ open CHCommon open CHLanguage open CHNumerical +open CHNumericalConstraints open CHPEPRTypes open CHPretty @@ -307,6 +308,37 @@ let xpr_to_boolexpr (nested_cmd_2_cmds c, e) +let xpr_to_numconstraint (x: xpr_t): numerical_constraint_t option = + match x with + | XOp (XEq, [XVar v1; XVar v2]) -> + let f1 = (numerical_one, new numerical_factor_t v1) in + let f2 = (numerical_one#neg, new numerical_factor_t v2) in + Some (new numerical_constraint_t + ~factors:[f1; f2] ~constant:numerical_zero ~kind:LINEAR_EQ) + | XOp (XEq, [XVar v1; XConst (IntConst constant)]) -> + let f1 = (numerical_one, new numerical_factor_t v1) in + Some (new numerical_constraint_t ~factors:[f1] ~constant ~kind:LINEAR_EQ) + | _ -> None + + +let numconstraint_to_xpr (c: numerical_constraint_t): xpr_t = + let factors = c#getFactors in + let constant = c#getConstant in + let lhs = + List.fold_left (fun acc f -> + let coeff = c#getCoefficient f in + if coeff#equal numerical_one then + XOp (XPlus, [acc; XVar f#getVariable]) + else if coeff#equal numerical_one#neg then + XOp (XMinus, [acc; XVar f#getVariable]) + else + XOp (XPlus, [acc; + XOp (XMult, [XConst (IntConst coeff); XVar f#getVariable])])) + (XConst (IntConst numerical_zero)) factors in + match c#getKind with + | LINEAR_EQ -> XOp (XEq, [lhs; num_constant_expr constant]) + | LINEAR_INEQ -> XOp (XLe, [lhs; num_constant_expr constant]) + (* =============================================================================== SUBSTITUTION diff --git a/CodeHawk/CH/xprlib/xprUtil.mli b/CodeHawk/CH/xprlib/xprUtil.mli index 573221d7..f2186179 100644 --- a/CodeHawk/CH/xprlib/xprUtil.mli +++ b/CodeHawk/CH/xprlib/xprUtil.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2022 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 @@ -29,6 +29,7 @@ (* chlib *) open CHLanguage +open CHNumericalConstraints open CHPEPRTypes (* chutil *) @@ -55,3 +56,6 @@ val get_pepr_range_xprs: pepr_params_int -> pepr_range_int -> pepr_xpr_extract val get_pepr_dependency_xprs: pepr_params_int -> param_constraint_set_int -> xpr_t list + +val xpr_to_numconstraint: xpr_t -> numerical_constraint_t option +val numconstraint_to_xpr: numerical_constraint_t -> xpr_t diff --git a/CodeHawk/CH/xprlib/xprt.ml b/CodeHawk/CH/xprlib/xprt.ml index a6886d20..97457bdc 100644 --- a/CodeHawk/CH/xprlib/xprt.ml +++ b/CodeHawk/CH/xprlib/xprt.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 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 @@ -137,6 +137,16 @@ let is_intconst (x: xpr_t) = | XConst (IntConst _ ) -> true | _ -> false +let is_equality (x: xpr_t) = + match x with + | XOp (XEq, _) -> true + | _ -> false + +let is_inequality (x: xpr_t) = + match x with + | XOp ((XGe | XGt | XLe | XLt), _) -> true + | _ -> false + let is_conjunction (x: xpr_t) = match x with | XOp (XLAnd, _) -> true diff --git a/CodeHawk/CH/xprlib/xprt.mli b/CodeHawk/CH/xprlib/xprt.mli index 83a93941..c2d964b7 100644 --- a/CodeHawk/CH/xprlib/xprt.mli +++ b/CodeHawk/CH/xprlib/xprt.mli @@ -1,4 +1,4 @@ -(* ============================================================================= + (* ============================================================================= CodeHawk Analyzer Infrastructure Utilities Author: Henny Sipma ------------------------------------------------------------------------------ @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 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 @@ -62,6 +62,9 @@ val is_random: xpr_t -> bool val is_true: xpr_t -> bool val is_false: xpr_t -> bool +val is_equality: xpr_t -> bool +val is_inequality: xpr_t -> bool + val is_conjunction: xpr_t -> bool val is_disjunction: xpr_t -> bool diff --git a/CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli b/CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli index 8e4ac02d..ba88b1cd 100644 --- a/CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli +++ b/CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2023 Henny B. Sipma - Copyright (c) 2024 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 @@ -112,11 +112,25 @@ object method mk_call_var: string -> int -> variable_t method mk_call_vars: variable_t - method mk_base_address_value: variable_t -> offset -> typ -> variable_t + (** [mk_base_address_memory_variable_init basevar offset type vt] returns a + memory variable with base address held in (constant-value) variable + [basevar], offset [offset], type [type], and chif-var type [vt], + together with a symbolic initial value for that variable. + *) + method mk_base_address_memory_variable_init: + variable_t -> offset -> typ -> variable_type_t -> (variable_t * variable_t) + + (** [mk_base_address_memory_variable_init basevar offset type vt] returns a + memory variable with base address held in (constant-value) variable + [basevar], offset [offset], type [type], and chif-var type [vt] + *) + method mk_base_address_memory_variable: + variable_t -> offset -> typ -> variable_type_t -> variable_t method mk_global_address_value: varinfo -> offset -> typ -> variable_t method mk_stack_address_value: varinfo -> offset -> typ -> variable_t method mk_memory_address_value: int -> offset -> variable_t method mk_string_address: string -> offset -> typ -> variable_t + method mk_initial_value: variable_t -> typ -> variable_type_t -> variable_t method mk_function_return_value: location @@ -157,7 +171,14 @@ object -> offset -> typ -> variable_type_t - -> (variable_t * variable_t * variable_t * variable_t) + -> (variable_t * variable_t) + + method mk_array_par_deref: + varinfo + -> typ + -> int + -> variable_type_t + -> (variable_t * variable_t) list method mk_struct_par_deref: varinfo @@ -207,9 +228,6 @@ object method get_declared_type_value_range: variable_t -> numerical_t option * numerical_t option - method get_external_addresses: variable_t list - method get_symbolic_dereferences: variable_t list - method get_parameter_exp: variable_t -> exp method get_global_exp: variable_t -> exp method get_callvar_callee: variable_t -> varinfo @@ -223,10 +241,14 @@ object method get_tainted_value_bounds: variable_t -> xpr_t option * xpr_t option method get_byte_sequence_origin: variable_t -> variable_t method get_memory_reference : variable_t -> memory_reference_int + method get_string_literal_address_string: variable_t -> string method get_region_name: int -> string (* memory region index *) method get_indicator: variable_t -> int (* augmentation variable *) + method get_initial_parameter_vinfo: variable_t -> varinfo * offset + method get_memory_address_wrapped_value: variable_t -> variable_t option + (** {1 Predicates} *) method is_augmentation_variable: variable_t -> bool @@ -236,7 +258,10 @@ object method is_global_variable: variable_t -> bool method is_fixed_value: variable_t -> bool method is_memory_variable: variable_t -> bool + method is_string_literal_address: variable_t -> bool method is_memory_address: variable_t -> bool + method is_mut_memory_address: variable_t -> bool + method is_ref_memory_address: variable_t -> bool method is_fixed_xpr: xpr_t -> bool method is_initial_value: variable_t -> bool method is_initial_parameter_value: variable_t -> bool @@ -572,32 +597,6 @@ class type po_query_int = (** {1 Checks} *) - (** {2 Command-line argument check} *) - - (** [check_command_line_argument exp safemsg vmsg dmsg] checks if [exp] is a - command-line argument, and if so, checks whether its index is less than - the argument count. If less the PO is set to safe, if greater than or - equal the PO is set to violation, and if no argument count is found, a - diagnostic message is set according to [dmsg].*) - method check_command_line_argument: - exp - -> (int -> int -> string) - -> (int -> int -> string) - -> (int -> string) - -> bool - - (** Returns the index of the supporting invariant fact and the - command-line argument count if this function is main and an invariant - fact is available with that information. Otherwise returns None.*) - method get_command_line_argument_count: (int * int) option - - (** [get_command_line_argument_index exp] returns the (0-based) function - argument index if exp is a function argument. - - raise [CCHFailure] if [exp] is not a command-line argument.*) - method get_command_line_argument_index: exp -> int - - method check_implied_by_assumptions: po_predicate_t -> po_predicate_t option (** {1 Information} *) @@ -616,6 +615,15 @@ class type po_query_int = (** same as [get_invariants], but with the result sorted by upper bound.*) method get_invariants_ub: int -> invariant_int list + (** [get_var_invariants var] returns a list of invariants for variable [var] + at the same cfg context as the proof obligation. + + This may be useful if a derived variable is constructed from the results + of another invariants, but invariants for that variable are not tied to + the proof obligation. + *) + method get_var_invariants: variable_t -> invariant_int list + (** [get_pepr_bounds argindex] returns a list of invariants for the PO argument with argument index (1-based) [argindex] generated by the PEPR domain together with lower-bound and upper-bound expressions. *) @@ -847,7 +855,7 @@ class type po_query_int = method is_api_expression: xpr_t -> bool method is_global_expression: xpr_t -> bool method is_function_return: xpr_t -> bool - method is_command_line_argument: exp -> bool + method is_memory_base_address: variable_t -> string option (** {1 Printing} *) diff --git a/CodeHawk/CHC/cchanalyze/cCHAssignmentTranslator.ml b/CodeHawk/CHC/cchanalyze/cCHAssignmentTranslator.ml index 770e9fe9..70bd94a8 100644 --- a/CodeHawk/CHC/cchanalyze/cCHAssignmentTranslator.ml +++ b/CodeHawk/CHC/cchanalyze/cCHAssignmentTranslator.ml @@ -69,6 +69,13 @@ object (self) val mutable location = unknown_location method translate (ctxt:program_context_int) (loc:location) (lhs:lval) (rhs:exp) = + let _ = + log_diagnostics_result + ~tag:"translate" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["lhs: " ^ (p2s (lval_to_pretty lhs)); + "rhs: " ^ (p2s (exp_to_pretty rhs))] in let _ = context <- ctxt in let _ = location <- loc in if self#has_contract_instr loc.line lhs then diff --git a/CodeHawk/CHC/cchanalyze/cCHCallTranslator.ml b/CodeHawk/CHC/cchanalyze/cCHCallTranslator.ml index 530816da..786ed6d1 100644 --- a/CodeHawk/CHC/cchanalyze/cCHCallTranslator.ml +++ b/CodeHawk/CHC/cchanalyze/cCHCallTranslator.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020-2023 Henny B. Sipma - Copyright (c) 2024 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 @@ -480,10 +480,19 @@ object (self) | Some (c, r) -> (c, r) | _ -> match returntype with - | TPtr (t,_) -> - let basevar = env#mk_base_address_value returnvalue NoOffset t in - (make_c_cmd SKIP, NUM_VAR basevar) + | TPtr ((TInt _ | TFloat _ | TPtr _) as t, _) -> + (* create a placeholder memory variable for the dereferenced return value *) + let (rmemvar, rmemvarinit) = + env#mk_base_address_memory_variable_init returnvalue NoOffset t NUM_VAR_TYPE in + let cmd = make_c_cmd (ASSIGN_NUM (rmemvar, NUM_VAR rmemvarinit)) in + (cmd, NUM_VAR returnvalue) | _ -> + let _ = + log_diagnostics_result + ~tag:"get_arg_post_value" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["returntype: " ^ (p2s (typ_to_pretty returntype))] in (make_c_cmd SKIP, NUM_VAR returnvalue) method private get_post_assert @@ -824,8 +833,8 @@ object (self) postconditions fname fvid rvar fnargs in let domainop = match type_of_lval fdecls lval with - | TPtr (t,_) -> - let frVar = env#mk_base_address_value frVar NoOffset t in + | TPtr (_t,_) -> + (* let frVar = env#mk_base_address_value frVar NoOffset t in *) make_c_cmd (DOMAIN_OPERATION ( [valueset_domain], @@ -903,11 +912,20 @@ object (self) | Some (c, r) -> (c, r) | _ -> match returntype with - | TPtr (t, _) -> - let basevar = env#mk_base_address_value returnvalue NoOffset t in - (make_c_cmd SKIP, NUM_VAR basevar) + | TPtr ((TInt _ | TFloat _ | TPtr _) as t, _) -> + (* create a placeholder memory variable for the dereferenced return value *) + let (rmemvar, rmemvarinit) = + env#mk_base_address_memory_variable_init returnvalue NoOffset t NUM_VAR_TYPE in + let cmd = make_c_cmd (ASSIGN_NUM (rmemvar, NUM_VAR rmemvarinit)) in + (cmd, NUM_VAR returnvalue) | _ -> - (make_c_cmd SKIP, NUM_VAR returnvalue) + let _ = + log_diagnostics_result + ~tag:"get_arg_post_value" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["returntype: " ^ (p2s (typ_to_pretty returntype))] in + (make_c_cmd SKIP, NUM_VAR returnvalue) method private get_post_assert (postconditions: @@ -1243,6 +1261,13 @@ object (self) (fname:string) (args:exp list) (_fnargs:xpr_t list) = let (pcs, _epcs) = get_postconditions env#get_functionname (Some fname) context in + let _ = + log_diagnostics_result + ~tag:"sym:get_postconditions" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["pcs: " ^ + (String.concat ", " (List.map annotated_xpredicate_to_string pcs))] in List.concat (List.map (fun (pc, _) -> match pc with @@ -1316,6 +1341,13 @@ object (self) (fnargs:xpr_t list) = let vinfo = fdecls#get_varinfo_by_vid fvid in let sideeffects = get_sideeffects env#get_functionname (Some fname) context in + let _ = + log_diagnostics_result + ~tag:"get_sideeffect:sym" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["side effects: " ^ + (String.concat ", " (List.map annotated_xpredicate_to_string sideeffects))] in let (sitevars,xsitevars) = env#get_site_call_vars context in let fnzargs = List.map (fun _ -> None) fnargs in let zsevar = @@ -1490,9 +1522,25 @@ object (self) | CastE (_, Lval (Var (_vname,vid), offset)) -> let vinfo = env#get_varinfo vid in Some (env#mk_program_var vinfo offset SYM_VAR_TYPE) - | _ -> None + | _ -> + begin + log_diagnostics_result + ~tag:"get_sideeffect:sym:initialized-range" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["no base variable found for " ^ (p2s (s_term_to_pretty base))]; + None + end end - | _ -> None in + | _ -> + begin + log_diagnostics_result + ~tag:"get_sideeffect:sym:initialized-range" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["base term not recognized: " ^ (p2s (s_term_to_pretty base))]; + None + end in let lenvalue = match len with | ArgValue (ParFormal n, ArgNoOffset) -> diff --git a/CodeHawk/CHC/cchanalyze/cCHEnvironment.ml b/CodeHawk/CHC/cchanalyze/cCHEnvironment.ml index b653962f..a5fe6776 100755 --- a/CodeHawk/CHC/cchanalyze/cCHEnvironment.ml +++ b/CodeHawk/CHC/cchanalyze/cCHEnvironment.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2024 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 @@ -37,6 +37,7 @@ open CHOnlineCodeSet (* chutil *) open CHLogger +open CHTraceResult (* xprlib *) open XprTypes @@ -61,6 +62,13 @@ open CCHAnalysisTypes module EU = CCHEngineUtil module H = Hashtbl +module TR = CHTraceResult + + +let p2s = CHPrettyUtil.pretty_to_string + +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " module NumericalCollections = CHCollections.Make @@ -176,8 +184,27 @@ object(self) method get_return_contexts = return_contexts#toList method mk_memory_variable (memrefindex:int) (offset:offset) (vt:variable_type_t) = + (* For a memory variable NoOffset and IndexOffset 0 are semantically equivalent. + To ensure that only a single variable is created for the two different + representations, the IndexOffset 0 is chosen. + *) + let offset = + match offset with + | NoOffset -> mk_constant_index_offset numerical_zero + | _ -> offset in let cvar = vmgr#mk_memory_variable memrefindex offset in - self#add_chifvar cvar vt + let chifvar = self#add_chifvar cvar vt in + let _ = + log_diagnostics_result + ~tag:"mk_memory_variable" + ~msg:self#get_functionname + __FILE__ __LINE__ + ["memrefindex: " ^ (string_of_int memrefindex); + "offset: " ^ (p2s (offset_to_pretty offset)); + "vt: " ^ (p2s (variable_type_to_pretty vt)); + "cvar: " ^ (p2s cvar#toPretty); + "chifvar: " ^ (p2s chifvar#toPretty)] in + chifvar method mk_return_var (typ:typ) (vt:variable_type_t) = let cVar = vmgr#mk_return_variable typ in @@ -230,12 +257,58 @@ object(self) let cVar = vmgr#mk_local_variable vinfo NoOffset in let chifvar = self#add_chifvar cVar vt in let vInit = self#mk_initial_value chifvar vinfo.vtype vt in - let memref = vmgr#memrefmgr#mk_external_reference vInit vinfo.vtype in - let memvar = vmgr#mk_memory_variable memref#index offset in - let chifmemvar = self#add_chifvar memvar vt in - let chifmemaddr = self#mk_memory_address_value memref#index NoOffset in - let memvarinit = self#mk_initial_value chifmemvar ttyp vt in - (chifvar, chifmemaddr, chifmemvar, memvarinit) + let memref = self#mk_external_reference vInit ttyp in + let chifmemvar = self#mk_memory_variable memref#index offset vt in + let chifmemvarinit = self#mk_initial_value chifmemvar ttyp vt in + let _ = + log_diagnostics_result + ~tag:"mk_par_deref_init" + ~msg:self#get_functionname + __FILE__ __LINE__ + ["typ: " ^ (p2s (typ_to_pretty ttyp)); + "cVar: " ^ (p2s cVar#toPretty); + "chifvar: " ^ (p2s chifvar#toPretty); + "vInit: " ^ (p2s vInit#toPretty); + "memref: " ^ (p2s memref#toPretty) + ^ " (index: " ^ (string_of_int memref#index) ^ ")"; + "chifmemvar: " ^ (p2s chifmemvar#toPretty); + "chifmemvarinit: " ^ (p2s chifmemvarinit#toPretty)] in + (chifmemvar, chifmemvarinit) + + method mk_array_par_deref + (vinfo: varinfo) (ttyp: typ) (size: int) (vt: variable_type_t) = + let cVar = vmgr#mk_local_variable vinfo NoOffset in + let chifvar = self#add_chifvar cVar vt in + let vInit = self#mk_initial_value chifvar vinfo.vtype vt in + List.init size (fun i -> + let offset = mk_constant_index_offset (mkNumerical i) in + let nullattr = + if self#get_functionname = "main" then NotNull else CanBeNull in + let memref = vmgr#memrefmgr#mk_external_reference ~nullattr vInit ttyp in + let chifmemvar = self#mk_memory_variable memref#index offset vt in + let memvarInit = self#mk_initial_value chifmemvar ttyp vt in + let memvarInit = + match ttyp with + | TPtr (tgttype, _) -> + let refattr = + if self#get_functionname = "main" then MutableRef else RawPointer in + let memref = + vmgr#memrefmgr#mk_external_reference memvarInit tgttype in + let memaddr = vmgr#mk_memory_address ~refattr memref#index NoOffset in + self#add_chifvar memaddr vt + | _ -> + memvarInit in + let _ = + log_diagnostics_result + ~tag:"mk_array_par_deref" + ~msg:self#get_functionname + __FILE__ __LINE__ + ["typ: " ^ (p2s (typ_to_pretty ttyp)); + "vt: " ^ (p2s (variable_type_to_pretty vt)); + "memref: " ^ (p2s memref#toPretty) + ^ " (index: " ^ (string_of_int memref#index) ^ ")"; + "chifmemvar: " ^ (p2s chifmemvar#toPretty)] in + (chifmemvar, memvarInit)) method mk_struct_par_deref (vinfo:varinfo) (ttyp:typ) (ckey:int) (vt:variable_type_t) = @@ -249,10 +322,9 @@ object(self) let offset = Field (fuse,NoOffset) in let memref = vmgr#memrefmgr#mk_external_reference vInit vinfo.vtype in - let memvar = vmgr#mk_memory_variable memref#index offset in - let memvar = self#add_chifvar memvar vt in - let memvarInit = self#mk_initial_value memvar field.ftype vt in - (memvar,memvarInit)) cinfo.cfields + let chifmemvar = self#mk_memory_variable memref#index offset vt in + let memvarInit = self#mk_initial_value chifmemvar field.ftype vt in + (chifmemvar, memvarInit)) cinfo.cfields with | Invalid_argument s -> begin @@ -358,7 +430,7 @@ object(self) let callvars = H.fold (fun _ v acc -> v @ acc) callvariables [] in self#mk_fn_entry_call_var :: callvars - method private mk_initial_value (v:variable_t) (t:typ) (vt:variable_type_t) = + method mk_initial_value (v:variable_t) (t:typ) (vt:variable_type_t) = let aVal = vmgr#mk_initial_value v t in self#add_chifvar aVal vt @@ -383,10 +455,76 @@ object(self) let addrvar = vmgr#mk_memory_address memref#index offset in self#add_chifvar addrvar NUM_VAR_TYPE - method mk_base_address_value (v:variable_t) (offset:offset) (t:typ) = - let memref = vmgr#memrefmgr#mk_external_reference v t in - let addrvar = vmgr#mk_memory_address memref#index offset in - self#add_chifvar addrvar NUM_VAR_TYPE + method private get_basevar_attributes + (v: variable_t): (ref_attribute_t * null_attribute_t) traceresult = + if self#is_initial_parameter_value v then + let (vinfo, _offset) = self#get_initial_parameter_vinfo v in + let vtype = fenv#get_type_unrolled vinfo.vtype in + let typattrs = CCHTypesUtil.get_typ_attributes vtype in + let _ = + log_diagnostics_result + ~msg:self#get_functionname + ~tag:"get_basevar_attributes" + __FILE__ __LINE__ + ["vinfo.vname: " ^ vinfo.vname; + "vinfo.vtype: " ^ (p2s (typ_to_pretty vtype)); + "typ attrs: " ^ (String.concat " " (List.map attribute_to_string typattrs)); + "vinfo.vattr: " + ^ (String.concat " " (List.map attribute_to_string vinfo.vattr))] in + if has_const_attribute vtype || has_deref_const_attribute vtype then + Ok (ImmutableRef, CanBeNull) + else + Ok (RawPointer, CanBeNull) + else + Error [(elocm __LINE__); "v: " ^ (p2s v#toPretty); "Not yet implemented"] + + method private mk_external_reference (v: variable_t) (t: typ): memory_reference_int = + TR.tfold + ~ok:(fun (_refattr, nullattr) -> + vmgr#memrefmgr#mk_external_reference ~nullattr v t) + ~error: (fun e -> + begin + log_diagnostics_result + ~msg:self#get_functionname + ~tag:"mk_external_reference:attrs" + __FILE__ __LINE__ + (e @ ["v: " ^ (p2s v#toPretty)]); + vmgr#memrefmgr#mk_external_reference v t + end) + (self#get_basevar_attributes v) + + method mk_base_address_memory_variable_init + (v: variable_t) (offset:offset) (t:typ) (vt: variable_type_t) = + let memref = self#mk_external_reference v t in + let chifmemvar = self#mk_memory_variable memref#index offset vt in + let chifmemvarinit = self#mk_initial_value chifmemvar t vt in + let _ = + log_diagnostics_result + ~tag:"mk_base_address_variable_init" + ~msg:v#getName#getBaseName + __FILE__ __LINE__ + ["offset: " ^ (p2s (offset_to_pretty offset)); + "type: " ^ (p2s (typ_to_pretty t)); + "chifmemvar: " ^ (p2s chifmemvar#toPretty)] in + (chifmemvar, chifmemvarinit) + + method mk_base_address_memory_variable + (v: variable_t) (offset:offset) (t:typ) (vt: variable_type_t) = + let memref = self#mk_external_reference v t in + let chifmemvar = self#mk_memory_variable memref#index offset vt in + let _ = + log_diagnostics_result + ~tag:"mk_base_address_variable" + ~msg:self#get_functionname + __FILE__ __LINE__ + ["v: " ^ (p2s v#toPretty); + "offset: " ^ (p2s (offset_to_pretty offset)); + "type: " ^ (p2s (typ_to_pretty t)); + "vt: " ^ (p2s (variable_type_to_pretty vt)); + "memref: " ^ (p2s memref#toPretty) + ^ " (index: " ^ (string_of_int memref#index) ^ ")"; + "chifmemvar: " ^ (p2s chifmemvar#toPretty)] in + chifmemvar method mk_global_memory_variable (vinfo:varinfo) (offset:offset) (_t:typ) (vt:variable_type_t) = @@ -452,8 +590,22 @@ object(self) | t -> let cVar = vmgr#mk_local_variable vinfo NoOffset in let chifvar = self#add_chifvar cVar vt in - let vInit = self#mk_initial_value chifvar vinfo.vtype vt in - [(vinfo.vname,t,chifvar,vInit)] + let vInit = self#mk_initial_value chifvar t vt in + let vInit = + match t with + | TPtr (tgttype, _) -> + let nullattr = + if self#get_functionname = "main" then NotNull else CanBeNull in + let refattr = + if self#get_functionname = "main" then MutableRef else RawPointer in + let memref = + vmgr#memrefmgr#mk_external_reference ~nullattr vInit tgttype in + let memaddr = vmgr#mk_memory_address ~refattr memref#index NoOffset in + self#add_chifvar memaddr vt + | _ -> + vInit in + (* let chifvInit = self#add_chifvar vInit vt in *) + [(vinfo.vname, t, chifvar, vInit)] method register_formals (formals: varinfo list) (vt:variable_type_t) = List.concat (List.map (fun v -> self#register_formal v vt) formals) @@ -564,10 +716,6 @@ object(self) else None - method get_symbolic_dereferences = [] (* TBD, see ref:get_frozen_dereferences *) - - method get_external_addresses = [] (* TBD, see ref *) - (* memory region manager services ------------------------------------------- *) method get_region_name (index:int) = @@ -591,7 +739,7 @@ object(self) else if self#is_memory_variable v then let (memref,offset) = self#get_memory_variable v in match memref#get_base with - | CBaseVar v -> + | CBaseVar (v, _) -> let (vinfo,voffset) = vmgr#get_local_variable v#getName#getSeqNumber in "stack variable " @@ -621,7 +769,7 @@ object(self) (LBLOCK [ STR "global address region of non-global-variable: "; v#toPretty])) - | CBaseVar v -> "basevar " ^ v#getName#getBaseName + | CBaseVar (v, _) -> "basevar " ^ v#getName#getBaseName | CUninterpreted s -> "unknown:" ^ s in aux index @@ -698,6 +846,9 @@ object(self) method is_initial_parameter_value v = vmgr#is_initial_parameter_value (self#get_seqnr v) + method get_initial_parameter_vinfo (v:variable_t): varinfo * offset = + vmgr#get_initial_parameter_vinfo (self#get_seqnr v) + method is_initial_parameter_deref_value v = vmgr#is_initial_parameter_deref_value (self#get_seqnr v) @@ -727,6 +878,19 @@ object(self) method is_memory_address v = vmgr#is_memory_address (self#get_seqnr v) + method is_mut_memory_address v = vmgr#is_mut_memory_address (self#get_seqnr v) + + method is_ref_memory_address v = vmgr#is_ref_memory_address (self#get_seqnr v) + + method get_memory_address_wrapped_value v = + vmgr#get_memory_address_wrapped_value (self#get_seqnr v) + + method is_string_literal_address v = + vmgr#is_string_literal_address (self#get_seqnr v) + + method get_string_literal_address_string (v: variable_t) = + vmgr#get_string_literal_address_string (self#get_seqnr v) + method is_memory_variable v = vmgr#is_memory_variable (self#get_seqnr v) method check_variable_applies_to_po diff --git a/CodeHawk/CHC/cchanalyze/cCHExpTranslator.ml b/CodeHawk/CHC/cchanalyze/cCHExpTranslator.ml index e3d5d6d9..141fb1b0 100644 --- a/CodeHawk/CHC/cchanalyze/cCHExpTranslator.ml +++ b/CodeHawk/CHC/cchanalyze/cCHExpTranslator.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2023 Henny B. Sipma - 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 @@ -150,7 +150,13 @@ object (self) | Field (f, o) -> Field (f, self#externalize_offset o) | Index (e, o) -> Index (externalize_exp e, self#externalize_offset o) - method private translate_lval lval = + method private translate_lval (lval: lval): variable_t = + let _ = + log_diagnostics_result + ~tag:"translate_lval" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["lval: " ^ (p2s (lval_to_pretty lval))] in match lval with | (Var (_, vid),offset) when vid > 0 -> let vinfo = env#get_varinfo vid in @@ -162,20 +168,100 @@ object (self) env#mk_stack_memory_variable vinfo eoffset otype NUM_VAR_TYPE else env#mk_program_var vinfo eoffset NUM_VAR_TYPE - | (Var _, _) -> env#mk_temp NUM_VAR_TYPE + | (Var _, _) -> + let _ = + log_diagnostics_result + ~tag:"translate_lval:Var" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["lval: " ^ (p2s (lval_to_pretty lval))] in + env#mk_temp NUM_VAR_TYPE | (Mem e, offset) -> match self#translate_exp context e with | XVar v when env#is_memory_address v -> let (memref, moffset) = env#get_memory_address v in - env#mk_memory_variable - memref#index (add_offset moffset offset) NUM_VAR_TYPE - | XVar v when env#is_initial_value v -> - let memref = - env#get_variable_manager#memrefmgr#mk_external_reference - v (type_of_exp fdecls e) in - env#mk_memory_variable memref#index offset NUM_VAR_TYPE - | XVar _ -> env#mk_temp NUM_VAR_TYPE - | _ -> env#mk_temp NUM_VAR_TYPE + let resultv = + env#mk_memory_variable + memref#index (add_offset moffset offset) NUM_VAR_TYPE in + let _ = + log_diagnostics_result + ~tag:"translate_lval:Mem:memory_address" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["e: " ^ (p2s (exp_to_pretty e)); + "offset: " ^ (p2s (offset_to_pretty offset)); + "resultv: " ^ (p2s (resultv#toPretty))] in + resultv + | XVar v when (env#is_initial_value v || env#is_function_return_value v) -> + let resultv = + (match type_of_exp fdecls e with + | TPtr (t, _) -> + env#mk_base_address_memory_variable v offset t NUM_VAR_TYPE + | _ -> + env#mk_temp NUM_VAR_TYPE) in + let _ = + log_diagnostics_result + ~tag:"translate_lval" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["v: " ^ (p2s v#toPretty); + "resultv: " ^ (p2s resultv#toPretty)] in + resultv + | XVar _ -> + let _ = + log_diagnostics_result + ~tag:"translate_lval:Mem:Var" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["lval: " ^ (p2s (lval_to_pretty lval))] in + env#mk_temp NUM_VAR_TYPE + | XOp (XPlus, [XVar base; XConst (IntConst n)]) + when (env#is_initial_value base || env#is_function_return_value base) -> + let ioffset = CCHTypesUtil.mk_constant_index_offset n in + let (resultv, t) = + (match type_of_exp fdecls e with + | TPtr (t, _) -> + (env#mk_base_address_memory_variable base ioffset t NUM_VAR_TYPE, t) + | _ -> + raise + (CCHFailure + (LBLOCK [STR "Unexpected type in dereference"]))) in + let _ = + log_diagnostics_result + ~tag:"translate_lval:index" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["base: " ^ (p2s base#toPretty); + "ioff: " ^ n#toString; + "typ: " ^ (p2s (typ_to_pretty t)); + "resultv: " ^ (p2s resultv#toPretty)] in + resultv + + | XOp (XPlus, [XVar base; XConst (IntConst n)]) + when env#is_memory_address base -> + let ioffset = CCHTypesUtil.mk_constant_index_offset n in + let (memref, memoff) = env#get_memory_address base in + let v = + env#mk_memory_variable memref#index + (add_offset memoff ioffset) NUM_VAR_TYPE in + let _ = + log_diagnostics_result + ~tag:"translate_lval" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["base: " ^ (p2s base#toPretty); + "ioff: " ^ n#toString; + "v: " ^ (p2s v#toPretty)] in + v + | mem_e -> + let _ = + log_diagnostics_result + ~tag:"translate_lval:Mem" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["lval: " ^ (p2s (lval_to_pretty lval)); + "mem_e: " ^ (x2s mem_e)] in + env#mk_temp NUM_VAR_TYPE method private translate_unop_expr op x = match op with @@ -199,7 +285,7 @@ object (self) begin match memxpr with | XVar v when env#is_initial_value v || env#is_function_return_value v -> - let memtype = type_of_exp fdecls e in + let memtype = get_pointer_expr_target_type fdecls e in let memref = vmgr#memrefmgr#mk_external_reference v memtype in XVar (env#mk_memory_address_value memref#index offset) | XVar v when env#is_memory_address v -> @@ -218,13 +304,14 @@ object (self) method private translate_binop_expr op x1 x2 ty = let ty = fenv#get_type_unrolled ty in let result = match op with + (* | PlusA when CCHBasicUtil.exp_is_zero x2 -> (self#translate_expr x1) *) | PlusA -> XOp (XPlus, [self#translate_expr x1; self#translate_expr x2]) | MinusA -> XOp (XMinus, [self#translate_expr x1; self#translate_expr x2]) | Mult -> XOp (XMult, [self#translate_expr x1; self#translate_expr x2]) | Div -> XOp (XDiv, [self#translate_expr x1; self#translate_expr x2]) | PlusPI | IndexPI -> - let targetTyp = match ty with + (* let targetTyp = match ty with | (TPtr (tty, _)) -> tty | _ -> raise @@ -233,7 +320,8 @@ object (self) STR "Application of PlusPI to non-pointer type: "; typ_to_pretty ty])) in let elementSize = size_of_type fdecls targetTyp in - let offsetx = XOp (XMult, [elementSize; self#translate_expr x2]) in + let offsetx = XOp (XMult, [elementSize; self#translate_expr x2]) in *) + let offsetx = self#translate_expr x2 in XOp (XPlus, [self#translate_expr x1; offsetx]) | MinusPP -> begin @@ -445,7 +533,7 @@ object (self) begin match memxpr with | XVar v when env#is_initial_value v || env#is_function_return_value v -> - let memtype = type_of_exp fdecls e in + let memtype = get_pointer_expr_target_type fdecls e in let memref = vmgr#memrefmgr#mk_external_reference v memtype in XVar (env#mk_memory_address_value memref#index offset) | XVar v when env#is_memory_address v -> XVar v @@ -469,16 +557,17 @@ object (self) XOp (XDiv, [self#translate_lhs_expr x1; self#translate_lhs_expr x2]) | PlusPI | IndexPI -> - let targetTyp = match ty with + (* let targetTyp = match ty with | (TPtr (tty, _)) -> tty | _ -> raise (CCHFailure (LBLOCK [ STR "Application of PlusPI to non-pointer type: "; - typ_to_pretty ty])) in - let elementSize = size_of_type fdecls targetTyp in - let xoffset = XOp (XMult, [elementSize; self#translate_lhs_expr x2]) in + typ_to_pretty ty])) in *) + (* let elementSize = size_of_type fdecls targetTyp in *) + (* let xoffset = XOp (XMult, [elementSize; self#translate_lhs_expr x2]) in *) + let xoffset = self#translate_lhs_expr x2 in XOp (XPlus, [self#translate_lhs_expr x1; xoffset]) | MinusPP -> begin @@ -575,7 +664,7 @@ object (self) match memref#get_base with | CStackAddress v -> v | CGlobalAddress v -> v - | CBaseVar v -> v + | CBaseVar (v, _) -> v | _ -> raise (CCHFailure @@ -713,7 +802,7 @@ object (self) begin match memxpr with | XVar v when env#is_initial_value v || env#is_function_return_value v -> - let memtype = type_of_exp fdecls e in + let memtype = get_pointer_expr_target_type fdecls e in let memref = vmgr#memrefmgr#mk_external_reference v memtype in XVar (env#mk_memory_address_value memref#index offset) | XVar v when env#is_memory_address v -> XVar v @@ -732,6 +821,9 @@ object (self) | Ge -> XOp (XGe, [self#translate_expr x1; self#translate_expr x2]) | Ne -> XOp (XNe, [self#translate_expr x1; self#translate_expr x2]) | Eq -> XOp (XEq, [self#translate_expr x1; self#translate_expr x2]) + | PlusPI | IndexPI -> + let offsetx = self#translate_expr x2 in + XOp (XPlus, [self#translate_expr x1; offsetx]) | _ -> random_constant_expr in simplify_xpr result @@ -739,7 +831,16 @@ object (self) let lvar = self#translate_lval lval in if env#has_constant_offset lvar then match orakel#get_external_value context (XVar lvar) with - | Some vx -> vx + | Some vx -> + let _ = + log_diagnostics_result + ~tag:"sym:translate_variable_expr" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["lval: " ^ (p2s (lval_to_pretty lval)); + "lvar: " ^ (p2s lvar#toPretty); + "vx: " ^ (x2s vx)] in + vx | _ -> XVar lvar else XVar lvar @@ -781,15 +882,104 @@ object (self) match self#translate_exp context e with | XVar v when env#is_memory_address v -> let (memref, moffset) = env#get_memory_address v in - env#mk_memory_variable - memref#index (add_offset moffset offset) SYM_VAR_TYPE - | XVar v when env#is_initial_value v -> + let resultv = + env#mk_memory_variable + memref#index (add_offset moffset offset) SYM_VAR_TYPE in + let _ = + log_diagnostics_result + ~tag:"sym:translate_lval" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["e: " ^ (p2s (exp_to_pretty e)); + "v: " ^ (p2s v#toPretty); + "resultv: " ^ (p2s resultv#toPretty)] in + resultv + | XVar v when env#is_initial_value v || env#is_function_return_value v -> + let resultv = + (match type_of_exp fdecls e with + | TPtr (t, _) -> + env#mk_base_address_memory_variable v NoOffset t NUM_VAR_TYPE + | _ -> + env#mk_temp SYM_VAR_TYPE) in + let _ = + log_diagnostics_result + ~tag:"translate_lval" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["v: " ^ (p2s v#toPretty); + "resultv: " ^ (p2s resultv#toPretty)] in + resultv + | XVar _ -> + let _ = + log_diagnostics_result + ~tag:"translate_lval:Mem:Var" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["lval: " ^ (p2s (lval_to_pretty lval))] in + env#mk_temp SYM_VAR_TYPE + | XOp (XPlus, [XVar base; XConst (IntConst n)]) + when (env#is_initial_value base || env#is_function_return_value base) -> + let ioffset = CCHTypesUtil.mk_constant_index_offset n in + let (resultv, t) = + (match type_of_exp fdecls e with + | TPtr (t, _) -> + (env#mk_base_address_memory_variable base ioffset t SYM_VAR_TYPE, t) + | _ -> + raise + (CCHFailure + (LBLOCK [STR "Unexpected type in dereference"]))) in + let _ = + log_diagnostics_result + ~tag:"translate_lval:index" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["base: " ^ (p2s base#toPretty); + "ioff: " ^ n#toString; + "typ: " ^ (p2s (typ_to_pretty t)); + "resultv: " ^ (p2s resultv#toPretty)] in + resultv + + | XOp (XPlus, [XVar base; XConst (IntConst n)]) + when env#is_memory_address base -> + let ioffset = CCHTypesUtil.mk_constant_index_offset n in + let (memref, memoff) = env#get_memory_address base in + let v = + env#mk_memory_variable memref#index + (add_offset memoff ioffset) SYM_VAR_TYPE in + let _ = + log_diagnostics_result + ~tag:"translate_lval" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["base: " ^ (p2s base#toPretty); + "ioff: " ^ n#toString; + "v: " ^ (p2s v#toPretty)] in + v + | mem_e -> + let _ = + log_diagnostics_result + ~tag:"translate_lval:Mem" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["lval: " ^ (p2s (lval_to_pretty lval)); + "e: " ^ (p2s (exp_to_pretty e)); + "mem_e: " ^ (x2s mem_e)] in + env#mk_temp SYM_VAR_TYPE +(* let memtype = get_pointer_expr_target_type fdecls e in let memref = - env#get_variable_manager#memrefmgr#mk_external_reference - v (type_of_exp fdecls e) in - env#mk_memory_variable memref#index offset SYM_VAR_TYPE + env#get_variable_manager#memrefmgr#mk_external_reference v memtype in + let resultv = env#mk_memory_variable memref#index offset SYM_VAR_TYPE in + let _ = + log_diagnostics_result + ~tag:"sym:translate_lval" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["e: " ^ (p2s (exp_to_pretty e)); + "v: " ^ (p2s v#toPretty); + "resultv: " ^ (p2s v#toPretty)] in + resultv | _ -> - env#mk_temp SYM_VAR_TYPE + env#mk_temp SYM_VAR_TYPE *) method translate_condition (context: program_context_int) (c: exp) = let make_assume (x:xpr_t) = diff --git a/CodeHawk/CHC/cchanalyze/cCHExtractInvariantFacts.ml b/CodeHawk/CHC/cchanalyze/cCHExtractInvariantFacts.ml index 35c55033..eb70e555 100644 --- a/CodeHawk/CHC/cchanalyze/cCHExtractInvariantFacts.ml +++ b/CodeHawk/CHC/cchanalyze/cCHExtractInvariantFacts.ml @@ -63,6 +63,9 @@ open CCHNumericalConstraints module H = Hashtbl +let p2s = CHPrettyUtil.pretty_to_string + + exception TimeOut of float @@ -530,7 +533,7 @@ let extract_valuesets let extract_symbols - (_env:c_environment_int) + (env:c_environment_int) (invio:invariant_io_int) (invariants:(string, (string,atlas_t) H.t) H.t) = try @@ -539,6 +542,15 @@ let extract_symbols let inv = H.find v symbolic_sets_domain in let context = get_context k in let facts = extract_symbol_facts symbolic_sets_domain inv in + let _ = + log_diagnostics_result + ~tag:"extract_symbols" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["facts: " ^ + (String.concat ", " + (List.map (fun f -> + (p2s (invariant_fact_to_pretty f))) facts))] in List.iter (fun f -> invio#add_fact context f) facts) invariants with | CCHFailure p -> diff --git a/CodeHawk/CHC/cchanalyze/cCHFunctionTranslator.ml b/CodeHawk/CHC/cchanalyze/cCHFunctionTranslator.ml index f59f109f..8729f3dc 100644 --- a/CodeHawk/CHC/cchanalyze/cCHFunctionTranslator.ml +++ b/CodeHawk/CHC/cchanalyze/cCHFunctionTranslator.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2024 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 @@ -97,30 +97,37 @@ object (self) List.fold_left (fun acc vinfo -> let ttyp = fenv#get_type_unrolled vinfo.vtype in match ttyp with - | TPtr ((TInt _ | TFloat _), _) -> - let (v, vInit, vm, vmInit) = - env#mk_par_deref_init vinfo NoOffset ttyp NUM_VAR_TYPE in + | TPtr ((TInt _ | TFloat _) as basetype, _) -> + let (vm, vmInit) = + env#mk_par_deref_init vinfo NoOffset basetype NUM_VAR_TYPE in let _ = log_diagnostics_result + ~tag:"get_deref_assigns:scalar" ~msg:env#get_functionname __FILE__ __LINE__ - ["v: " ^ (p2s v#toPretty); - "vInit: " ^ (p2s vInit#toPretty); - "vm: " ^ (p2s vm#toPretty); + ["vm: " ^ (p2s vm#toPretty); "vmInit: " ^ (p2s vmInit#toPretty)] in - (ASSIGN_NUM (v, NUM_VAR vInit)) - :: (ASSIGN_NUM (vm, NUM_VAR vmInit)) - :: acc + (ASSIGN_NUM (vm, NUM_VAR vmInit)) :: acc | TPtr (TComp (ckey, _), _) -> (List.map (fun (v, vInit) -> ASSIGN_NUM (v, NUM_VAR vInit)) (env#mk_struct_par_deref vinfo ttyp ckey NUM_VAR_TYPE)) @ acc - | TPtr (TPtr _,_) -> - let (v, vInit, vm, vmInit) = - env#mk_par_deref_init vinfo NoOffset ttyp NUM_VAR_TYPE in - (ASSIGN_NUM (v, NUM_VAR vInit)) - :: (ASSIGN_NUM (vm, NUM_VAR vmInit)) - :: acc + | TPtr (TPtr _ as basetype, _) -> + if env#get_functionname = "main" then + (List.map + (fun (v, vInit) -> ASSIGN_NUM (v, NUM_VAR vInit)) + (env#mk_array_par_deref vinfo basetype 6 NUM_VAR_TYPE)) @ acc + else + let (vm, vmInit) = + env#mk_par_deref_init vinfo NoOffset basetype NUM_VAR_TYPE in + let _ = + log_diagnostics_result + ~tag:"get_deref_assigns:pointer" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["vm: " ^ (p2s vm#toPretty); + "vmInit: " ^ (p2s vmInit#toPretty)] in + (ASSIGN_NUM (vm, NUM_VAR vmInit)) :: acc | _ -> acc) [] formals method private assert_global_values globals = @@ -181,6 +188,7 @@ object (self) let fsymbol = EU.symbol f.svar.vname in let proc = EU.mkProcedure fsymbol ~signature:[] ~bindings:[] ~scope ~body:fbody in + (* let _ = CHPretty.pr_debug [proc#toPretty; NL; NL] in *) let csystem = EU.mkSystem (new symbol_t "c-system") in let _ = csystem#addProcedure proc in (None, csystem) @@ -373,6 +381,7 @@ object let fsymbol = EU.symbol f.svar.vname in let proc = EU.mkProcedure fsymbol ~signature:[] ~bindings:[] ~scope ~body:fbody in + (* let _ = CHPretty.pr_debug [proc#toPretty; NL; NL] in *) let csystem = EU.mkSystem (new symbol_t "c-system") in let _ = csystem#addProcedure proc in (None, csystem) diff --git a/CodeHawk/CHC/cchanalyze/cCHNumericalConstraints.ml b/CodeHawk/CHC/cchanalyze/cCHNumericalConstraints.ml index 385ca587..4a4e0baa 100644 --- a/CodeHawk/CHC/cchanalyze/cCHNumericalConstraints.ml +++ b/CodeHawk/CHC/cchanalyze/cCHNumericalConstraints.ml @@ -36,7 +36,7 @@ open CHPretty open CHUtils (* cchlib *) -open CCHUtilities +(* open CCHUtilities *) (* cchanalyze *) open CCHAnalysisTypes @@ -133,7 +133,7 @@ object (self) let _ = if coeff1#equal numerical_zero || coeff2#equal numerical_zero then raise - (CCHFailure + (CHCommon.CHFailure (LBLOCK [ STR "Internal error in elimination of "; v#toPretty; diff --git a/CodeHawk/CHC/cchanalyze/cCHOperationsProvider.ml b/CodeHawk/CHC/cchanalyze/cCHOperationsProvider.ml index a6bec502..c44e73ce 100644 --- a/CodeHawk/CHC/cchanalyze/cCHOperationsProvider.ml +++ b/CodeHawk/CHC/cchanalyze/cCHOperationsProvider.ml @@ -59,6 +59,8 @@ open CCHCommand module H = Hashtbl let x2p = xpr_formatter#pr_expr +let p2s = CHPrettyUtil.pretty_to_string +let x2s x = p2s (x2p x) module ProgramContextCollections = CHCollections.Make @@ -190,14 +192,27 @@ object (self) [make_c_cmd SKIP] | _ -> match exp_translator#translate_exp context e with - | XVar symvar -> [make_c_cmd (ASSIGN_SYM (v, SYM_VAR symvar))] - | XConst _ -> [make_c_cmd SKIP] + | XVar symvar -> + let _ = + log_diagnostics_result + ~tag:"make_context_operation:sym:symvar" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["e: " ^ (p2s (exp_to_pretty e)); + "symvar: " ^ (p2s symvar#toPretty)] in + [make_c_cmd (ASSIGN_SYM (v, SYM_VAR symvar))] + | XConst _ -> + [make_c_cmd SKIP] | xpr -> begin - chlog#add "no symbolic check value assigned" - (LBLOCK [STR env#get_functionname; STR ": "; - exp_to_pretty e; STR " --> "; - x2p xpr]); + log_diagnostics_result + ~tag:"make_context_operation:sym" + ~msg:env#get_functionname + __FILE__ __LINE__ + ["no symbolic check value assigned for: " ^ + "e: " ^ (p2s (exp_to_pretty e)); + "translated to: " ^ + "xpr: " ^ (x2s xpr)]; [make_c_cmd SKIP] end end diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckAllocationBase.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckAllocationBase.ml index d7d5add2..b36f399b 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckAllocationBase.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckAllocationBase.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - Copyright (c) 2024 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 @@ -151,7 +151,7 @@ object (self) let deps = DLocal [invindex] in let msg = "address of stack variable: " ^ vinfo.vname in Some (deps,msg) - | CBaseVar v -> self#var_is_stack_memory invindex v + | CBaseVar (v, _) -> self#var_is_stack_memory invindex v | _ -> None method private var_is_stack_memory (invindex: int) (v: variable_t) = @@ -413,7 +413,7 @@ object (self) method private memref_implies_delegation (invindex: int) (memref: memory_reference_int) = match memref#get_base with - | CBaseVar v -> self#var_implies_delegation invindex v + | CBaseVar (v, _) -> self#var_implies_delegation invindex v | _ -> None method private var_implies_delegation (invindex: int) (v: variable_t) = diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckInScope.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckInScope.ml index 727c4a3b..06c934e2 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckInScope.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckInScope.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - Copyright (c) 2024 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 @@ -123,7 +123,7 @@ object (self) let deps = DLocal [invindex] in match memrefbase with | CStackAddress stackvar when poq#env#is_local_variable stackvar -> - let (vinfo,offset) = poq#env#get_local_variable stackvar in + let (vinfo, offset) = poq#env#get_local_variable stackvar in let msg = self#var_address_to_string vinfo offset in Some (deps, msg) | CStringLiteral _ -> @@ -133,7 +133,7 @@ object (self) let (vinfo, offset) = poq#env#get_global_variable gvar in let msg = self#var_address_to_string vinfo offset in Some (deps, msg) - | CBaseVar v -> self#var_implies_safe invindex v + | CBaseVar (v, _) -> self#var_implies_safe invindex v | _ -> None method private var_implies_safe (invindex: int) (v: variable_t) = @@ -230,21 +230,6 @@ object (self) r method check_safe = - let safemsg = fun index arg_count -> ("command-line argument" - ^ (string_of_int index) - ^ " is guaranteed to be in scope" - ^ " for argument count " - ^ (string_of_int arg_count)) in - let vmsg = fun index arg_count -> ("command-line argument " - ^ (string_of_int index) - ^ " is not included in argument count of " - ^ (string_of_int arg_count)) in - let dmsg = fun index -> ("no invariant found for argument count; " - ^ "unable to validate scope of " - ^ "command-line argument " - ^ (string_of_int index)) in - - poq#check_command_line_argument e safemsg vmsg dmsg || match invs with | [] -> begin diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml index 7a45b62b..4c4bd6bf 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - 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 @@ -71,60 +71,6 @@ class initialized_checker_t (poq:po_query_int) (lval:lval) (invs:invariant_int list) = object (self) - method private check_program_name = - if poq#is_command_line_argument (Lval lval) then - let index = poq#get_command_line_argument_index (Lval lval) in - if index == 0 then - begin - (* first index into argv is always safe, it is the program name *) - poq#record_safe_result - (DLocal []) - ("command-line argument " - ^ (string_of_int index) - ^ " is guaranteed initialized by the operating system"); - true - end - else - false - else - false - - method private check_command_line_argument = - if poq#is_command_line_argument (Lval lval) then - let index = poq#get_command_line_argument_index (Lval lval) in - match poq#get_command_line_argument_count with - | Some (inv, arg_count) -> - if index < arg_count then - begin - poq#record_safe_result - (DLocal [inv]) - ("command-line argument " - ^ (string_of_int index) - ^ " is guaranteed initialized for argument count " - ^ (string_of_int arg_count)); - true - end - else - begin - poq#record_violation_result - (DLocal [inv]) - ("command-line argument " - ^ (string_of_int index) - ^ " is not included in argument count of " - ^ (string_of_int arg_count)); - true - end - | _ -> - begin - poq#set_diagnostic - ("no invariant found for argument count; unable to validate access of " - ^ "command-line argument " - ^ (string_of_int index)); - false - end - else - false - method private get_symbol_name (s: symbol_t) = s#getBaseName ^ (match s#getAttributes with @@ -153,8 +99,6 @@ object (self) (* ----------------------------- safe ------------------------------------- *) (* check_safe - inv_implies_safe - - inv_xpr_implies_safe - - inv_bounded_xpr_implies_safe - check_safe_command_line_argument - check_safe_lval - check_safe_memlval @@ -164,29 +108,6 @@ object (self) - memlval_vinv_memref_basevar_implies_safe *) - method private inv_xpr_implies_safe (invindex: int) (x: xpr_t) = - let deps = DLocal [invindex] in - let msg = - "variable " - ^ (p2s (lval_to_pretty lval)) - ^ " has the value " - ^ (x2s x) in - let site = Some (__FILE__, __LINE__, "inv_xpr_implies_safe") in - Some (deps, msg, site) - - method private inv_bounded_xpr_implies_safe - (invindex: int) (lb: xpr_t) (ub: xpr_t) = - let deps = DLocal [invindex] in - let msg = - "variable " - ^ (p2s (lval_to_pretty lval)) - ^ " is bounded by LB: " - ^ (x2s lb) - ^ " and UB: " - ^ (x2s ub) in - let site = Some (__FILE__, __LINE__, "inv_bounded_xpr_implies_safe") in - Some (deps, msg, site) - method private inv_implies_safe (inv: invariant_int) = let mname = "inv_implies_safe" in match inv#get_fact with @@ -204,14 +125,7 @@ object (self) let site = Some (__FILE__, __LINE__, mname) in Some (deps, msg, site) end - | _ -> - match inv#expr with - | Some x -> self#inv_xpr_implies_safe inv#index x - | _ -> - match (inv#lower_bound_xpr, inv#upper_bound_xpr) with - | (Some lb, Some ub) -> - self#inv_bounded_xpr_implies_safe inv#index lb ub - | _ -> None + | _ -> None method private check_safe_functionpointer (vinfo: varinfo) = let vinfovalues = poq#get_vinfo_offset_values vinfo in @@ -436,7 +350,7 @@ object (self) self#memlval_vinv_memref_stackvar_implies_safe invindex vinfo | _ -> None) - | CBaseVar v -> + | CBaseVar (v, _) -> (try self#memlval_vinv_memref_basevar_implies_safe invindex v memoffset with @@ -556,8 +470,7 @@ object (self) | _ -> false method check_safe = - self#check_command_line_argument - || (List.fold_left (fun acc inv -> + (List.fold_left (fun acc inv -> acc || match self#inv_implies_safe inv with | Some (deps, msg, site) -> @@ -666,9 +579,39 @@ object (self) None method private inv_implies_delegation (inv: invariant_int) = - match inv#expr with - | Some x -> self#xpr_implies_delegation inv#index x - | _ -> None + let mname = "inv_implies_delegation" in + let r = None in + let r = + match r with + | Some _ -> r + | _ -> + match inv#expr with + | Some (XVar v) when + poq#env#is_mut_memory_address v || poq#env#is_ref_memory_address v -> + begin + (match poq#x2api (XVar v) with + | Some a1 when poq#is_api_expression (XVar v) -> + (match a1 with + | Lval lval -> + let pred = PInitialized lval in + let deps = DEnvC ([inv#index], [ApiAssumption pred]) in + let msg = + "exclusive reference " ^ (p2s v#toPretty) + ^ "; condition " ^ (p2s (po_predicate_to_pretty pred)) + ^ " delegated to the api" in + let site = Some (__FILE__, __LINE__, mname) in + Some (deps, msg, site) + | _ -> None) + | _ -> + begin + poq#set_diagnostic ("exclusive reference: " ^ (p2s v#toPretty)); + None + end) + end + | Some x -> + self#xpr_implies_delegation inv#index x + | _ -> None in + r method private check_delegation_invs = match invs with @@ -805,10 +748,7 @@ object (self) | _ -> false method check_delegation = - if self#check_program_name then - false - else - self#check_delegation_invs || self#check_delegation_lval + self#check_delegation_invs || self#check_delegation_lval end diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckInitializedRange.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckInitializedRange.ml index fb5608cf..ef9e9583 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckInitializedRange.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckInitializedRange.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - Copyright (c) 2024 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 @@ -32,6 +32,7 @@ open CHNumerical open CHPretty (* chutil *) +open CHLogger open CHPrettyUtil (* xprlib *) @@ -46,6 +47,7 @@ open CCHUtilities (* cchpre *) open CCHMemoryBase +open CCHPOPredicate open CCHPreTypes open CCHProofObligation @@ -121,26 +123,69 @@ object (self) | _ -> None) None invs2 | _ -> None - method private get_initialization_length (vinfo: varinfo) = - let vinfovalues = poq#get_vinfo_offset_values vinfo in - List.fold_left (fun acc (inv,offset) -> + method private get_initialization_length_from_memory_variable (vinfo: varinfo) = + let memvar = + poq#env#mk_stack_memory_variable vinfo NoOffset vinfo.vtype SYM_VAR_TYPE in + let varinvs = poq#get_var_invariants memvar in + let _ = + log_diagnostics_result + ~tag:"get_initialization_length_from_memory_variable" + __FILE__ __LINE__ + ["vinfo: " ^ vinfo.vname; + "memvar: " ^ (p2s memvar#toPretty); + "memvar-invariants: " ^ + (String.concat ", " (List.map (fun inv -> p2s inv#toPretty) varinvs))] in + List.fold_left (fun acc inv -> match acc with | Some _ -> acc | _ -> - match offset with - | Field _ | Index _ -> None - | NoOffset -> - match inv#get_fact with - | NonRelationalFact(_,FInitializedSet [sym]) - when is_initialized_range sym -> - begin - match get_initialized_range_len sym with - | Some (irname, irlen) -> - let deps = DLocal [inv#index] in - Some (deps, irname,irlen) - | _ -> None - end - | _ -> None) None vinfovalues + match inv#get_fact with + | NonRelationalFact(_, FInitializedSet [sym]) + when is_initialized_range sym -> + begin + match get_initialized_range_len sym with + | Some (irname, irlen) -> + let deps = DLocal [inv#index] in + Some (deps, irname, irlen) + | _ -> None + end + | _ -> None) None varinvs + + method private get_initialization_length (vinfo: varinfo) = + let vinfovalues = poq#get_vinfo_offset_values vinfo in + let _ = + log_diagnostics_result + ~tag:"get_initialization_length" + ~msg:poq#env#get_functionname + __FILE__ __LINE__ + ["vinfo: " ^ vinfo.vname; + "vinfo-values: " ^ + (String.concat ", " + (List.map (fun (inv, offset) -> + "(" ^ (p2s inv#toPretty) ^ ", " ^ (p2s (offset_to_pretty offset))) + vinfovalues))] in + match vinfovalues with + | [] -> + self#get_initialization_length_from_memory_variable vinfo + | _ -> + List.fold_left (fun acc (inv, offset) -> + match acc with + | Some _ -> acc + | _ -> + match offset with + | Field _ | Index _ -> None + | NoOffset -> + match inv#get_fact with + | NonRelationalFact(_,FInitializedSet [sym]) + when is_initialized_range sym -> + begin + match get_initialized_range_len sym with + | Some (irname, irlen) -> + let deps = DLocal [inv#index] in + Some (deps, irname,irlen) + | _ -> None + end + | _ -> None) None vinfovalues method private get_element_initializations (vinfo: varinfo) = let vinfovalues = poq#get_vinfo_offset_values vinfo in @@ -320,20 +365,6 @@ object (self) | _ -> None method check_safe = - let safemsg = fun index arg_count -> ("command-line argument" - ^ (string_of_int index) - ^ " is guaranteed initialized for argument count " - ^ (string_of_int arg_count)) in - let vmsg = fun index arg_count -> ("command-line argument " - ^ (string_of_int index) - ^ " is not included in argument count of " - ^ (string_of_int arg_count)) in - let dmsg = fun index -> ("no invariant found for argument count; " - ^ "unable to validate initialization of " - ^ "command-line argument " - ^ (string_of_int index)) in - - poq#check_command_line_argument e1 safemsg vmsg dmsg || match self#unsigned_length_conflict with | Some _ -> false | _ -> @@ -361,7 +392,54 @@ object (self) | _ -> false (* ----------------------- delegation ------------------------------------- *) - method check_delegation = false + + method private inv_implies_delegation (inv: invariant_int) = + let r = None in + let r = + match r with + | Some _ -> r + | _ -> + match inv#expr with + | Some (XVar v) when + poq#env#is_mut_memory_address v || poq#env#is_ref_memory_address v -> + begin + (match poq#x2api (XVar v) with + | Some a1 when poq#is_api_expression (XVar v) -> + (match e2 with + | CnApp ("ntp", [Some len], xx) + | CastE (_, CnApp ("ntp", [Some len], xx)) + when (cd#index_exp e1) = (cd#index_exp len) -> + let a2 = CnApp ("ntp", [Some a1], xx) in + let pred = PInitializedRange (a1, a2) in + let deps = DEnvC ([inv#index], [ApiAssumption pred]) in + let msg = + "exclusive reference " ^ (p2s v#toPretty) + ^ "; condition " ^ (p2s (po_predicate_to_pretty pred)) + ^ " delegated to the api" in + Some (deps, msg) + | _ -> None) + | _ -> + begin + poq#set_diagnostic ("exclusive reference: " ^ (p2s v#toPretty)); + None + end) + end + | _ -> None in + r + + method check_delegation = + match invs1 with + | [] -> false + | _ -> + List.fold_left (fun acc inv -> + acc || + (match self#inv_implies_delegation inv with + | Some (deps, msg) -> + begin + poq#record_safe_result deps msg; + true + end + | _ -> false)) false invs1 end diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckIntOverflow.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckIntOverflow.ml index 60baad2c..c4bc6b83 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckIntOverflow.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckIntOverflow.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - Copyright (c) 2024 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 @@ -175,7 +175,7 @@ object (self) let (memref, _offset) = poq#env#get_memory_address v in begin match memref#get_base with - | CBaseVar bv -> + | CBaseVar (bv, _) -> let _ = poq#set_diagnostic_arg arg ("base var: " ^ (p2s bv#toPretty)) in diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckIntUnderflow.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckIntUnderflow.ml index 31139afd..a7e68cd3 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckIntUnderflow.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckIntUnderflow.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - Copyright (c) 2024 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 @@ -878,7 +878,7 @@ object (self) let (memref, _offset) = poq#env#get_memory_address v in begin match memref#get_base with - | CBaseVar bv -> + | CBaseVar (bv, _) -> let _ = poq#set_diagnostic_arg arg ("base var: " ^ (p2s bv#toPretty)) in diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckLocallyInitialized.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckLocallyInitialized.ml index 88d4b0b7..525168bb 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckLocallyInitialized.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckLocallyInitialized.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2025 Aarno Labs LLC + Copyright (c) 2025-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 @@ -123,7 +123,7 @@ object (self) ^ vinfo.vname in let site = Some (__FILE__, __LINE__, mname) in Some (deps, msg, site) - | CBaseVar bvar -> + | CBaseVar (bvar, _) -> self#memlval_memref_basevar_implies_safe invindex bvar | _ -> begin diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckLowerBound.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckLowerBound.ml index 344a15ad..e5260a60 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckLowerBound.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckLowerBound.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - Copyright (c) 2024 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 @@ -90,7 +90,7 @@ object (self) let (vinfo, _offset) = poq#env#get_local_variable svar in let msg = "address of stack variable: " ^ vinfo.vname in Some (deps, msg) - | CBaseVar svar -> + | CBaseVar (svar, _) -> let msg = "address of externally provided variable/field: " ^ svar#getName#getBaseName in @@ -198,21 +198,6 @@ object (self) | _ -> None method check_safe = - let safemsg = fun index arg_count -> ("command-line argument" - ^ (string_of_int index) - ^ " is guaranteed to be valid to access" - ^ " for argument count " - ^ (string_of_int arg_count)) in - let vmsg = fun index arg_count -> ("command-line argument " - ^ (string_of_int index) - ^ " is not included in argument count of " - ^ (string_of_int arg_count)) in - let dmsg = fun index -> ("no invariant found for argument count; " - ^ "unable to validate access of " - ^ "command-line argument " - ^ (string_of_int index)) in - - poq#check_command_line_argument e safemsg vmsg dmsg || match invs with | [] -> begin @@ -270,7 +255,7 @@ object (self) None | _ -> None end - | CBaseVar v -> + | CBaseVar (v, _) -> self#var_offset_implies_universal_violation invindex v xoffset | _ -> None diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckNoOverlap.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckNoOverlap.ml index 2535da6c..d696a93a 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckNoOverlap.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckNoOverlap.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - Copyright (c) 2024 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 @@ -106,7 +106,7 @@ object (self) let memref = poq#env#get_memory_reference v in let _ = poq#set_diagnostic_arg arg (self#memref_to_string memref) in match memref#get_base with - | CBaseVar basevar -> self#is_alloca_address arg basevar invindex + | CBaseVar (basevar, _) -> self#is_alloca_address arg basevar invindex | _ -> None else None @@ -135,7 +135,7 @@ object (self) let memref = poq#env#get_memory_reference v in let _ = poq#set_diagnostic_arg arg (self#memref_to_string memref) in match memref#get_base with - | CBaseVar basevar -> + | CBaseVar (basevar, _) -> if poq#is_api_expression (XVar basevar) then let xapi = poq#get_api_expression (XVar basevar) in let deps = DLocal [invindex] in diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckNotNull.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckNotNull.ml index 7e7c63bf..4de29b9d 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckNotNull.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckNotNull.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - Copyright (c) 2024 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 @@ -57,7 +57,7 @@ let x2s x = p2s (x2p x) let e2s e = p2s (exp_to_pretty e) -class not_null_checker_t (poq:po_query_int) (e:exp) (invs:invariant_int list) = +class not_null_checker_t (poq:po_query_int) (_e:exp) (invs:invariant_int list) = object (self) method private memref_to_string memref = @@ -158,7 +158,7 @@ object (self) | CStringLiteral _ -> let msg = "address of string literal" in Some (deps, msg) - | CBaseVar v -> self#xpr_implies_safe invindex (XVar v) + | CBaseVar (v, _) -> self#xpr_implies_safe invindex (XVar v) | _ -> None method private memory_variable_safe (_invindex: int) (v: variable_t) = @@ -277,30 +277,15 @@ object (self) r method check_safe = - let safemsg = fun index arg_count -> ("command-line argument" - ^ (string_of_int index) - ^ " is guaranteed not null" - ^ " for argument count " - ^ (string_of_int arg_count)) in - let vmsg = fun index arg_count -> ("command-line argument " - ^ (string_of_int index) - ^ " is not included in argument count of " - ^ (string_of_int arg_count)) in - let dmsg = fun index -> ("no invariant found for argument count; " - ^ "unable to validate not-null of " - ^ "command-line argument " - ^ (string_of_int index)) in - - poq#check_command_line_argument e safemsg vmsg dmsg - || (List.fold_left (fun acc inv -> - acc || - match self#inv_implies_safe inv with - | Some (deps,msg) -> - begin - poq#record_safe_result deps msg; - true - end - | _ -> false) false invs) + (List.fold_left (fun acc inv -> + acc || + match self#inv_implies_safe inv with + | Some (deps,msg) -> + begin + poq#record_safe_result deps msg; + true + end + | _ -> false) false invs) (* ----------------------- violation -------------------------------------- *) @@ -311,7 +296,7 @@ object (self) method private memref_implies_delegation (invindex: int) (memref: memory_reference_int) = match memref#get_base with - | CBaseVar v when poq#is_api_expression (XVar v) -> + | CBaseVar (v, _) when poq#is_api_expression (XVar v) -> let a = poq#get_api_expression (XVar v) in let pred = PNotNull a in let deps = DEnvC ([invindex],[ApiAssumption pred]) in diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckNullTerminated.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckNullTerminated.ml index 982c520a..965dc3a3 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckNullTerminated.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckNullTerminated.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - Copyright (c) 2024 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 @@ -44,6 +44,7 @@ open CCHTypesToPretty (* cchpre *) open CCHMemoryBase +open CCHPOPredicate open CCHPreTypes (* cchanalyze *) @@ -166,21 +167,6 @@ object (self) | _ -> None method check_safe = - let safemsg = fun index arg_count -> ("command-line argument" - ^ (string_of_int index) - ^ " is guaranteed to be null-termianted" - ^ " for argument count " - ^ (string_of_int arg_count)) in - let vmsg = fun index arg_count -> ("command-line argument " - ^ (string_of_int index) - ^ " is not included in argument count of " - ^ (string_of_int arg_count)) in - let dmsg = fun index -> ("no invariant found for argument count; " - ^ "unable to validate null-termination of " - ^ "command-line argument " - ^ (string_of_int index)) in - - poq#check_command_line_argument e safemsg vmsg dmsg || match invs with | [] -> begin @@ -201,7 +187,49 @@ object (self) (* ----------------------- violation -------------------------------------- *) method check_violation = false (* ----------------------- delegation ------------------------------------- *) - method check_delegation = false + + method private inv_implies_delegation (inv: invariant_int) = + let r = None in + let r = + match r with + | Some _ -> r + | _ -> + match inv#expr with + | Some (XVar v) when + poq#env#is_mut_memory_address v || poq#env#is_ref_memory_address v -> + begin + (match poq#x2api (XVar v) with + | Some a1 when poq#is_api_expression (XVar v) -> + let pred = PNullTerminated a1 in + let deps = DEnvC ([inv#index], [ApiAssumption pred]) in + let msg = + "exclusive reference " ^ (p2s v#toPretty) + ^ "; condition " ^ (p2s (po_predicate_to_pretty pred)) + ^ " delegated to the api" in + Some (deps, msg) + | _ -> + begin + poq#set_diagnostic ("exclusive reference: " ^ (p2s v#toPretty)); + None + end) + end + | _ -> None in + r + + method check_delegation = + match invs with + | [] -> false + | _ -> + List.fold_left (fun acc inv -> + acc || + (match self#inv_implies_delegation inv with + | Some (deps, msg) -> + begin + poq#record_safe_result deps msg; + true + end + | _ -> false)) false invs + end diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterInitialized.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterInitialized.ml index 36504faa..8e28f5f4 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterInitialized.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterInitialized.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2025 Aarno Labs LLC + Copyright (c) 2025-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 @@ -83,7 +83,7 @@ object (self) if poq#env#is_memory_variable paramvar then let (memref, _offset) = poq#env#get_memory_variable paramvar in (match memref#get_base with - | CBaseVar base when poq#env#is_initial_parameter_value base -> + | CBaseVar (base, _) when poq#env#is_initial_parameter_value base -> let basevar = poq#env#get_initial_value_variable base in if basevar#equal numv then let deps = DLocal ([invindex]) in diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterUnaltered.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterUnaltered.ml index b9f47213..417eb904 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterUnaltered.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterUnaltered.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2025 Aarno Labs LLC + Copyright (c) 2025-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 @@ -92,7 +92,7 @@ object (self) (invindex: int) (memref: memory_reference_int) = let mname = "memlval_memref_implies_safe" in match memref#get_base with - | CBaseVar bvar -> + | CBaseVar (bvar, _) -> self#memlval_memref_basevar_implies_safe invindex bvar | _ -> begin @@ -148,7 +148,7 @@ object (self) if poq#env#is_memory_variable paramvar then let (memref, _offset) = poq#env#get_memory_variable paramvar in (match memref#get_base with - | CBaseVar base -> + | CBaseVar (base, _) -> let basevar = poq#env#get_initial_value_variable base in if basevar#equal numv then let deps = DLocal ([invindex]) in diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckPointerCast.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckPointerCast.ml index 36a4f3b2..61388a29 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckPointerCast.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckPointerCast.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - Copyright (c) 2024 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 @@ -160,7 +160,7 @@ object (self) | CStackAddress svar -> let (vinfo, offset) = poq#env#get_local_variable svar in self#declared_variable_implies_safe false invindex vinfo offset - | CBaseVar v -> self#var_implies_safe invindex v + | CBaseVar (v, _) -> self#var_implies_safe invindex v | _ -> None method private var_implies_safe (invindex: int) (v: variable_t) = @@ -273,7 +273,7 @@ object (self) else if poq#env#is_memory_address v then let (memref,offset) = poq#env#get_memory_address v in match (memref#get_base,offset) with - | (CBaseVar basevar, NoOffset) -> + | (CBaseVar (basevar, _), NoOffset) -> self#var_implies_violation invindex basevar | _ -> None else @@ -313,7 +313,7 @@ object (self) method private memref_implies_delegation (invindex: int) (memref: memory_reference_int) = match memref#get_base with - | CBaseVar v -> self#var_implies_delegation invindex v + | CBaseVar (v, _) -> self#var_implies_delegation invindex v | _ -> None method private var_implies_delegation (invindex: int) (v: variable_t) = diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckPtrLowerBound.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckPtrLowerBound.ml index f1cd1604..d67de014 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckPtrLowerBound.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckPtrLowerBound.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - Copyright (c) 2024 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 @@ -156,7 +156,7 @@ object (self) let (memref, offset) = poq#env#get_memory_address v in begin match (memref#get_base, offset) with - | (CBaseVar basevar, NoOffset) -> + | (CBaseVar (basevar, _), NoOffset) -> self#basevar_implies_minuspi_universal_violation invindices basevar numerical_zero x2 | _ -> None @@ -220,7 +220,7 @@ object (self) Some (deps, msg) else None - | CBaseVar v -> + | CBaseVar (v, _) -> self#basevar_implies_minuspi_universal_violation invindices v offsetlb decr | _ -> None @@ -264,7 +264,7 @@ object (self) let memref = poq#env#get_memory_reference v in begin match memref#get_base with - | CBaseVar v -> + | CBaseVar (v, _) -> self#basevar_implies_pluspi_universal_violation invindices v offsetub incr | _ -> None diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckPtrUpperBound.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckPtrUpperBound.ml index a8363eb9..d9d6a8e7 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckPtrUpperBound.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckPtrUpperBound.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - Copyright (c) 2024 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 @@ -455,21 +455,6 @@ object (self) | _ -> false) acc1 invs2) false invs1 method check_safe = - let safemsg = fun index arg_count -> ("command-line argument" - ^ (string_of_int index) - ^ " is guaranteed to be valid to access" - ^ " for argument count " - ^ (string_of_int arg_count)) in - let vmsg = fun index arg_count -> ("command-line argument " - ^ (string_of_int index) - ^ " is not included in argument count of " - ^ (string_of_int arg_count)) in - let dmsg = fun index -> ("no invariant found for argument count; " - ^ "unable to validate access of " - ^ "command-line argument " - ^ (string_of_int index)) in - - poq#check_command_line_argument e1 safemsg vmsg dmsg || match self#null_terminated_string_implies_pluspi_safe with | Some (deps,msg) -> begin @@ -758,7 +743,7 @@ object (self) else if poq#env#is_memory_address v1 then let (memref, _offset) = poq#env#get_memory_address v1 in match memref#get_base with - | CBaseVar basevar -> + | CBaseVar (basevar, _) -> self#var_const_implies_delegation invindices basevar n | _ -> None else @@ -777,12 +762,46 @@ object (self) else if poq#env#is_memory_address v1 then let (memref, _offset) = poq#env#get_memory_address v1 in match memref#get_base with - | CBaseVar basevar -> + | CBaseVar (basevar, _) -> self#var_api_implies_delegation invindices basevar a2 | _ -> None else None + method private inv1_implies_delegation (inv: invariant_int) = + let r = None in + let r = + match r with + | Some _ -> r + | _ -> + match inv#expr with + | Some (XVar v) when + poq#env#is_mut_memory_address v || poq#env#is_ref_memory_address v -> + begin + (match poq#x2api (XVar v) with + | Some a1 when poq#is_api_expression (XVar v) -> + (match e2 with + | CnApp ("ntp", [Some len], xx) + | CastE (_, CnApp ("ntp", [Some len], xx)) + when (cd#index_exp e1) = (cd#index_exp len) -> + let a2 = CnApp ("ntp", [Some a1], xx) in + let pred = self#get_predicate a1 a2 in + let deps = DEnvC ([inv#index], [ApiAssumption pred]) in + let msg = + "exclusive reference " ^ (p2s v#toPretty) + ^ "; condition " ^ (p2s (po_predicate_to_pretty pred)) + ^ " delegated to the api" in + Some (deps, msg) + | _ -> None) + | _ -> + begin + poq#set_diagnostic ("exclusive reference: " ^ (p2s v#toPretty)); + None + end) + end + | _ -> None in + r + method private inv_implies_delegation (inv1: invariant_int) (inv2: invariant_int) = let r = None in @@ -876,7 +895,17 @@ object (self) method check_delegation = match (invs1, invs2) with - | ([], _) | (_, []) -> false + | ([], _) -> false + | (_, []) -> + List.fold_left (fun acc1 inv1 -> + acc1 || + match self#inv1_implies_delegation inv1 with + | Some (deps, msg) -> + begin + poq#record_safe_result deps msg; + true + end + | _ -> false) false invs1 | _ -> List.fold_left (fun acc1 inv1 -> acc1 || diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckStackAddressEscape.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckStackAddressEscape.ml index 258b3cb2..33a93adf 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckStackAddressEscape.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckStackAddressEscape.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - Copyright (c) 2024 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 @@ -111,7 +111,7 @@ object (self) ^ (self#memref_to_string memref) ^ " is allowed to leave local scope" in Some (deps, msg) - | CBaseVar v -> self#var_implies_safe invindex v + | CBaseVar (v, _) -> self#var_implies_safe invindex v | _ -> None end else @@ -144,14 +144,14 @@ object (self) let _ = poq#set_diagnostic_arg 2 (self#memref_to_string memref) in begin match memref#get_base with - | CBaseVar v when poq#is_api_expression (XVar v) -> + | CBaseVar (v, _) when poq#is_api_expression (XVar v) -> let deps = DLocal [inv#index] in let msg = "address " ^ (x2s (XVar v)) ^ " received from caller is returned to caller" in Some (deps,msg) - | CBaseVar v -> self#var_implies_safe inv#index v + | CBaseVar (v, _) -> self#var_implies_safe inv#index v | CStringLiteral _ -> let deps = DLocal [inv#index] in let msg = @@ -237,7 +237,7 @@ object (self) ^ (self#memref_to_string memref) ^ " should not leave scope" in Some (deps,msg) - | CBaseVar v -> self#xpr_implies_violation invindex (XVar v) + | CBaseVar (v, _) -> self#xpr_implies_violation invindex (XVar v) | _ -> None end | XOp (_, [xbase; _xinc]) -> self#xpr_implies_violation invindex xbase diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckUpperBound.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckUpperBound.ml index f754f58f..429d3e21 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckUpperBound.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckUpperBound.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - Copyright (c) 2024 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,7 +88,7 @@ object (self) let (vinfo,_offset) = poq#env#get_local_variable svar in let msg = "address of stack variable: " ^ vinfo.vname in Some (deps, msg) - | CBaseVar svar -> + | CBaseVar (svar, _) -> let msg = "address of externally provided variable/field: " ^ svar#getName#getBaseName in @@ -181,21 +181,6 @@ object (self) | Some l -> self#xprlist_implies_safe inv#index l method check_safe = - let safemsg = fun index arg_count -> ("command-line argument" - ^ (string_of_int index) - ^ " is guaranteed to be valid to access" - ^ " for argument count " - ^ (string_of_int arg_count)) in - let vmsg = fun index arg_count -> ("command-line argument " - ^ (string_of_int index) - ^ " is not included in argument count of " - ^ (string_of_int arg_count)) in - let dmsg = fun index -> ("no invariant found for argument count; " - ^ "unable to validate access of " - ^ "command-line argument " - ^ (string_of_int index)) in - - poq#check_command_line_argument e safemsg vmsg dmsg || match invs with | [] -> begin diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckValidMem.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckValidMem.ml index 8584e4f7..94ff7eaa 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckValidMem.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckValidMem.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - Copyright (c) 2024 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 @@ -216,7 +216,7 @@ object (self) | CStringLiteral _ -> let msg = "address of string literal" in Some (deps,msg) - | CBaseVar v -> self#var_implies_safe invindex v + | CBaseVar (v, _) -> self#var_implies_safe invindex v | _ -> None method private call_preserves_validity_excludes @@ -330,17 +330,25 @@ object (self) method private initial_value_implies_safe (invindex: int) (v: variable_t) = if poq#env#is_initial_parameter_value v then - let vv = poq#env#get_initial_value_variable v in - let deps = DLocal [invindex] in - let msg = "initial value of argument: " ^ vv#getName#getBaseName in - let _ = - poq#set_diagnostic_arg 1 ("initial value of " ^ (p2s (vv#toPretty))) in - match self#validity_maintenance v poq#env#get_fn_entry_call_var with - | Some (d, m) -> - let deps = join_dependencies deps d in - let msg = msg ^ "; " ^ m in - Some (deps, msg) - | _ -> None + let (vinfo, _) = poq#env#get_initial_parameter_vinfo v in + let vtype = + CCHFileEnvironment.file_environment#get_type_unrolled vinfo.vtype in + if CCHTypesUtil.has_deref_const_attribute vtype then + let deps = DLocal [invindex] in + let msg = "function parameter " ^ vinfo.vname ^ " is a const parameter" in + Some (deps, msg) + else + let vv = poq#env#get_initial_value_variable v in + let deps = DLocal [invindex] in + let msg = "initial value of argument: " ^ vv#getName#getBaseName in + let _ = + poq#set_diagnostic_arg 1 ("initial value of " ^ (p2s (vv#toPretty))) in + match self#validity_maintenance v poq#env#get_fn_entry_call_var with + | Some (d, m) -> + let deps = join_dependencies deps d in + let msg = msg ^ "; " ^ m in + Some (deps, msg) + | _ -> None else if poq#is_global_expression (XVar v) then match self#global_implies_safe invindex (poq#get_global_expression (XVar v)) with @@ -359,7 +367,7 @@ object (self) if poq#env#is_memory_variable vv then let (memref, offset) = poq#env#get_memory_variable vv in match memref#get_base with - | CBaseVar v -> + | CBaseVar (v, _) -> begin poq#set_diagnostic_arg 1 @@ -447,22 +455,7 @@ object (self) r method check_safe = - let safemsg = fun index arg_count -> ("command-line argument" - ^ (string_of_int index) - ^ " is guaranteed to have valid memory" - ^ " for argument count " - ^ (string_of_int arg_count)) in - let vmsg = fun index arg_count -> ("command-line argument " - ^ (string_of_int index) - ^ " is not included in argument count of " - ^ (string_of_int arg_count)) in - let dmsg = fun index -> ("no invariant found for argument count; " - ^ "unable to validate memory validity of " - ^ "command-line argument " - ^ (string_of_int index)) in - - poq#check_command_line_argument e safemsg vmsg dmsg - || self#global_free + self#global_free || (match invs with | [] -> false | _ -> @@ -505,7 +498,7 @@ object (self) if poq#env#is_memory_variable vi then let (memref, offset) = poq#env#get_memory_variable vi in match memref#get_base with - | CBaseVar bv when poq#is_api_expression (XVar bv) -> + | CBaseVar (bv, _) when poq#is_api_expression (XVar bv) -> let a = poq#get_api_expression (XVar bv) in let pred = PValidMem (Lval (Mem a, offset)) in let deps = DEnvC ([invindex], [ApiAssumption pred]) in @@ -540,6 +533,31 @@ object (self) match inv#lower_bound_xpr with | Some x -> self#xpr_implies_delegation inv#index x | _ -> None in + let r = + match r with + | Some _ -> r + | _ -> + match inv#expr with + | Some (XVar v) when + poq#env#is_mut_memory_address v || poq#env#is_ref_memory_address v -> + begin + (match poq#x2api (XVar v) with + | Some a1 when poq#is_api_expression (XVar v) -> + let pred = PValidMem a1 in + let deps = DEnvC ([inv#index], [ApiAssumption pred]) in + let msg = + "exclusive reference " ^ (p2s v#toPretty) + ^ "; condition " ^ (p2s (po_predicate_to_pretty pred)) + ^ " delegated to the api" in + let site = Some (__FILE__, __LINE__, "inv_implies_delegation") in + Some (deps, msg, site) + | _ -> + begin + poq#set_diagnostic ("exclusive reference: " ^ (p2s v#toPretty)); + None + end) + end + | _ -> None in r method check_delegation = diff --git a/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml b/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml index df5f4854..aba0464a 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2022 Henny Sipma - Copyright (c) 2023-2024 Aarno Labs LLC + Copyright (c) 2023-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 @@ -38,6 +38,7 @@ open CHPrettyUtil open CHXmlDocument (* xprlib *) +open Xconsequence open Xprt open XprTypes open XprToPretty @@ -68,6 +69,7 @@ open CCHProofScaffolding open CCHAnalysisTypes open CCHCheckImplication open CCHExpTranslator +open CCHNumericalConstraints open CCHOrakel let x2p = xpr_formatter#pr_expr @@ -284,25 +286,384 @@ object (self) else None + method private has_api_assumptions (deps: dependencies_t): bool = + match deps with + | DEnvC (_, l) -> + List.exists (fun a -> + match a with | ApiAssumption _ -> true | _ -> false) l + | _ -> false + + method private get_main_argc_invariants (argcvar: variable_t) = + if fname = "main" then + let locinvio = invio#get_location_invariant cfgcontext in + let facts = List.concat (List.map locinvio#get_var_invariants [argcvar]) in + let _ = + log_diagnostics_result + ~tag:"get_main_argc_invariants" + __FILE__ __LINE__ + [String.concat "; " (List.map (fun f -> p2s f#toPretty) facts)] in + facts + else + [] + + (* Handling of assumptions delegated to the api of the main function. + + Regular functions can delegate (part of) proof obligations to assumptions + on the arguments to that function, to be satisfied by the callers of that + function. The main function, however, has no callers, and thus assumptions + delegated cannot be propagated and thus are never checked in this way. + The assumptions on main can only be checked against the C standard, that is, + the C standard provides the only guarantees that can be assumed for the + arguments of main. + + Section 5.1.2.2.1 Program startup of the C99 standard imposes the following + requirements on the first two arguments of main (referred to here as argc + and argv) (if they are declared): + - The value of argc shall be nonnegative. + - If the value of argc is greater than zero, the array members argv[0] + through argv[argc-1] inclusive shall contain pointers to string, which + are given implementation-defined values by the host environement prior + to program startup. + - If the value of argc is greater than zero, the string pointed to by + argv[0] represents the program name; argv[0][0] shall the be null + character if the program name is not available from the host environment. + If the value of argc is greater than one, the strings pointed to by + argv[1] through argv[argc-1] represent the program parameters. + - The parameters argc and argv and the strings pointed to by the argv + array shall be modifiable by the program, and retain their last-stored + values between program startup and program termination. + + These requirements are checked by intercepting the recording of proof + results for main and checking whether any assumptions delegated to the + function api are implied by the guarantees described in the C standard. + It is checked whether the api assumptions made indeed concern (the + initial value of) argv, and, if applicable, which member of the array + pointed at by argv. Furthermore it is checked that the index into the + array is less than (or sometimes equal to) the initial value of argc. + + The following predicate kinds can be discharged against the C standard + assumptions: + - not-null(argv): valid: argv is guaranteed non-null + - not-null(argv[i]): valid if i < argc + - initialized(argv[i]): valid if i <= argc + - null-terminated(argv[i]): valid if i < argc + - initialized-range(argv[i]): valid if i < argc + - valid-mem(argv[i]): valid if i < argc + - ptr-upper-bound-deref(argv, i, _, _): valid if i <= argc + - ptr-upper-bound(argv[i], null-terminator-position(argv[i], _, _): + (the pointer in argv[i] can safely be incremented with the index + of the null-terminator position): valid if i < argc + + If an assumption is determined to be implied by the guarantees provided + by the standard, the status of the proof obligation is changed from + A (delegated to api) to L (local). If an assumption cannot be proven to + be implied by the guarantees, the status of the proof obligation is + changed from A to ? (open), indicating that the proof obligation has not + been discharged and is potentially a violation. + + Note that the interception only happens if argv/argv[i] has already + been shown to be equal to the initial value at function entry. If the + value has been changed (as is allowed according to the C standard), + discharge follows the same procedure as for other variables. + *) + method private record_main_api_proof_result + ?(site: (string * int * string) option = None) + (status:po_status_t) + (deps:dependencies_t) + (expl:string) = + let line = match site with Some (_, l, _) -> l | _ -> -1 in + let is_argv (vid: int): bool = + fenv#is_formal vid && (self#env#get_varinfo vid).vparam = 2 in + let _argc_invs = self#get_main_argc_invariants in + let is_argv_array_member_location (lval: lval): bool = + match lval with + | (Mem (Lval (Var (_, vid), NoOffset)), NoOffset) + | (Mem (Lval (Var (_, vid), NoOffset)), Index _) -> is_argv vid + | (Mem e, offset) -> + let _ = + log_diagnostics_result + ~tag:"record_main_api_proof_result:unmatched" + __FILE__ __LINE__ + ["e: " ^ (p2s (exp_to_pretty e)); + "offset: " ^ (p2s (offset_to_pretty offset))] in + false + | _ -> false in + let is_argv_array_member (e: exp): bool = + match e with + | Lval lval -> is_argv_array_member_location lval + | _ -> false in + let get_argv_array_member_index (e: exp): int option = + match e with + | Lval (Mem _, Index (Const (CInt (i64, _, _)), NoOffset)) -> + Some (Int64.to_int i64) + | _ -> None in + let (invs, assumptions) = + match deps with + | DEnvC (invs, al) -> (invs, al) + | _ -> ([], []) in + let assumptions = + List.fold_left (fun acc a -> + match a with + | ApiAssumption p -> p :: acc + | _ -> acc) [] assumptions in + let _ = + log_diagnostics_result + ~tag:"record_main_api_proof_result" + __FILE__ __LINE__ + [(string_of_int line); + " "; + String.concat + "; " + (List.map (fun a -> (p2s (po_predicate_to_pretty a))) assumptions)] in + let (ldeps, expls, predicates') = + List.fold_left (fun (ldeps, expls, preds) p -> + let predicate_msg () = + match p with + | PNotNull _ -> "is guaranteed to be non-null" + | PValidMem _ -> "is guaranteed to be valid memory" + | PUpperBound _ -> + "is guaranteed to not exceed to upper bound of the buffer pointed at" + | PLowerBound _ -> + "is guaranteed to not go below the lower bound of the buffer pointed at" + | PInScope _ -> + "is guaranteed to be in scope" + | PInitializedRange _ -> + "is guaranteed to point at a buffer that is initialized up to its " + ^ "null terminator" + | PNullTerminated _ -> + "is guaranteed to point at a buffer that is null terminated" + | PPtrUpperBound _ | PPtrUpperBoundDeref _ -> + "allows for incrementing the pointer up to the null terminator" + | _ -> "?" in + + match p with + | PNotNull (Lval (Var (_, vid), NoOffset)) when is_argv vid -> + (ldeps, "the initial value of argv is guaranteed not null" :: expls, preds) + | PNotNull e + | PValidMem e + | PUpperBound (_, e) + | PLowerBound (_, e) + | PInScope e + | PInitializedRange (e, _) + | PNullTerminated e when is_argv_array_member e -> + (match get_argv_array_member_index e with + | Some index -> + (match self#is_valid_argv_index index with + | Some (ideps, imsg) -> + ((ideps @ ldeps, + ("the value of argv[" ^ (string_of_int index) ^ "] " ^ + (predicate_msg ())) :: imsg :: expls, preds)) + | _ -> + (ldeps, expls, p :: preds)) + | _ -> + (ldeps, expls, p :: preds)) + + | PPtrUpperBound (_, _, e, CnApp ("ntp", [Some len], _)) + | PPtrUpperBoundDeref (_, _, e, CnApp ("ntp", [Some len], _)) + when (exp_compare e len) = 0 -> + (match get_argv_array_member_index e with + | Some index -> + (match self#is_valid_argv_index index with + | Some (ideps, imsg) -> + ((ideps @ ldeps, + ("the value of argv[" ^ (string_of_int index) ^ "] " ^ + (predicate_msg ())) :: imsg :: expls, preds)) + | _ -> + (ldeps, expls, p :: preds)) + | _ -> + (ldeps, expls, p :: preds)) + + | PPtrUpperBoundDeref (_, + IndexPI, + Lval (Var (_, vid), NoOffset), + Const (CInt (i64, _, _))) when is_argv vid -> + let index = Int64.to_int i64 in + (match self#is_valid_argv_index index with + | Some (ideps, imsg) -> + ((ideps @ ldeps, + ("the value of argv stays within bounds when incremented by " + ^ (string_of_int index)) :: imsg :: expls, preds)) + | _ -> + begin + self#set_diagnostic + ("Unable to prove that increment of " ^ (string_of_int index) + ^ " is safe"); + (ldeps, expls, p :: preds) + end) + + | PInitialized lval when is_argv_array_member_location lval -> + (match get_argv_array_member_index (Lval lval) with + | Some index -> + (match self#is_valid_argv_index ~strict:false index with + | Some (ideps, imsg) -> + ((ideps @ ldeps, + ("the value of argv[" ^ (string_of_int index) ^ "] " ^ + "is guaranteed to be initialized") :: imsg :: expls, preds)) + | _ -> + (ldeps, expls, p :: preds)) + | _ -> + (ldeps, expls, p :: preds)) + | _ -> + (ldeps, expls, p :: preds)) ([], [], []) assumptions in + if (List.length predicates') = 0 then + let deps' = DLocal (invs @ ldeps) in + let expl' = (String.concat "; " expls) ^ "; " ^ expl in + self#record_proof_result ~site status deps' expl' + else + begin + log_diagnostics_result + ~tag:"record_main_api_proof_result:rejected" + __FILE__ __LINE__ + ["assumptions: " ^ + (String.concat ", " + (List.map (fun a -> (p2s (po_predicate_to_pretty a))) assumptions))]; + self#set_diagnostic + ("Unable to discharge all assumptions made against the api of main: " + ^ (String.concat + ", " (List.map (fun p -> p2s (po_predicate_to_pretty p)) predicates'))); + po#set_status Orange; + po#set_dependencies deps; + po#set_explanation ~site expl; + po#set_resolution_timestamp (current_time_to_string ()); + (match proof_scaffolding#record_proof_obligation_result self#fname po with + | Ok _ -> () + | Error e -> + raise + (CCHFailure + (LBLOCK [ + STR "Error in record-proof-result: "; + STR (String.concat "; " e)]))) + end + + (* Checks the value of the index into the array pointed at by argv against + the initial value of argc. *) + method private is_valid_argv_index + ?(strict=true) (index: int): (int list * string) option = + let argc = fenv#get_formal 1 in + let argcvar = self#env#mk_program_var argc NoOffset NUM_VAR_TYPE in + let argcinit = self#env#mk_initial_value argcvar (TInt (IInt, [])) NUM_VAR_TYPE in + let indexxpr = + if strict then + simplify_xpr (XOp (XPlus, [int_constant_expr index; one_constant_expr])) + else + int_constant_expr index in + let consequence = simplify_xpr (XOp (XMinus, [indexxpr; XVar argcinit])) in + let msg = + "property argc#init" + ^ (if strict then " > " else " >= ") + ^ "index for index = " ^ (string_of_int index) + ^ " implied by " in + let facts = self#get_main_argc_invariants argcvar in + let _ = + po#set_diagnostic_invariants 0 (List.map (fun f -> f#index) facts) in + let invxprs = + List.fold_left (fun acc inv -> + match inv#expr with + | Some x -> XOp (XEq, [XVar argcvar; x]) :: acc + | _ -> acc) [] facts in + let numconstraints = + List.fold_left (fun acc x -> + match xpr_to_numconstraint x with + | Some c -> c :: acc + | _ -> acc) [] invxprs in + let constraintset = mk_constraint_set () in + let _ = List.iter constraintset#add numconstraints in + let newconstraintset = constraintset#project_out [argcvar] in + match newconstraintset with + | Some cs -> + let newconstraints = cs#get_constraints in + let cxprs = List.map numconstraint_to_xpr newconstraints in + let cxprs = List.map simplify_xpr cxprs in + let _ = + log_diagnostics_result + ~tag:"is_valid_argv_index" + __FILE__ __LINE__ + ["constraints: " + ^ (String.concat ", " (List.map (fun c -> p2s c#toPretty) newconstraints)); + "xprs: " ^ (String.concat ", " (List.map x2s cxprs)); + "index: " ^ (string_of_int index)] in + let antecedents = + List.fold_left (fun acc a -> + match a with + | XOp (XEq, [a; b]) -> + (XOp (XMinus, [a; b])) :: (XOp (XMinus, [b; a])) :: acc + | _ -> acc) [] cxprs in + let implication = + List.fold_left (fun acc a -> + acc || (xfimplies a consequence)) false antecedents in + if implication then + Some (List.map (fun f -> f#index) facts, msg ^ " invariants") + + else + begin + log_diagnostics_result + ~tag:"is_valid_argv_index:no-implication" + __FILE__ __LINE__ + ["indexxpr: " ^ (x2s indexxpr); + "consequence: " ^ (x2s consequence); + "antecedents: " ^ (String.concat ", " (List.map x2s antecedents))]; + self#set_diagnostic + ("Unable to prove index < argc#init for index = " ^ (string_of_int index)); + None + end + | _ -> + let parameterconstraints = self#get_parameter_constraints in + let antecedents = + List.fold_left + (fun acc p -> + match p with + | XOp (XGe, [a; b]) -> + (simplify_xpr (XOp (XMinus, [b; a]))) :: acc + | XOp (XEq, [a; b]) -> + (simplify_xpr (XOp (XMinus, [a; b]))) :: + (simplify_xpr (XOp (XMinus, [b; a]))) :: acc + | _ -> acc) [] parameterconstraints in + let implication = + List.fold_left (fun acc a -> + acc || (xfimplies a consequence)) false antecedents in + if implication then + Some ([], msg + ^ " parameter constraint(s) " + ^ (String.concat ", " (List.map x2s parameterconstraints))) + else + begin + log_diagnostics_result + ~tag:"is_valid_argv_index:no-constraintset/no parameterconstraints" + __FILE__ __LINE__ + ["invxprs: " ^ (String.concat ", " (List.map x2s invxprs)); + "parameter constraints: " + ^ (String.concat ", " (List.map x2s parameterconstraints))]; + self#set_diagnostic "Unable to prove index < argc#init"; + None + end + method private record_proof_result ?(site: (string * int * string) option = None) (status:po_status_t) (deps:dependencies_t) (expl:string) = - begin - po#set_status status; - po#set_dependencies deps; - po#set_explanation ~site expl; - po#set_resolution_timestamp (current_time_to_string ()); - (match proof_scaffolding#record_proof_obligation_result self#fname po with - | Ok _ -> () - | Error e -> - raise - (CCHFailure - (LBLOCK [ - STR "Error in record-proof-result: "; - STR (String.concat "; " e)]))) - end + if self#env#get_functionname = "main" + && (match (status, deps) with + | (Green, DEnvC (_, al)) -> + List.exists (fun a -> + match a with ApiAssumption _ -> true | _ -> false) al + | _ -> false) then + self#record_main_api_proof_result ~site status deps expl + else + begin + po#set_status status; + po#set_dependencies deps; + po#set_explanation ~site expl; + po#set_resolution_timestamp (current_time_to_string ()); + (match proof_scaffolding#record_proof_obligation_result self#fname po with + | Ok _ -> () + | Error e -> + raise + (CCHFailure + (LBLOCK [ + STR "Error in record-proof-result: "; + STR (String.concat "; " e)]))) + end method set_diagnostic ?(site: (string * int * string) option = None) @@ -393,7 +754,7 @@ object (self) if self#env#is_memory_variable v then let (memref, memoffset) = self#env#get_memory_variable v in (match memref#get_base with - | CBaseVar base when self#env#is_initial_parameter_value base -> + | CBaseVar (base, _) when self#env#is_initial_parameter_value base -> let basevar = self#env#get_initial_value_variable base in if numv#equal basevar && (offset_compare offset memoffset) = 0 then @@ -521,6 +882,10 @@ object (self) | NonRelationalFact (v, _) when env#is_call_var v -> inv :: acc | _ -> acc) [] invs + method get_var_invariants (var: variable_t): invariant_int list = + let locinvio = invio#get_location_invariant cfgcontext in + locinvio#get_var_invariants var + method get_invariants (argindex: int): invariant_int list = let id = po#index in let locinvio = invio#get_location_invariant cfgcontext in @@ -1019,7 +1384,7 @@ object (self) ^ (p2s (offset_to_pretty offset))) in None end - | CBaseVar v -> + | CBaseVar (v, _) -> begin self#set_diagnostic_arg arg ("basevar: " ^ v#getName#getBaseName); self#xpr_buffer_offset_size arg invindex (XVar v) @@ -1196,6 +1561,19 @@ object (self) self#record_unevaluated x; None end) + | XVar v when Option.is_some (env#get_memory_address_wrapped_value v) -> + (match env#get_memory_address_wrapped_value v with + | Some wv -> + (try Some (env#get_parameter_exp wv) with + | CCHFailure p -> + begin + chlog#add + "api expression" + (LBLOCK [STR env#get_functionname; STR ": "; p]); + self#record_unevaluated x; + None + end) + | _ -> None) | XOp (op, [x1; x2]) -> begin match (self#x2api x1, self#x2api x2) with @@ -1433,99 +1811,6 @@ object (self) with | Failure _ -> None - method is_command_line_argument (e:exp) = - fname = "main" && - match e with - | CastE (_,ee) -> self#is_command_line_argument ee - | Lval (Mem (BinOp - ((PlusPI | IndexPI), - Lval (Var (_, vid), NoOffset), - Const (CInt (_i64, _, _)), _)), - NoOffset) when vid > 0 -> - fenv#is_formal vid && (self#env#get_varinfo vid).vparam = 2 - | _ -> false - - method get_command_line_argument_index (e:exp) = - if self#is_command_line_argument e then - match e with - | CastE (_, ee) -> self#get_command_line_argument_index ee - | Lval (Mem (BinOp - ((PlusPI | IndexPI), - Lval (Var (_, _vid), NoOffset), - Const (CInt (i64, _, _)), _)), NoOffset) -> - Int64.to_int i64 - | _ -> - raise - (CCHFailure - (LBLOCK [STR "Internal error in get_command_line_argument_index"])) - else - raise - (CCHFailure - (LBLOCK [ - STR "expression "; - exp_to_pretty e; - STR " is not a command-line argument"])) - - method get_command_line_argument_count: (int * int) option = - if fname = "main" then - let locinvio = invio#get_location_invariant cfgcontext in - let argc = fenv#get_formal 1 in - let argcvar = self#env#mk_program_var argc NoOffset NUM_VAR_TYPE in - let facts = List.concat (List.map locinvio#get_var_invariants [argcvar]) in - let facts = - List.fold_left (fun acc f -> - match f#get_fact with - | NonRelationalFact (_v, i) -> (f#index, i) :: acc - | _ -> acc) [] facts in - List.fold_left (fun acc (inv, i) -> - match acc with - | Some _ -> acc - | _ -> - match i with - | FIntervalValue (Some lb, Some ub) when lb#equal ub -> - begin - try - Some (inv,lb#toInt) - with - _ -> - begin - chlog#add - "large value" - (LBLOCK [STR self#fname; STR ": "; lb#toPretty]); - None - end - end - | _ -> acc) None facts - else - None - - method check_command_line_argument - (e:exp) - (safemsg:int -> int -> string) - (vmsg:int -> int -> string) - (dmsg:int -> string): bool = - if self#is_command_line_argument e then - let index = self#get_command_line_argument_index e in - match self#get_command_line_argument_count with - | Some (inv, i) -> - if index < i then - begin - self#record_safe_result (DLocal [inv]) (safemsg index i); - true - end - else - begin - self#record_violation_result (DLocal [inv]) (vmsg index i); - true - end - | _ -> - begin - self#set_diagnostic (dmsg index); - false - end - else - false - method check_implied_by_assumptions (p:po_predicate_t) = let assumptions = List.map (fun a -> a#get_predicate) self#get_api_assumptions in diff --git a/CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml b/CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml index 30ff2ecc..99f04512 100644 --- a/CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml +++ b/CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml @@ -69,6 +69,10 @@ let cmds = [ let cmdchoices = String.concat ", " cmds +let iteration_index = ref 0 + +let set_iteration (index: int) = iteration_index := index + let cmd = ref "version" let setcmd s = if List.mem s cmds then @@ -119,6 +123,7 @@ let speclist = [ ("-domains", Arg.String set_domains, "domains to be used in invariant generation: " ^ "[l:lineq; v:valuesets; i:intervals; s:symbolicsets]"); + ("-iteration", Arg.Int set_iteration, "iteration index"); ("-cfilename", Arg.String system_settings#set_cfilename, "base filename of c source code file without extension"); ("-cfilepath", Arg.String system_settings#set_cfilepath, @@ -148,12 +153,13 @@ let read_args () = Arg.parse speclist system_settings#set_targetpath usage_msg let save_log_files (contenttype:string) = + let index = "_" ^ (string_of_int !iteration_index) in begin - save_logfile ch_info_log contenttype "infolog"; - append_to_logfile ch_error_log contenttype "errorlog"; - save_logfile chlog contenttype "chlog"; + save_logfile ch_info_log contenttype ("infolog" ^ index); + append_to_logfile ch_error_log contenttype ("errorlog" ^ index); + save_logfile chlog contenttype ("chlog" ^ index); (if collect_diagnostics () then - save_logfile ch_diagnostics_log contenttype "ch_diagnostics_log") + save_logfile ch_diagnostics_log contenttype ("ch_diagnostics_log" ^ index)) end diff --git a/CodeHawk/CHC/cchlib/cCHTypesUtil.ml b/CodeHawk/CHC/cchlib/cCHTypesUtil.ml index 70bd3d07..25ea0b22 100644 --- a/CodeHawk/CHC/cchlib/cCHTypesUtil.ml +++ b/CodeHawk/CHC/cchlib/cCHTypesUtil.ml @@ -174,6 +174,11 @@ let minval w = (mkNumerical_big v)#neg +let mk_constant_index_offset (n: numerical_t): offset = + let i64 = Int64.of_string n#toString in + Index (Const (CInt (i64, IInt, None)), NoOffset) + + let rec is_field_offset offset = match offset with | NoOffset -> false diff --git a/CodeHawk/CHC/cchlib/cCHTypesUtil.mli b/CodeHawk/CHC/cchlib/cCHTypesUtil.mli index 09112618..62b3b314 100644 --- a/CodeHawk/CHC/cchlib/cCHTypesUtil.mli +++ b/CodeHawk/CHC/cchlib/cCHTypesUtil.mli @@ -74,6 +74,8 @@ val float_fits_kind: float -> fkind -> bool val enum_fits_kind: string -> ikind -> bool +val get_typ_attributes: typ -> attribute list + val has_const_attribute: typ -> bool val has_deref_const_attribute: typ -> bool @@ -132,6 +134,8 @@ val is_constant_string: exp -> bool val is_enum_constant: string -> exp -> bool +val mk_constant_index_offset: numerical_t -> offset + val get_field_offset: offset -> string * int val get_scalar_struct_offsets: typ -> offset list diff --git a/CodeHawk/CHC/cchlib/cCHVersion.ml b/CodeHawk/CHC/cchlib/cCHVersion.ml index cd8c390f..324c3060 100644 --- a/CodeHawk/CHC/cchlib/cCHVersion.ml +++ b/CodeHawk/CHC/cchlib/cCHVersion.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2024 Henny B. Sipma - 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 @@ -62,5 +62,5 @@ object (self) end let version = new version_info_t - ~version:"0.3.0_20260130" - ~date:"2026-01-30" + ~version:"0.3.0_20260223" + ~date:"2026-02-23" diff --git a/CodeHawk/CHC/cchpre/cCHCheckValid.ml b/CodeHawk/CHC/cchpre/cCHCheckValid.ml index 53bff48f..10250430 100644 --- a/CodeHawk/CHC/cchpre/cCHCheckValid.ml +++ b/CodeHawk/CHC/cchpre/cCHCheckValid.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2022 Henny Sipma - Copyright (c) 2023-2025 Aarno Labs LLC + Copyright (c) 2023-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 @@ -573,24 +573,6 @@ let check_ppo_validity let set_diagnostic = ppo#add_diagnostic_msg in - let is_argv (vid:int) = - vid > 0 - && fname = "main" - && env#is_formal vid - && (get_varinfo vid).vparam = 2 in - - let rec is_program_name (e:exp) = - fname = "main" && - (match e with - | CastE (_, ee) -> is_program_name ee - | Lval (Mem (BinOp - ((PlusPI | IndexPI), - Lval (Var (_, vid), NoOffset), - Const (CInt (i64, _, _)), _)), - NoOffset) -> - is_argv vid && (get_varinfo vid).vparam = 2 && (Int64.to_int i64) = 0 - | _ -> false) in - let make_record status mth explanation = begin ppo#set_status status; @@ -629,14 +611,6 @@ let check_ppo_validity | _ -> () end - | PNotNull e when is_program_name e -> - make - ("pointer to program name is guaranteed not null by operating system") - - | PNotNull (Lval (Var (_vname, vid), NoOffset)) when is_argv vid -> - make - ("second argument to main is guaranteed not-null by the operating system") - | PNotNull (AddrOf (Var v,_)) | PNotNull (StartOf (Var v,_)) | PNotNull (CastE (_,AddrOf (Var v,_))) @@ -709,11 +683,6 @@ let check_ppo_validity NoOffset))) -> make ("library variable " ^ vname ^ " is valid") - | PValidMem e when is_program_name e -> - make - ("validity of pointer to program name is guaranteed by the " - ^ "operating system") - | PValidMem e when is_null_pointer e -> make "null pointer" @@ -1562,11 +1531,6 @@ let check_ppo_validity | _ -> () end - | PPtrUpperBound (_, _, e, _) when is_program_name e -> - make - ("validity of pointer to program name is guaranteed by the " - ^ "operating system") - | PPtrUpperBound (_, _, e, _) when is_null_pointer e -> make ("not-null of first argument is checked separately") @@ -1786,11 +1750,6 @@ let check_ppo_validity | _ -> () end - | PLowerBound (_, e) when is_program_name e -> - make - ("validity of pointer to program name is guaranteed by the " - ^ "operating system") - | PLowerBound (_, Const (CStr _)) | PLowerBound (_, CastE (_, Const (CStr _))) -> make "constant string is allocated by compiler" @@ -1862,11 +1821,6 @@ let check_ppo_validity NoOffset))) -> make ("library variable " ^ vname ^ " satisfies upper bound") - | PUpperBound (_,e) when is_program_name e -> - make - ("validity of pointer to program name is guaranteed by the " - ^ "operating system") - | PUpperBound (_, Const (CStr _)) | PUpperBound (_, CastE (_, Const (CStr _))) -> make "constant string is allocated by compiler" @@ -2119,11 +2073,6 @@ let check_ppo_validity | PInitialized (Mem e, NoOffset) when is_constant_string e -> make ("constant string is guaranteed to have at least one character") - | PInitializedRange (e, _) when is_program_name e -> - make - ("validity of pointer to program name is guaranteed by the " - ^ "operating system") - | PInitializedRange (e, _) when is_null_pointer e -> make "null pointer does have any range, so this is trivially valid" @@ -2212,11 +2161,6 @@ let check_ppo_validity | PNullTerminated (Const (CWStr _)) | PNullTerminated (CastE (_, Const (CWStr _))) -> make "wide string literal" - | PNullTerminated e when is_program_name e -> - make - ("validity of pointer to program name is guaranteed by the " - ^ "operating system") - | PNullTerminated e when is_null_pointer e -> make "null pointer is not subject to null-termination" diff --git a/CodeHawk/CHC/cchpre/cCHInvariantFact.ml b/CodeHawk/CHC/cchpre/cCHInvariantFact.ml index d5172b5d..c95367c6 100644 --- a/CodeHawk/CHC/cchpre/cCHInvariantFact.ml +++ b/CodeHawk/CHC/cchpre/cCHInvariantFact.ml @@ -621,7 +621,13 @@ object (self) else inv :: entry in H.replace table vindex newentry - | _ -> () + | _ -> + let _ = + log_diagnostics_result + ~tag:"integrate_fact:ignored" + __FILE__ __LINE__ + [p2s inv#toPretty] in + () method write_xml (node:xml_element_int) = let invs = List.sort Stdlib.compare (H.fold (fun k _ a -> k::a) facts []) in diff --git a/CodeHawk/CHC/cchpre/cCHMemoryBase.ml b/CodeHawk/CHC/cchpre/cCHMemoryBase.ml index 7fa97b7f..99422adf 100644 --- a/CodeHawk/CHC/cchpre/cCHMemoryBase.ml +++ b/CodeHawk/CHC/cchpre/cCHMemoryBase.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2024 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 @@ -28,33 +28,14 @@ ============================================================================= *) (* chlib *) +open CHLanguage open CHPretty (* cchpre *) open CCHPreTypes -let memory_base_compare (b1:memory_base_t) (b2:memory_base_t) = - match (b1,b2) with - | (CNull i1, CNull i2) -> Stdlib.compare i1 i2 - | (CNull _, _) -> -1 - | (_, CNull _) -> 1 - | (CStringLiteral i1, CStringLiteral i2) -> Stdlib.compare i1 i2 - | (CStringLiteral _, _) -> -1 - | (_, CStringLiteral _) -> 1 - | (CStackAddress v1, CStackAddress v2) -> - Stdlib.compare v1#getName#getSeqNumber v2#getName#getSeqNumber - | (CStackAddress _, _) -> -1 - | (_, CStackAddress _) -> 1 - | (CGlobalAddress v1, CGlobalAddress v2) -> - Stdlib.compare v1#getName#getSeqNumber v2#getName#getSeqNumber - | (CGlobalAddress _, _) -> -1 - | (_, CGlobalAddress _) -> 1 - | (CBaseVar v1, CBaseVar v2) -> - Stdlib.compare v1#getName#getSeqNumber v2#getName#getSeqNumber - | (CBaseVar _,_) -> -1 - | (_, CBaseVar _) -> 1 - | (CUninterpreted s1, CUninterpreted s2) -> Stdlib.compare s1 s2 +let p2s = CHPrettyUtil.pretty_to_string let memory_base_to_string (b:memory_base_t) = @@ -67,8 +48,14 @@ let memory_base_to_string (b:memory_base_t) = ^ v#getName#getBaseName ^ "_" ^ (string_of_int v#getName#getSeqNumber) + ^ "_" + ^ (p2s (variable_type_to_pretty v#getType)) | CGlobalAddress v -> "addrof_globalvar_" ^ v#getName#getBaseName - | CBaseVar v -> "addr_in_" ^ v#getName#getBaseName + | CBaseVar (v, nullattr) -> + "addr_in_" + ^ v#getName#getBaseName + ^ "_" + ^ (match nullattr with NotNull -> "notnull" | _ -> "") | CUninterpreted s -> "uninterpreted_" ^ s diff --git a/CodeHawk/CHC/cchpre/cCHMemoryBase.mli b/CodeHawk/CHC/cchpre/cCHMemoryBase.mli index 829c76b5..6d2a4f51 100644 --- a/CodeHawk/CHC/cchpre/cCHMemoryBase.mli +++ b/CodeHawk/CHC/cchpre/cCHMemoryBase.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2023 Henny B. Sipma - Copyright (c) 2024 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 @@ -34,8 +34,6 @@ open CHPretty open CCHPreTypes -val memory_base_compare: memory_base_t -> memory_base_t -> int - val memory_base_to_string: memory_base_t -> string val memory_base_to_pretty: memory_base_t -> pretty_t diff --git a/CodeHawk/CHC/cchpre/cCHMemoryReference.ml b/CodeHawk/CHC/cchpre/cCHMemoryReference.ml index afc7ad7c..20db685c 100644 --- a/CodeHawk/CHC/cchpre/cCHMemoryReference.ml +++ b/CodeHawk/CHC/cchpre/cCHMemoryReference.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2024 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 @@ -32,10 +32,12 @@ open CHLanguage open CHPretty (* chutil *) +open CHLogger open CHXmlDocument (* cchlib *) open CCHBasicTypes +open CCHTypesToPretty open CCHUtilities (* cchpre *) @@ -45,6 +47,13 @@ open CCHMemoryBase module H = Hashtbl +let p2s = CHPrettyUtil.pretty_to_string + + +let memory_reference_data_to_pretty (d: memory_reference_data_t) = + LBLOCK [memory_base_to_pretty d.memrefbase; STR "; "; typ_to_pretty d.memreftype] + + class memory_reference_t ~(vard:vardictionary_int) ~(index:int) @@ -74,7 +83,7 @@ object (self:'a) match data.memrefbase with | CStackAddress v | CGlobalAddress v - | CBaseVar v -> v + | CBaseVar (v, _) -> v | _ -> raise (CCHFailure @@ -101,12 +110,20 @@ object (self:'a) method get_external_basevar = match data.memrefbase with - | CBaseVar v -> v + | CBaseVar (v, _) -> v | _ -> raise (CCHFailure (LBLOCK [STR "Not a base variable: "; STR self#get_name])) + method get_string_literal_base = + match data.memrefbase with + | CStringLiteral s -> s + | _ -> + raise + (CCHFailure + (LBLOCK [STR "Not a string literal reference: "; STR self#get_name])) + method has_external_base = match data.memrefbase with CBaseVar _ -> true | _ -> false @@ -116,6 +133,9 @@ object (self:'a) method is_global_reference = match data.memrefbase with CGlobalAddress _ -> true | _ -> false + method is_string_reference = + match data.memrefbase with CStringLiteral _ -> true | _ -> false + method write_xml (node:xml_element_int) = begin vard#write_xml_memory_reference_data node data; @@ -152,6 +172,12 @@ object (self) method private mk_memory_reference (data:memory_reference_data_t) = let index = vard#index_memory_reference_data data in + let _ = + log_diagnostics_result + ~tag:"mk_memory_reference" + __FILE__ __LINE__ + ["data: " ^ (p2s (memory_reference_data_to_pretty data)); + "index: " ^ (string_of_int index)] in if H.mem table index then H.find table index else @@ -173,10 +199,11 @@ object (self) let data = { memrefbase = CGlobalAddress v; memreftype = typ } in self#mk_memory_reference data - method mk_external_reference (v:variable_t) (typ:typ) = - let data = { memrefbase = CBaseVar v; memreftype = typ } in + method mk_external_reference ?(nullattr=CanBeNull) (v:variable_t) (typ:typ) = + let data = { memrefbase = CBaseVar (v, nullattr); memreftype = typ } in self#mk_memory_reference data end + let mk_memory_reference_manager = new memory_reference_manager_t diff --git a/CodeHawk/CHC/cchpre/cCHMemoryReference.mli b/CodeHawk/CHC/cchpre/cCHMemoryReference.mli index b2387d29..1de6cfaa 100644 --- a/CodeHawk/CHC/cchpre/cCHMemoryReference.mli +++ b/CodeHawk/CHC/cchpre/cCHMemoryReference.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2023 Henny B. Sipma - Copyright (c) 2024 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 @@ -31,5 +31,8 @@ open CCHPreTypes +val memory_reference_data_to_pretty: + memory_reference_data_t -> CHPretty.pretty_t + val mk_memory_reference_manager: vardictionary_int -> memory_reference_manager_int diff --git a/CodeHawk/CHC/cchpre/cCHMemoryRegion.ml b/CodeHawk/CHC/cchpre/cCHMemoryRegion.ml index 135ed8d8..4baf1cdb 100644 --- a/CodeHawk/CHC/cchpre/cCHMemoryRegion.ml +++ b/CodeHawk/CHC/cchpre/cCHMemoryRegion.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2024 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 @@ -46,6 +46,7 @@ module H = Hashtbl let pr2s = CHPrettyUtil.pretty_to_string + class memory_region_t ~(vard:vardictionary_int) ~(index:int) @@ -69,7 +70,7 @@ object (self:'a) method get_base_var = match memory_base with - | CBaseVar v -> v + | CBaseVar (v, _) -> v | _ -> raise (CCHFailure @@ -175,8 +176,8 @@ object (self) method mk_global_region (v:variable_t) = self#mk_memory_region (CGlobalAddress v) - method mk_external_region (v:variable_t) = - self#mk_memory_region (CBaseVar v) + method mk_external_region ?(nullattr=CanBeNull) (v:variable_t) = + self#mk_memory_region (CBaseVar (v, nullattr)) method mk_uninterpreted_region (s:string) = let s = if s = "" then "none" else s in @@ -200,8 +201,8 @@ object (self) method mk_global_region_sym (v:variable_t) = self#mk_sym (self#mk_global_region v) - method mk_external_region_sym (v:variable_t) = - self#mk_sym (self#mk_external_region v) + method mk_external_region_sym ?(nullattr=CanBeNull) (v:variable_t) = + self#mk_sym (self#mk_external_region ~nullattr v) method mk_uninterpreted_sym (s:string) = self#mk_sym (self#mk_uninterpreted_region s) @@ -236,4 +237,5 @@ object (self) end + let mk_memory_region_manager = new memory_region_manager_t diff --git a/CodeHawk/CHC/cchpre/cCHPreSumTypeSerializer.ml b/CodeHawk/CHC/cchpre/cCHPreSumTypeSerializer.ml index 1a848cb6..24c5dd7c 100644 --- a/CodeHawk/CHC/cchpre/cCHPreSumTypeSerializer.ml +++ b/CodeHawk/CHC/cchpre/cCHPreSumTypeSerializer.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2023 Henny B. Sipma - 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 @@ -58,6 +58,16 @@ let address_type_mfts: address_type_t mfts_int = mk_mfts "address_type_t" [(Heap, "h"); (Stack, "s"); (External, "x")] +let ref_attribute_mfts: ref_attribute_t mfts_int = + mk_mfts + "ref_attribute_t" + [(MutableRef, "m"); (ImmutableRef, "i"); (RawPointer, "r")] + + +let null_attribute_mfts: null_attribute_t mfts_int = + mk_mfts "null_attribute_t" [(NotNull, "nn"); (CanBeNull, "pn")] + + class output_parameter_rejection_reason_mcts_t: [output_parameter_rejection_reason_t] mfts_int = object diff --git a/CodeHawk/CHC/cchpre/cCHPreSumTypeSerializer.mli b/CodeHawk/CHC/cchpre/cCHPreSumTypeSerializer.mli index b6e07244..ea74c294 100644 --- a/CodeHawk/CHC/cchpre/cCHPreSumTypeSerializer.mli +++ b/CodeHawk/CHC/cchpre/cCHPreSumTypeSerializer.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2023 Henny B. Sipma - 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 @@ -50,6 +50,10 @@ val po_status_mfts: po_status_t mfts_int val address_type_mfts: address_type_t mfts_int +val ref_attribute_mfts: ref_attribute_t mfts_int + +val null_attribute_mfts: null_attribute_t mfts_int + val assignment_mcts: assignment_t mfts_int val global_value_mcts: global_value_t mfts_int diff --git a/CodeHawk/CHC/cchpre/cCHPreTypes.mli b/CodeHawk/CHC/cchpre/cCHPreTypes.mli index b12e4b49..41d93b91 100644 --- a/CodeHawk/CHC/cchpre/cCHPreTypes.mli +++ b/CodeHawk/CHC/cchpre/cCHPreTypes.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020-2022 Henny B. Sipma - Copyright (c) 2023-2025 Aarno Labs LLC + Copyright (c) 2023-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 @@ -51,14 +51,36 @@ class type idregistry_int = method read_xml: xml_element_int -> unit end + +type ref_attribute_t = + | MutableRef + | ImmutableRef + | RawPointer + + +type null_attribute_t = + | NotNull + | CanBeNull + + (** {1 Memory representations}*) (** {2 Memory base} *) (** The memory_base_t type denotes the (symbolic) address of the base of a memory - region that is used as the ground type in a memory reference (a representation - of a memory variable) and in a memory region (a representation of the entire - memory region identified by this base. + region that is used as the ground type in a memory reference (a representation + of a memory variable) and in a memory region (a representation of the entire + memory region identified by this base. + + If the memory base includes a variable two distinct representations for the + same logical memory location may exist: one with the NUM_VAR_TYPE variable, + and one for the SYM_VAR_TYPE variable, resulting in two distinct memref + indices. This is not a problem for aliasing, as they are used in different + domains. However, it may be inconvenient in proof obligation discharge, as + it may be necessary to create the corresponding alternative representation + to retrieve invariants from that domain. An example of this is the method + [get_initialization_length_from_memory_variable vinfo] in the po checker + class file [cCHPOCheckInitializedRange]. *) type memory_base_t = | CNull of int @@ -73,7 +95,7 @@ type memory_base_t = | CGlobalAddress of variable_t (** base address of a global memory region: global variable *) - | CBaseVar of variable_t + | CBaseVar of (variable_t * null_attribute_t) (** address provided by contents of an externally controlled variable *) | CUninterpreted of string @@ -138,7 +160,10 @@ class type memory_region_manager_int = method mk_global_region: variable_t -> memory_region_int (** [mk_external_region base] returns a memory with base pointer [base]*) - method mk_external_region: variable_t -> memory_region_int + method mk_external_region: + ?nullattr: null_attribute_t + -> variable_t + -> memory_region_int method mk_uninterpreted_region: string -> memory_region_int method mk_null_sym: int -> symbol_t @@ -146,7 +171,10 @@ class type memory_region_manager_int = method mk_stack_region_sym : variable_t -> symbol_t method mk_global_region_sym: variable_t -> symbol_t - method mk_external_region_sym: variable_t -> symbol_t + method mk_external_region_sym: + ?nullattr: null_attribute_t + -> variable_t + -> symbol_t method mk_uninterpreted_sym: string -> symbol_t method mk_base_region_sym: memory_base_t -> symbol_t @@ -169,12 +197,12 @@ class type memory_region_manager_int = (** {2 Memory reference} *) -(* A memory reference is a memory base address; - points to the storage location of a variable at that location in memory - *) + (** A memory reference is an encapsulated memory base combined with the + type of the memory location pointed at. *) + type memory_reference_data_t = { memrefbase: memory_base_t ; - memreftype: typ + memreftype: typ (* type of memory pointed at *) } @@ -190,11 +218,14 @@ object ('a) (* accessors *) method get_data: memory_reference_data_t method get_base: memory_base_t + + (** Returns the type of the memory pointed at by this reference. *) method get_type: typ method get_name: string method get_external_basevar: variable_t method get_stack_address_var: variable_t method get_global_address_var: variable_t + method get_string_literal_base: string method get_base_variable: variable_t (* predicates *) @@ -202,6 +233,7 @@ object ('a) method has_external_base: bool method is_stack_reference: bool method is_global_reference: bool + method is_string_reference: bool (* xml *) method write_xml: xml_element_int -> unit @@ -218,7 +250,11 @@ object ('a) method mk_string_reference: string -> typ -> memory_reference_int method mk_stack_reference: variable_t -> typ -> memory_reference_int method mk_global_reference: variable_t -> typ -> memory_reference_int - method mk_external_reference: variable_t -> typ -> memory_reference_int + method mk_external_reference: + ?nullattr:null_attribute_t + -> variable_t + -> typ + -> memory_reference_int (* accessors *) method get_memory_reference: int -> memory_reference_int @@ -265,8 +301,16 @@ type constant_value_variable_t = | ByteSequence of variable_t * xpr_t option (** byte sequence written by v with length x *) - | MemoryAddress of int * offset - (** memory reference index *) + | MemoryAddress of int * offset * ref_attribute_t + (** constant that represents the address indicated by a memory reference index + and offset. + + Note that the offset in this case is interpreted differently than for the + variable MemoryVariable. Here the offsets mean: + NoOffset: base-address + 0 + FieldOffset(f): base-address.field + IndexOffset(n): base-address + n +*) (** {2 Unique storage location} *) @@ -294,7 +338,18 @@ type c_variable_denotation_t = *) | MemoryVariable of int * offset - (** variable identified by memory reference index *) + (** variable identified by memory reference index + + The meaning of this variable for a memory reference with basevar v is + NoOffset: *v + FieldOffset(f): v->f or ( *v ).f (memvar-x.f) + IndexOffset(n): v[n] or *(v + n) (memvar-x.n) + + The meaning of this variable for a memory reference with a stack address + of global address a, where a is declared as an array or struct is + FieldOffset(f): a.f + IndexOffset(n): a[n] + *) | MemoryRegionVariable of int (** variable used for valid-mem region analysis *) @@ -427,7 +482,8 @@ object (** mk_memory_address memindex [offset] returns a memory address from memory reference index [memindex] and an offset*) - method mk_memory_address: int -> offset -> c_variable_int + method mk_memory_address: + ?refattr:ref_attribute_t -> int -> offset -> c_variable_int method mk_string_address: string -> offset -> typ -> c_variable_int @@ -489,6 +545,8 @@ object *) method get_parameter_exp: int -> exp + method get_initial_parameter_vinfo: int -> varinfo * offset + (** [get_global_exp varindex] returns the expression associated with the initial-value variable with index [varindex] of a global variable. @@ -530,6 +588,9 @@ object method get_memory_variable: int -> (memory_reference_int * offset) method get_memory_address: int -> (memory_reference_int * offset) + + method get_memory_address_wrapped_value: int -> variable_t option + method get_initial_value_variable: int -> variable_t (** [get_purpose varindex] returns the purpose associated with the @@ -557,6 +618,8 @@ object *) method get_canonical_fnvar_index: int -> int + method get_string_literal_address_string: int -> string + (** {1 Predicates on variables}*) method is_symbolic_value: int -> bool @@ -573,6 +636,12 @@ object method is_memory_address: int -> bool + method is_mut_memory_address: int -> bool + + method is_ref_memory_address: int -> bool + + method is_string_literal_address: int -> bool + method is_program_variable: int -> bool method is_augmentation_variable: int -> bool diff --git a/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml b/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml index a2d710ea..a872bdf0 100644 --- a/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml +++ b/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml @@ -315,6 +315,8 @@ and create_po_binop addxop (PNotNull e1) 1; addxop (PValidMem e1) 1; addxop (PInScope e1) 1; + addxop (PLowerBound (tgttyp, e1)) 1; + addxop (PUpperBound (tgttyp, e1)) 1; add (PPtrLowerBound (tgttyp, binop, e1, e2)); add (if deref then PPtrUpperBoundDeref (tgttyp, binop, e1, e2) @@ -377,6 +379,10 @@ and create_po_binop addxop (PValidMem e2) 2; addxop (PInScope e1) 1; addxop (PInScope e2) 2; + addxop (PLowerBound (tgttyp1, e1)) 1; + addxop (PLowerBound (tgttyp2, e2)) 2; + addxop (PUpperBound (tgttyp1, e1)) 1; + addxop (PUpperBound (tgttyp2, e2)) 2; add (PCommonBase (e1,e2)); add (PCommonBaseType (e1,e2)); end @@ -491,8 +497,8 @@ and create_po_exp | Question (e1, e2, e3, _t) -> begin create_po_exp env (context#add_question 1) e1 loc; - create_po_exp env (context#add_question 2) e2 loc; - create_po_exp env (context#add_question 3) e3 loc + create_po_exp ~deref env (context#add_question 2) e2 loc; + create_po_exp ~deref env (context#add_question 3) e3 loc end | CastE (t, e) -> diff --git a/CodeHawk/CHC/cchpre/cCHVarDictionary.ml b/CodeHawk/CHC/cchpre/cCHVarDictionary.ml index e8f181aa..8b40b823 100644 --- a/CodeHawk/CHC/cchpre/cCHVarDictionary.ml +++ b/CodeHawk/CHC/cchpre/cCHVarDictionary.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020-2023 Henny B. Sipma - Copyright (c) 2024 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 @@ -118,8 +118,9 @@ object (self) | CNull i -> (tags,[i]) | CStringLiteral s -> (tags,[cd#index_string s]) | CStackAddress v - | CGlobalAddress v - | CBaseVar v -> (tags, [xd#index_variable v]) + | CGlobalAddress v -> (tags, [xd#index_variable v]) + | CBaseVar (v, nullity) -> + (tags @ [null_attribute_mfts#ts nullity], [xd#index_variable v]) | CUninterpreted s -> (tags @ [s],[]) in memory_base_table#add key @@ -133,7 +134,8 @@ object (self) | "str" -> CStringLiteral (cd#get_string (a 0)) | "sa" -> CStackAddress (xd#get_variable (a 0)) | "ga" -> CGlobalAddress (xd#get_variable (a 0)) - | "bv" -> CBaseVar (xd#get_variable (a 0)) + | "bv" -> + CBaseVar (xd#get_variable (a 0), null_attribute_mfts#fs (t 1)) | "ui" -> CUninterpreted (t 1) | s -> raise_tag_error name s memory_base_mcts#tags @@ -203,7 +205,8 @@ object (self) | SymbolicValue (x, t) -> let args = [xd#index_xpr x; cd#index_typ t] in (tags,args) - | MemoryAddress (i, o) -> (tags, [i; cd#index_offset o]) in + | MemoryAddress (i, o, r) -> + (tags @ [ref_attribute_mfts#ts r], [i; cd#index_offset o]) in constant_value_variable_table#add key method get_constant_value_variable (index:int) = @@ -256,7 +259,7 @@ object (self) get_opt_xpr (a 2), cd#get_typ (a 3)) | "bs" -> ByteSequence (xd#get_variable (a 0), get_opt_xpr (a 1)) - | "ma" -> MemoryAddress (a 0, cd#get_offset (a 1)) + | "ma" -> MemoryAddress (a 0, cd#get_offset (a 1), ref_attribute_mfts#fs (t 1)) | s -> raise_tag_error name s constant_value_variable_mcts#tags method index_c_variable_denotation (v:c_variable_denotation_t) = diff --git a/CodeHawk/CHC/cchpre/cCHVariable.ml b/CodeHawk/CHC/cchpre/cCHVariable.ml index b6be30a2..ba6558f8 100644 --- a/CodeHawk/CHC/cchpre/cCHVariable.ml +++ b/CodeHawk/CHC/cchpre/cCHVariable.ml @@ -102,10 +102,14 @@ let constant_value_variable_compare c1 c2 = | (ByteSequence (v1, _), ByteSequence (v2, _)) -> v1#compare v2 | (ByteSequence _, _) -> -1 | (_, ByteSequence _) -> 1 - | (MemoryAddress (i1, o1), MemoryAddress (i2, o2)) -> + | (MemoryAddress (i1, o1, r1), MemoryAddress (i2, o2, r2)) -> let l0 = Stdlib.compare i1 i2 in - if l0 = 0 then offset_compare o1 o2 else l0 - + if l0 = 0 then + let l1 = offset_compare o1 o2 in + if l1 = 0 then + Stdlib.compare r1 r2 + else l1 + else l0 let _c_variable_denotation_compare v1 v2 = match (v1, v2) with @@ -217,11 +221,23 @@ let constant_value_variable_to_pretty c = STR "_len:"; optx_to_pretty optlen; STR ")"] - | MemoryAddress (i,o) -> + | MemoryAddress (i, o, r) -> + let pr = + STR ( + "_" + ^ match r with MutableRef -> "mut" | ImmutableRef -> "ref" | _ -> "raw") in match o with - | NoOffset -> LBLOCK [STR "memaddr-"; INT i] - | _ -> - LBLOCK [STR "memaddr-"; INT i; STR ":"; offset_to_pretty o] + | NoOffset -> LBLOCK [STR "memaddr-"; INT i; pr] + | Field _ -> + LBLOCK [STR "memaddr-"; INT i; offset_to_pretty o; pr] + | Index (e, offset) -> + LBLOCK [ + STR "(memaddr-"; + INT i; + STR " + "; + exp_to_pretty e; STR ")"; + offset_to_pretty offset; + pr] let c_variable_denotation_to_pretty v = @@ -230,8 +246,14 @@ let c_variable_denotation_to_pretty v = | GlobalVariable (vinfo,offset) -> LBLOCK [STR vinfo.vname; offset_to_pretty offset] | ExternalStateVariable s -> STR s - | MemoryVariable (i,offset) -> - LBLOCK [STR "memvar-"; INT i; offset_to_pretty offset] + | MemoryVariable (i, offset) -> + (match offset with + | NoOffset -> LBLOCK [STR "memvar-"; INT i; STR ".0"] + | Field _ -> + LBLOCK [STR "memvar-"; INT i; offset_to_pretty offset] + | Index (e, suboffset) -> + LBLOCK [STR "memvar-"; INT i; STR "."; exp_to_pretty e; + offset_to_pretty suboffset]) | MemoryRegionVariable i -> LBLOCK [STR "memreg-"; INT i] | ReturnVariable _ -> STR "return" @@ -312,7 +334,7 @@ object (self:'a) | SymbolicValue (_, t) -> t | TaintedValue (_, _, _, t) -> t | ByteSequence _ -> TVoid [] - | MemoryAddress (i, offset) -> + | MemoryAddress (i, offset, _) -> TPtr (type_of_offset fdecls @@ -637,12 +659,12 @@ object (self) method mk_symbolic_value (x:xpr_t) (t:typ) = self#mk_variable (AuxiliaryVariable (SymbolicValue (x, t))) - method mk_memory_address (mindex:int) (offset:offset)= - self#mk_variable (AuxiliaryVariable (MemoryAddress (mindex, offset))) + method mk_memory_address ?(refattr=RawPointer) (mindex:int) (offset:offset)= + self#mk_variable (AuxiliaryVariable (MemoryAddress (mindex, offset, refattr))) method mk_string_address (s:string) (offset:offset) (t:typ):c_variable_int = let memref = memrefmgr#mk_string_reference s t in - self#mk_memory_address memref#index offset + self#mk_memory_address ~refattr:ImmutableRef memref#index offset method mk_check_variable l t = self#mk_variable (CheckVariable (l,t)) @@ -799,9 +821,46 @@ object (self) (match (self#get_variable index)#get_denotation with AuxiliaryVariable (MemoryAddress _) -> true | _ -> false) + method is_mut_memory_address (index: int) = + index >= 0 && + (match (self#get_variable index)#get_denotation with + AuxiliaryVariable (MemoryAddress (_, _, MutableRef)) -> true | _ -> false) + + method is_ref_memory_address (index: int) = + index >= 0 && + (match (self#get_variable index)#get_denotation with + AuxiliaryVariable (MemoryAddress (_, _, ImmutableRef)) -> true | _ -> false) + + method is_string_literal_address (index: int) = + (self#is_memory_address index) && + (match (self#get_variable index)#get_denotation with + | AuxiliaryVariable (MemoryAddress (i, _, _)) -> + let memref = memrefmgr#get_memory_reference i in + memref#is_string_reference + | _ -> false) + + method get_string_literal_address_string (index: int) = + if self#is_string_literal_address index then + (match (self#get_variable index)#get_denotation with + | AuxiliaryVariable (MemoryAddress (i, _, _)) -> + let memref = memrefmgr#get_memory_reference i in + memref#get_string_literal_base + | _ -> + raise + (CCHFailure + (LBLOCK [ + STR "Not a string literal address reference: "; + INT index]))) + else + raise + (CCHFailure + (LBLOCK [ + STR "Not a string literal address reference: "; + INT index])) + method get_memory_reference (index:int) = match (self#get_variable index)#get_denotation with - | AuxiliaryVariable (MemoryAddress (i, _offset)) -> + | AuxiliaryVariable (MemoryAddress (i, _offset, _)) -> memrefmgr#get_memory_reference i | MemoryVariable (i, _offset) -> memrefmgr#get_memory_reference i @@ -858,13 +917,26 @@ object (self) method get_memory_address (index:int) = if index > 0 then (match (self#get_variable index)#get_denotation with - | AuxiliaryVariable (MemoryAddress (i,offset)) -> + | AuxiliaryVariable (MemoryAddress (i,offset, _)) -> (memrefmgr#get_memory_reference i, offset) | _ -> raise (CCHFailure (LBLOCK [STR "Not a memory address: "; INT index]))) else raise (CCHFailure (LBLOCK [STR "Not a memory address: "; INT index])) + method get_memory_address_wrapped_value (index: int): variable_t option = + if index > 0 then + (match (self#get_variable index)#get_denotation with + | AuxiliaryVariable (MemoryAddress (i, _, _)) -> + let memref = memrefmgr#get_memory_reference i in + if memref#has_external_base then + Some memref#get_external_basevar + else + None + | _ -> None) + else + None + method get_purpose (index:int) = if self#is_augmentation_variable index then (self#get_variable index)#get_purpose @@ -941,6 +1013,25 @@ object (self) | LocalVariable _ -> true | _ -> false)) + method get_initial_parameter_vinfo (index: int): varinfo * offset = + if self#is_initial_parameter_value index then + let initvar = (self#get_variable index)#get_initial_value_variable in + let initindex = initvar#getName#getSeqNumber in + match (self#get_variable initindex)#get_denotation with + | LocalVariable (vinfo, offset) -> (vinfo, offset) + | _ -> + raise + (CCHFailure + (LBLOCK [ + STR "Variable "; + initvar#toPretty; + STR " is not an initial parameter"])) + else + raise + (CCHFailure + (LBLOCK [ + STR "Variable "; INT index; STR " is not an initial parameter"])) + method is_initial_parameter_deref_value (index:int) = (self#is_initial_value index) && (let initvar = (self#get_variable index)#get_initial_value_variable in @@ -952,13 +1043,12 @@ object (self) let memrefbase = memref#get_base in begin match memrefbase with - | CBaseVar v -> + | CBaseVar (v, _) -> self#is_initial_parameter_value v#getName#getSeqNumber | _ -> false end | _ -> false)) - method is_initial_global_value (index:int) = (self#is_initial_value index) && (let initvar = (self#get_variable index)#get_initial_value_variable in diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.ml b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.ml index 583bf050..eaed2ddd 100644 --- a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.ml +++ b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.ml @@ -115,7 +115,9 @@ let check_safe () = ("gl-inv-003", "gl_inv_003", "gl_inv_003", [], 14, -1, - "inv_implies_safe", ""); + "inv_implies_safe", "") + (* disabling the tests based on the presence of an + initial value ("gl-inv-xpr-001", "gl_inv_xpr_001", "gl_inv_xpr_001", ["(*p)"], -1, -1, @@ -137,6 +139,7 @@ let check_safe () = ["(*p)"], 14, -1, "memlval_vinv_memref_stackvar_implies_safe", "assignment(s) to i: assignedAt#11_xx_assignedAt#9") + *) ] in begin TS.new_testsuite (testname ^ "_check_safe") lastupdated; diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckLocallyInitializedTest.ml b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckLocallyInitializedTest.ml index c853407e..787b8ed1 100644 --- a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckLocallyInitializedTest.ml +++ b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckLocallyInitializedTest.ml @@ -97,6 +97,7 @@ let check_safe () = *) let check_violation () = let tests = [ + (* disabling two tests for now ("rl-xpr-001", "locally_initialized_rl_xpr_001", "rl_xpr_001", [], -1, -1, @@ -107,6 +108,7 @@ let check_violation () = [], -1, -1, "xpr_implies_violation", "value of (*p) is obtained from dereferencing parameter p"); + *) ("rl-memlval-001", "locally_initialized_rl_memlval_001", "rl_memlval_001", [], -1, -1, diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckOutputParameterInitializedTest.ml b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckOutputParameterInitializedTest.ml index 2f044d1e..cb489b0d 100644 --- a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckOutputParameterInitializedTest.ml +++ b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckOutputParameterInitializedTest.ml @@ -50,10 +50,12 @@ let po_filter (po: proof_obligation_int): proof_obligation_int option = *) let check_violation () = let tests = [ + (* disabling tests for now ("rl-inv-xpr-001", "output_parameter_initialized_rl_inv_xpr_001", "rl_inv_xpr_001", [], -1, -1, "inv_xpr_implies_violation", "") + *) ] in begin TS.new_testsuite (testname ^ "_check_violation") lastupdated;