cCHPOCheckInitialized.ml

(* =============================================================================
   CodeHawk C Analyzer
   Author: Henny Sipma
   ------------------------------------------------------------------------------
   The MIT License (MIT)

   Copyright (c) 2005-2019 Kestrel Technology LLC
   Copyright (c) 2020-2024 Henny B. Sipma
   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
   in the Software without restriction, including without limitation the rights
   to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
   copies of the Software, and to permit persons to whom the Software is
   furnished to do so, subject to the following conditions:

   The above copyright notice and this permission notice shall be included in all
   copies or substantial portions of the Software.

   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
   OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
   SOFTWARE.
   ============================================================================= *)

(* chlib *)
open CHLanguage
open CHNumerical
open CHPretty

(* chutil *)
open CHLogger
open CHPrettyUtil

(* xprlib *)
open Xprt
open XprTypes
open XprToPretty

(* cchlib *)
open CCHBasicTypes
open CCHFileEnvironment
open CCHLibTypes
open CCHTypesCompare
open CCHTypesToPretty
open CCHTypesUtil
open CCHUtilities

(* cchpre *)
open CCHMemoryBase
open CCHPOPredicate
open CCHPreTypes
open CCHProofObligation

(* cchanalyze *)
open CCHAnalysisTypes

let x2p = xpr_formatter#pr_expr
let p2s = pretty_to_string
let x2s x = p2s (x2p x)
let e2s e = p2s (exp_to_pretty e)

let fenv = CCHFileEnvironment.file_environment


class initialized_checker_t
        (poq:po_query_int) (lval:lval) (invs:invariant_int list)  =
object (self)

  method private get_symbol_name (s: symbol_t) =
    s#getBaseName
    ^ (match s#getAttributes with
       | [] -> ""
       | l  -> "(" ^ (String.concat "" l) ^ ")")

  method private is_function_pointer (memlval: lval) =
    match fenv#get_type_unrolled (type_of_lval poq#env#get_fdecls memlval) with
    | TPtr (TFun _,_) -> true
    | _ -> false

  method private memref_to_string (memref: memory_reference_int) =
    "memory base: " ^ (p2s (memory_base_to_pretty memref#get_base))

  method private offset_to_string (offset: offset) =
    match offset with
    | NoOffset -> ""
    | Field ((fname,_),foff) ->
       "offset: ." ^ fname ^ self#offset_to_string foff
    | Index (e,ioff) ->
       "offset: [" ^ (e2s e) ^ "]" ^ self#offset_to_string ioff

  method private memaddr_to_string (memref: memory_reference_int) (offset: offset) =
    (self#memref_to_string memref) ^ (self#offset_to_string offset)

  (* ----------------------------- safe ------------------------------------- *)
  (* check_safe
     - inv_implies_safe
     - check_safe_command_line_argument
     - check_safe_lval
       - check_safe_memlval
         - check_safe_functionpointer
         - memlval_vinv_implies_safe
           - memlval_vinv_memref_implies_safe
             - memlval_vinv_memref_basevar_implies_safe
   *)

  method private postcondition_implies_safe
                   (invindex: int)
                   (callee: varinfo)
                   (pcs: annotated_xpredicate_t list) =
    let mname = "postcondition_implies_safe" in
    match pcs with
    | [] -> None
    | _ ->
       List.fold_left (fun facc (pc, _) ->
           match facc with
           | Some _ -> facc
           | _ ->
              match pc with
              | XInitialized (ArgAddressedValue (ReturnValue, ArgNoOffset)) ->
                 let deps =
                   DEnvC ([invindex], [PostAssumption (callee.vid, pc)]) in
                 let msg =
                   "value addressed by return value from "
                   ^ callee.vname
                   ^ " is initialized" in
                 let site = Some (__FILE__, __LINE__, mname) in
                 Some (deps, msg, site)
              | _ -> None) None pcs

  method private inv_implies_safe (inv: invariant_int) =
    let mname = "inv_implies_safe" in
    match inv#get_fact with
    | NonRelationalFact (_, FInitializedSet l) ->
       let localAssigns =
         List.filter (fun s -> not (s#getBaseName = "parameter")) l in
       begin
         match localAssigns with
         | [] -> None
         | _ ->
            let deps = DLocal [inv#index] in
            let msg =
              (String.concat
                 "_xx_" (List.map self#get_symbol_name localAssigns)) in
            let site = Some (__FILE__, __LINE__, mname) in
            Some (deps, msg, site)
       end
    | _ ->
       match inv#expr with
       | Some (XVar v) when poq#env#is_initial_value v ->
          let var = poq#env#get_initial_value_variable v in
          if poq#env#is_memory_variable var then
            let (memref, offset) = poq#env#get_memory_variable var in
            if is_zero_memory_offset offset then
              if memref#has_external_base then
                let basevar = memref#get_external_basevar in
                if poq#env#is_function_return_value basevar then
                  let callee = poq#env#get_callvar_callee basevar in
                  let (pcs, epcs) = poq#get_postconditions basevar in
                  let r =
                    match epcs with
                    | [] ->
                       self#postcondition_implies_safe inv#index callee pcs
                    | _ -> None in
                  match r with
                  | None ->
                     let pcr =
                       XInitialized
                         (ArgAddressedValue (ReturnValue, ArgNoOffset)) in
                     begin
                       poq#mk_postcondition_request pcr callee;
                       poq#set_diagnostic
                         ("Unable to determine if memory pointed at by the return "
                          ^ "value from "
                          ^ callee.vname
                          ^ " is initialized.");
                       None
                     end
                  | Some _ -> r
                else
                   begin
                     poq#set_diagnostic_arg
                       1 ("memvar:base: " ^ (p2s memref#toPretty));
                 None
               end
            else
               None
          else
            begin
              poq#set_diagnostic_arg
                1 ("initial-value: " ^ (p2s v#toPretty));
              None
            end
          else
            None
       | _ ->
          None

  method private check_safe_functionpointer (vinfo: varinfo) =
    let vinfovalues = poq#get_vinfo_offset_values vinfo in
    let _ = poq#set_diagnostic ("function pointer: " ^ vinfo.vname)  in
    List.fold_left (fun acc (inv, offset) ->
        acc ||
          match offset with
          | NoOffset ->
             begin
               match inv#expr with
               | Some (XVar v) when poq#env#is_memory_address v ->
                  let (memref,offset) = poq#env#get_memory_address v in
                  let _ =
                    poq#set_diagnostic_arg
                      1
                      ("memory address: "
                       ^ (self#memaddr_to_string memref offset)) in
                  begin
                    match memref#get_base with
                    | CGlobalAddress v ->
                       let (gvinfo, _gvoffset) = poq#env#get_global_variable v in
                       let deps = DLocal [inv#index] in
                       let msg =
                         "variable "
                         ^ vinfo.vname
                         ^ " is initialized with function pointer "
                         ^ gvinfo.vname in
                       begin
                         poq#record_safe_result deps msg;
                         true
                       end
                    | _ -> false
                  end
               | Some x ->
                  begin
                    poq#set_diagnostic ("deref expr: " ^ (x2s x));
                    false
                  end
               | _ -> false
             end
          | _ ->
             begin
               poq#set_diagnostic
                 ("offset: "
                  ^ (p2s (offset_to_pretty offset))
                  ^ "; invariant: "
                  ^ (p2s inv#value_to_pretty)
                  ^ ")");
               false
             end) false vinfovalues

  method private memlval_vinv_memref_stackvar_implies_safe
                   (invindex: int) (vinfo: varinfo) =
    let mname = "memlval_vinv_memref_stackvar_implies_safe" in
    let vinfovalues = poq#get_vinfo_offset_values vinfo in
    List.fold_left (fun acc (vinv, voffset) ->
        match acc with
        | Some _ -> acc
        | _ ->
           match vinv#get_fact, voffset with
           | NonRelationalFact (_, FInitializedSet l), NoOffset ->
              (match l with
               | [] -> None
               | _ ->
                  let deps = DLocal [invindex; vinv#index] in
                  let msg =
                    "assignment(s) to "
                    ^ vinfo.vname
                    ^ ": "
                    ^ (String.concat
                         "_xx_" (List.map self#get_symbol_name l)) in
                  let site = Some (__FILE__, __LINE__, mname) in
                  Some (deps, msg, site))
           | _ ->
              begin
                poq#set_diagnostic
                  ~site:(Some (__FILE__, __LINE__, mname))
                  ("[" ^ vinfo.vname ^ "]: " ^ (p2s vinv#toPretty));
                None
              end
      ) None vinfovalues

  method private memlval_vinv_memref_basevar_implies_safe
                   (invindex: int) (v: variable_t) (memoffset: offset) =
    let mname = "memlval_vinv_memref_basevar_implies_safe" in
    if poq#env#is_function_return_value v then
      let callee = poq#env#get_callvar_callee v in
      let (pcs,_) = poq#get_postconditions v in
      let _ =
        poq#set_diagnostic_arg
          ~site:(Some (__FILE__, __LINE__, mname))
          1 ("return value from: " ^ callee.vname) in
      let request () =
        match memoffset with
        | NoOffset | Field _ ->
           let xpred =
             XInitialized
               (ArgAddressedValue (ReturnValue, offset_to_s_offset memoffset)) in
           if List.mem callee.vname ["malloc"; "calloc"; "realloc"] then
             poq#set_diagnostic
               ~site:(Some (__FILE__, __LINE__, mname))
               "[action]:identify side effects of intervening calls"
           else
             poq#mk_postcondition_request xpred callee
        | _ -> poq#set_diagnostic_arg
                 ~site:(Some (__FILE__, __LINE__, mname))
                 1
                 ("rv:memoffset: " ^ (p2s (offset_to_pretty memoffset))) in
      let returntype =
        match file_environment#get_type_unrolled callee.vtype with
        | TFun (t, _, _, _) -> t
        | t ->
           raise
             (CCHFailure
                (LBLOCK [
                     STR "Unexpected function type: ";
                     typ_to_pretty t;
                     STR " for: ";
                     STR callee.vname])) in
      let tgttype =
        match returntype with
        | TPtr (t, _) -> t
        | _ ->
           raise
             (CCHFailure
                (LBLOCK [
                     STR "Unexpected return type for dereferencing: ";
                     typ_to_pretty returntype;
                     STR " for ";
                     STR callee.vname])) in
      match pcs with
      | [] -> begin request (); None end
      | _ ->
         let r =
           List.fold_left (fun facc (pc, _) ->
               match facc with
               | Some _  -> facc
               | _ ->
                  match pc with
                  | XInitialized (ArgAddressedValue (ReturnValue, soff))
                       when (offset_compare
                               (s_offset_to_offset tgttype soff) memoffset) = 0 ->
                     let deps =
                       DEnvC ([invindex], [PostAssumption (callee.vid, pc)]) in
                     let rec offset_s o = match o with
                       | NoOffset -> ""
                       | Field ((fname, _), oo) -> "." ^ fname ^ (offset_s oo)
                       | Index (_e, oo) -> "[.]" ^ (offset_s oo) in
                     let offsetstring o =
                       let s = offset_s o in
                       if (String.length s) > 0 then
                         " (offset: " ^ s ^ ") "
                       else
                         "" in
                     let msg =
                       "value addressed by return value from "
                       ^ callee.vname
                       ^ (offsetstring memoffset)
                       ^ " is initialized" in
                     let site = Some (__FILE__, __LINE__, mname) in
                     Some (deps, msg, site)
                  | _ -> None) None pcs in
         match r with
         | Some _ -> r
         | _ ->
            begin
             request ();
             None
           end
    else
      None

  method private memlval_vinv_memref_implies_safe
                   (invindex: int)
                   (memref: memory_reference_int)
                   (offset: offset)
                   (memoffset: offset) =
    let mname = "memlval_vinv_memref_implies_safe" in
    match offset with
    | NoOffset ->
       begin
         match memref#get_base with
         | CGlobalAddress gvar ->
            let (gvinfo, goffset) = poq#env#get_global_variable gvar in
            begin
              match goffset with
              | NoOffset ->
                 let lval =
                   (Mem (Lval (Var (gvinfo.vname, gvinfo. vid), NoOffset)),
                    memoffset) in
                 let pred = PInitialized lval in
                 begin
                   match poq#check_implied_by_assumptions pred with
                   | Some pred ->
                      let deps = DEnvC ([invindex],[GlobalApiAssumption pred]) in
                      let msg =
                        "initialized implied by global assumption: "
                        ^ (p2s  (po_predicate_to_pretty pred)) in
                      let site = Some (__FILE__, __LINE__, mname) in
                      Some (deps, msg, site)
                   | _ ->
                      let xpred = po_predicate_to_xpredicate poq#fenv pred in
                      begin
                        poq#mk_global_request xpred;
                        None
                      end
                 end
              | _ -> None
            end
         | CStackAddress svar ->
            let (vinfo, voffset) = poq#env#get_local_variable svar in
            let _ =
              poq#set_diagnostic_arg
                ~site:(Some (__FILE__, __LINE__, mname))
                1
                ("stack variable: "
                 ^ vinfo.vname
                 ^ " with offset "
                 ^ (p2s (offset_to_pretty voffset))) in
            (match (voffset, memoffset) with
             | (NoOffset, NoOffset) ->
                self#memlval_vinv_memref_stackvar_implies_safe invindex vinfo
             | _ -> None)

         | CBaseVar (v, _) ->
            (try
               self#memlval_vinv_memref_basevar_implies_safe invindex v memoffset
             with
             | CCHFailure p ->
                begin
                  poq#set_diagnostic
                    ~site:(Some (__FILE__, __LINE__, mname))
                    ("E:basevar: " ^ v#getName#getBaseName);
                  ch_error_log#add "initialized-basevar" p;
                  None
                end
             | _ -> None)
         | _ -> None
       end
    | _ ->
       None

  method private memlval_vinv_implies_safe
                   (inv: invariant_int) (memoffset: offset) =
    let mname = "memlval_vinv_implies_safe" in
    let is_field_offset offset =
      match offset with
      | NoOffset -> true
      | Field (_,NoOffset) -> true
      | _  -> false in
    match inv#expr with
    | Some x when poq#is_global_expression x ->
       if is_field_offset memoffset then
         let g = poq#get_global_expression x in
         let derefg = (Mem g, memoffset) in
         let pred = PInitialized derefg in
         begin
           match poq#check_implied_by_assumptions pred with
           | Some pred ->
              let deps = DEnvC ([inv#index], [GlobalApiAssumption pred]) in
              let msg =
                "initialized property implied by global assumption: "
                ^ (p2s (po_predicate_to_pretty pred)) in
              let site = Some (__FILE__, __LINE__, mname) in
              Some (deps, msg, site)
           | _ ->
              let xpred = po_predicate_to_xpredicate poq#fenv pred in
              begin
                poq#mk_global_request xpred;
                None
              end
         end
       else
         let site = Some (__FILE__, __LINE__, mname) in
         begin
           poq#set_diagnostic
             ~site ("mem-offset: " ^ (p2s (offset_to_pretty memoffset)));
           None
         end
    | Some (XVar v) when poq#env#is_memory_address v ->
       let (memref, offset) = poq#env#get_memory_address v in
       let _ =
         poq#set_diagnostic_arg
           ~site:(Some (__FILE__, __LINE__, mname))
           1
           ("D:memory address: " ^ (self#memaddr_to_string memref offset)) in
       let _ =
         poq#set_diagnostic
           ~site:(Some (__FILE__, __LINE__, mname))
           ("mem-offset: " ^ (p2s (offset_to_pretty memoffset))) in
       self#memlval_vinv_memref_implies_safe inv#index memref offset memoffset
    | Some x ->
       begin
         poq#set_diagnostic_arg
           ~site:(Some (__FILE__, __LINE__, mname)) 1 ("[deref] " ^ (x2s x));
         None
       end
    | _ -> None

  method private check_safe_memlval (memlval: lval) (memoffset: offset) =
    let mname = "check_safe_memlval" in
    match (memlval, memoffset) with
    | ((Var (_vname, vid), NoOffset), NoOffset)
         when self#is_function_pointer memlval && vid > 0 ->
       self#check_safe_functionpointer (poq#env#get_varinfo vid)
    | ((Var (_vname, vid), NoOffset), _) when vid > 0 ->
       let vinfo = poq#env#get_varinfo vid in
       let vinfovalues = poq#get_vinfo_offset_values vinfo in
       let _ =
         poq#set_vinfo_diagnostic_invariants
           ~site:(Some (__FILE__, __LINE__, mname)) vinfo in
       let _ =
         poq#set_diagnostic
           ~site:(Some (__FILE__, __LINE__, mname))
           ("[mem-offset]: " ^ (p2s (offset_to_pretty memoffset))) in
       List.fold_left (fun acc (inv, offset) ->
           acc ||
             match offset with
             | NoOffset ->
                begin
                  match self#memlval_vinv_implies_safe inv memoffset with
                  | Some (deps, msg, site) ->
                     begin
                       poq#record_safe_result ~site deps msg;
                       true
                     end
                  | _ -> false
                end
             | _ ->
                begin
                  poq#set_diagnostic
                    ~site:(Some (__FILE__, __LINE__, mname))
                    ("[deref offset]: " ^  (p2s (offset_to_pretty offset)));
                  false
                end) false vinfovalues
    | _ -> false

  method private check_safe_lval =
    match lval with
    | (Mem (Lval memlval), memoffset) ->
       self#check_safe_memlval memlval memoffset
    | _ -> false

  method check_safe =
    (List.fold_left (fun acc inv ->
            acc ||
              match self#inv_implies_safe inv with
              | Some (deps, msg, site) ->
                 begin
                   poq#record_safe_result ~site deps msg;
                   true
                 end
              | _ -> false) false invs)
    || self#check_safe_lval

  (* ----------------------- violation -------------------------------------- *)
  (* check_violation
     - inv_implies_violation
       - xprlist_implies_violation
         - xpr_implies_violation
           - var_implies_violation
   *)

  method private var_implies_violation (invindex: int) (v: variable_t) =
    let mname = "var_implies_violation" in
    if poq#env#is_byte_sequence v then
      let bsv = poq#env#get_byte_sequence_origin v in
      let callee = poq#env#get_callvar_callee bsv in
      let deps = DLocal [invindex] in
      let msg = "value may be tainted by " ^ callee.vname in
      let site = Some (__FILE__, __LINE__, mname) in
      Some (deps, msg, site)
    else
      None

  method private xpr_implies_violation (invindex: int) (x: xpr_t) =
    let r = None in
    let r = match r with
      | Some _ -> r
      | _ ->
         match x with
         | XVar v -> self#var_implies_violation invindex v
         | _ -> None in
    r

  method  private xprlist_implies_violation (invindex: int) (l: xpr_t list) =
    List.fold_left (fun acc x ->
        match acc with
        | Some _ -> acc
        | _ -> self#xpr_implies_violation invindex x) None l

  method private inv_implies_violation (inv: invariant_int) =
    let r = None in
    let r = match r with
      | Some _ -> r
      | _ ->
         match inv#lower_bound_xpr with
         | Some x ->  self#xpr_implies_violation inv#index x
         | _ -> None in
    let r = match r with
      | Some _ -> r
      | _ ->
         match inv#lower_bound_xpr_alternatives with
         | Some l -> self#xprlist_implies_violation inv#index l
         | _ -> None in
    r

  method check_violation =
    List.fold_left (fun acc inv ->
        acc ||
          match self#inv_implies_violation inv with
          | Some (deps, msg, site) ->
             begin
               poq#record_violation_result ~site deps msg;
               true
             end
          |  _ -> false) false invs

  (* ----------------------- delegation ------------------------------------- *)
  (* check_delegation
     - check_delegation_lval
       - check_delegation_memlval
         - memlval_vinv_implies_delegation
           - memlval_var_implies_delegation

     - check_delegation_invs
       - inv_implies_delegation
         - xpr_implies_delegation
   *)

  method private xpr_implies_delegation (invindex: int) (x: xpr_t) =
    let mname = "xpr_implies_delegation" in
    if poq#is_api_expression x then
      let _ =
        poq#set_diagnostic_arg
          ~site:(Some (__FILE__, __LINE__, mname))
          1
          ("api expression: " ^ (e2s (poq#get_api_expression x))) in
      match poq#get_api_expression x with
      | Lval apilval ->
         let pred = PInitialized apilval in
         let deps = DEnvC ([invindex], [ApiAssumption pred]) in
         let msg =
           "condition "
           ^ (p2s (po_predicate_to_pretty pred))
           ^ " delegated to the api" in
         let site = Some (__FILE__, __LINE__, mname) in
         Some (deps, msg, site)
      | _ -> None
    else
      None

  method private inv_implies_delegation (inv: invariant_int) =
    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
    | [] -> false
    | _ ->
       List.fold_left (fun acc inv ->
           acc ||
             match self#inv_implies_delegation inv with
             | Some (deps, msg, site) ->
                begin
                  poq#record_safe_result ~site deps msg;
                  true
                end
             | _ -> false) false invs

  method private memlval_var_implies_delegation
                   (invindex: int) (lval: lval) (memoffset: offset) =
    let mname = "memlval_var_implies_delegation" in
    match memoffset with
    | Field ((fname,fid),
             Index (Lval (Var (_vname, vid), NoOffset),
                    (( NoOffset | Field (_, NoOffset)) as suboff))) when vid > 0 ->
       let vinfo = poq#env#get_varinfo vid in
       let vinfovalues = poq#get_vinfo_offset_values vinfo in
       let _ = poq#set_vinfo_diagnostic_invariants vinfo in
       let mkdeps n =
         let noffset = Field ((fname, fid),Index (make_constant_exp n,suboff))  in
         let memlval = (Mem (Lval lval), noffset) in
         let pred = PInitialized memlval  in
         let deps = DEnvC ([invindex],[ApiAssumption pred]) in
         let site = Some (__FILE__, __LINE__, mname) in
         let msg =
           "delegate condition "
           ^ (p2s (po_predicate_to_pretty pred))
           ^ " to the api" in
         (deps, msg, site) in
       List.fold_left (fun acc (inv, _offset) ->
           match acc with
           | Some _ -> acc
           | _ ->
              match (inv#lower_bound_xpr, inv#upper_bound_xpr) with
              | (Some (XConst (IntConst lb)), Some (XConst (IntConst ub)))
                   when (ub#sub lb)#lt (mkNumerical 10) ->
                 let numrange = mk_num_range lb (ub#add numerical_one) in
                 begin
                   match numrange with
                   | [] -> None
                   | h::tl ->
                      let (deps, msg, _) =
                        List.fold_left (fun (d, m, _) n ->
                            let (dd, mm, _) = mkdeps n in
                            let d = join_dependencies d dd in
                            let m = m ^ "; " ^ mm in
                            (d, m, None)) (mkdeps h) tl in
                      let site = Some (__FILE__, __LINE__, mname) in
                      Some (deps, msg, site)
                 end
              | _ -> None) None vinfovalues
    | _ ->
       begin
         poq#set_diagnostic ("[U:memoffset] " ^ (p2s (offset_to_pretty memoffset)));
         None
       end

  method private memlval_vinv_implies_delegation
                   (inv: invariant_int) (memoffset: offset) =
    let mname = "memlval_vinv_implies_delegation" in
    match inv#expr with
    | Some x when poq#is_api_expression x ->
       begin
         match poq#get_api_expression x with
         | Lval lval ->
            if is_constant_offset memoffset then
              let memlval =  (Mem (Lval lval),memoffset) in
              let pred = PInitialized memlval in
              let deps = DEnvC ([inv#index], [ApiAssumption  pred]) in
              let msg =
                "condition "
                ^ (p2s (po_predicate_to_pretty pred))
                ^ " delegated to the api (vinv)" in
              let site = Some (__FILE__, __LINE__, mname) in
              Some (deps, msg, site)
            else
              self#memlval_var_implies_delegation inv#index lval memoffset
         | _ ->
            begin
              poq#set_diagnostic_arg
                ~site:(Some (__FILE__, __LINE__, mname)) 1 ("[api] " ^ (x2s x));
              None
            end
       end
    | _ -> None

  method private check_delegation_memlval (memlval: lval) (memoffset: offset) =
    match memlval with
    | (Var (_vname, vid), NoOffset) when vid > 0 ->
       let vinfo  = poq#env#get_varinfo vid in
       let vinfovalues = poq#get_vinfo_offset_values vinfo in
       List.fold_left (fun  acc (inv, offset) ->
           acc ||
             match offset with
             | NoOffset ->
                begin
                  match self#memlval_vinv_implies_delegation
                          inv memoffset  with
                  | Some (deps, msg, site) ->
                     begin
                       poq#record_safe_result ~site deps msg;
                       true
                     end
                  | _ -> false
                end
             | _ -> false) false vinfovalues
    | _ -> false

  method private check_delegation_lval =
    match lval with
    | (Mem (Lval memlval), memoffset) ->
       self#check_delegation_memlval memlval memoffset
    | (Mem
         (BinOp
            (_,
             Lval (Var (_vname, vid), NoOffset),
             Const (CInt (i64,_,_)), _) as e), NoOffset) when vid > 0  ->
       let vinfo = poq#env#get_varinfo vid in
       begin
         poq#set_vinfo_diagnostic_invariants vinfo;
         poq#set_diagnostic_arg 1 ("offset: " ^ (Int64.to_string i64));
         (let xpr = poq#get_external_value e in
          if is_random xpr then () else
            poq#set_diagnostic_arg 1 ("deref-value: " ^ (x2s xpr)));
         false
       end
    | _ -> false

  method check_delegation =
    self#check_delegation_invs || self#check_delegation_lval

end


let check_initialized (poq:po_query_int) (lval:lval) =
  let f_priority (inv: invariant_int) =
    match inv#get_fact with
    | NonRelationalFact (_, FInitializedSet _) -> true
    | _ -> false in
  let invs =
    CCHInvariantFact.prioritize_invariants f_priority (poq#get_invariants 1) in
  let _ = poq#set_diagnostic_invariants 1 in
  let checker = new initialized_checker_t poq lval invs in
  checker#check_safe || checker#check_violation || checker#check_delegation