Cmdlineargs

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

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

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

CodeHawk/CH/xprlib/xprt.mli

@@ -1,12 +1,12 @@
-(* =============================================================================
+ (* =============================================================================
    CodeHawk Analyzer Infrastructure Utilities
    Author: Henny Sipma
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
    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
 

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} *)

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