CHC:add representation for output parameter rejection reasons

Author: sipma

CodeHawk/CH/chutil/cHTraceResult.ml

@@ -168,6 +168,16 @@ let tbind_iter_list (f: 'a -> unit traceresult) (args: 'a list): unit traceresul
       | _ -> f a) (Ok ()) args
 
 
+let tbind_map_list (f: 'a -> 'b traceresult) (args: 'a list): 'b list traceresult =
+  List.fold_left (fun acc_r a ->
+      match acc_r with
+      | Error _ -> acc_r
+      | Ok vl ->
+         match f a with
+         | Error e -> Error e
+         | Ok v -> Ok (vl @ [v])) (Ok []) args
+
+
 let to_bool (f: 'a -> bool) (r: 'a traceresult) =
   match r with
   | Ok v -> f v

CodeHawk/CH/chutil/cHTraceResult.mli

@@ -143,6 +143,9 @@ val tfold_list_fail:
 val tbind_iter_list: ('a -> unit traceresult) -> 'a list -> unit traceresult
 
 
+val tbind_map_list: ('a -> 'b traceresult) -> 'a list -> 'b list traceresult
+
+
 (** [to_bool f r] is [f v] if [r] is [Ok v] and [false] otherwise.*)
 val to_bool: ('a -> bool) -> 'a traceresult -> bool
 

CodeHawk/CHC/cchcil/cCHXParseFile.ml

@@ -240,13 +240,17 @@ let save_xml_file f =
       List.fold_left (fun a g ->
           match g with
           | GFun (fdec, _loc) -> fdec :: a | _ -> a) [] f.globals in
+    let _ =
+      log_info "Found %d function(s) [%s:%d]" (List.length fns) __FILE__ __LINE__ in
+    let _ =
+      List.iter (fun fn -> log_info "Decl: %s" fn.svar.vdecl.file) fns in
     let fns =
       if !keep_system_includes then
         fns
       else
         (* filter out functions with an absolute path names *)
         List.filter (fun fdec ->
-            not ((String.get fdec.svar.vdecl.file 0) = '/')) fns in
+            not ((String.sub fdec.svar.vdecl.file 0 4) = "/usr")) fns in
     let fnsTarget = Filename.concat (Filename.dirname absoluteTarget) "functions" in
     begin
       List.iter (fun f -> cil_function_to_file target f fnsTarget) fns;

CodeHawk/CHC/cchlib/cCHTypesUtil.ml

@@ -870,7 +870,7 @@ let rec is_scalar_struct_type (t: typ): bool =
   | TComp (ckey, _) ->
      let cinfo = fenv#get_comp ckey in
      List.for_all (fun finfo ->
-         match finfo.ftype with
+         match fenv#get_type_unrolled finfo.ftype with
          | TInt _
            | TFloat _
            | TPtr _

CodeHawk/CHC/cchpre/cCHCandidateOutputParameter.ml

@@ -39,7 +39,7 @@ open CCHPreTypes
 
 module H = Hashtbl
 
-let (let* ) x f = CHTraceResult.tbind f x   
+let (let* ) x f = CHTraceResult.tbind f x
 
 let ccontexts = CCHContext.ccontexts
 let cdictionary = CCHDictionary.cdictionary
@@ -150,7 +150,7 @@ object (self)
       fdecls#write_xml_location node self#loc;
       ccontexts#write_xml_context node self#ctxt;
       cdictionary#write_xml_exp_opt node self#rv;
-    end    
+    end
 
 end
 
@@ -163,11 +163,11 @@ object (self)
   val mutable status: output_parameter_status_t = OpUnknown
   val returnsites = H.create 3 (* ictxt -> copparam_returnsite_t *)
   val calldeps = H.create 3  (* ictxt ->  copparam_call_dependency_t *)
-  val mutable reject_reasons: string list = []
+  val mutable reject_reasons: output_parameter_rejection_reason_t list = []
 
   method parameter = vinfo
 
-  method reject (reason: string) =
+  method reject (reason: output_parameter_rejection_reason_t) =
     begin
       reject_reasons <- reason :: reject_reasons;
       status <- OpRejected reject_reasons
@@ -177,15 +177,17 @@ object (self)
     match po#get_predicate with
     | PLocallyInitialized _ ->
        if po#is_violation then
-         self#reject
-           ("parameter is read at line " ^ (string_of_int po#get_location.line))
+         self#reject (OpParameterRead po#get_location.line)
+    | POutputParameterScalar (vinfo, _) ->
+       if po#is_violation then
+         self#reject (OpArrayType vinfo.vtype)
     | POutputParameterInitialized _
       | POutputParameterUnaltered _ ->
        let ictxt = ccontexts#index_context po#get_context in
        if H.mem returnsites ictxt then
          (H.find returnsites ictxt)#record_proof_obligation_result po
     | _ -> ()
-       
+
 
   method is_active (_po_s: proof_obligation_int list) =
     match status with

CodeHawk/CHC/cchpre/cCHCreateOutputParameterPOs.ml

@@ -439,37 +439,31 @@ let initialize_output_parameters
          let ptype = fenv#get_type_unrolled ptrparam.vtype in
          if has_const_attribute ptype then
            (* parameter is read-only *)
-           analysisdigest#reject_parameter pname "parameter has const qualifier"
+           analysisdigest#reject_parameter pname (OpConstQualifier ptype)
          else if has_deref_const_attribute ptype then
            (* pointed-to object is read-only *)
-           analysisdigest#reject_parameter
-             pname "deref parameter has const qualifier"
+           analysisdigest#reject_parameter pname (OpConstQualifier ptype)
          else if is_char_star_type ptype then
            (* parameter is probably an array, excluded for now *)
-           analysisdigest#reject_parameter pname "parameter is a char-star"
+           analysisdigest#reject_parameter pname (OpArrayType ptype)
          else if is_void_ptr_type ptype then
            (* parameter target has undetermined type, excluded for now *)
-           analysisdigest#reject_parameter pname "parameter is void-star"
+           analysisdigest#reject_parameter pname OpVoidPointer
          else
            match ptype with
            | TPtr (tgt, _) ->
               (match tgt with
                | TPtr _ ->
                   (* parameter is pointer to pointer, excluded for now *)
-                  analysisdigest#reject_parameter pname "parameter is double reference"
+                  analysisdigest#reject_parameter pname (OpPointerPointer ptype)
                | TComp (ckey, _) when is_system_struct tgt ->
                   (* structs created by a system library, such as _IO__FILE_ *)
                   let compinfo = fenv#get_comp ckey in
-                  analysisdigest#reject_parameter
-                    pname
-                    ("parameter is pointer to system struct: " ^ compinfo.cname)
+                  analysisdigest#reject_parameter pname (OpSystemStruct compinfo)
                | TComp (ckey, _) when not (is_scalar_struct_type tgt) ->
                   (* struct has embedded arrays, excluded for now *)
                   let compinfo = fenv#get_comp ckey in
-                  analysisdigest#reject_parameter
-                    pname
-                    ("parameter is pointer to struct with embedded array: " ^
-                       compinfo.cname)
+                  analysisdigest#reject_parameter pname (OpArrayStruct compinfo)
                | _ -> (* accept *) Ok ())
            | _ ->
               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__);
@@ -484,7 +478,7 @@ let process_function (fname:string): unit traceresult =
   let _ = log_info "Process function %s [%s:%d]" fname __FILE__ __LINE__ in
   let fundec = read_function_semantics fname in
   let ptrparams = get_pointer_parameters fundec in
-  if (List.length ptrparams) > 0 then
+  (* if (List.length ptrparams) > 0 then *)
     let _ = read_proof_files fname fundec.sdecls in
     let* _ = proof_scaffolding#initialize_output_parameter_analysis fname in
     let* analysisdigest = proof_scaffolding#get_output_parameter_analysis fname in
@@ -495,8 +489,8 @@ let process_function (fname:string): unit traceresult =
     let _ = save_proof_files fname in
     let _ = save_api fname in
     Ok ()
-  else
-    Ok ()
+  (* else
+    Ok () *)
 
 
 let output_parameter_po_process_file (): unit traceresult =
@@ -508,7 +502,7 @@ let output_parameter_po_process_file (): unit traceresult =
     let _ = fenv#initialize cfile in
     let _ = cdeclarations#index_location call_sink in
     let functions = fenv#get_application_functions in
-    let functions = List.filter (fun f -> not (f.vname = "main")) functions in
+    (* let functions = List.filter (fun f -> not (f.vname = "main")) functions in *)
     let _ =
       log_info
         "Cfile %s initialized with %d functions [%s:%d]"

CodeHawk/CHC/cchpre/cCHOutputParameterAnalysis.ml

@@ -222,7 +222,9 @@ object (self)
   method private callee_callsites =
     H.fold (fun _ v a -> v :: a) callee_callsites []
 
-  method reject_parameter (vname: string) (reason: string): unit traceresult =
+  method reject_parameter
+           (vname: string)
+           (reason: output_parameter_rejection_reason_t): unit traceresult =
     if H.mem params vname then
       Ok ((H.find params vname)#reject reason)
     else

CodeHawk/CHC/cchpre/cCHPODictionary.ml

@@ -45,7 +45,9 @@ open CCHPreSumTypeSerializer
 open CCHPreTypes
 
 module H = Hashtbl
+module TR = CHTraceResult
 
+let (let* ) x f = CHTraceResult.tbind f x
 
 let cdecls = CCHDeclarations.cdeclarations
 let cd = CCHDictionary.cdictionary
@@ -87,6 +89,8 @@ class podictionary_t
         (_fname:string) (fdecls:cfundeclarations_int):podictionary_int =
 object (self)
 
+  val output_parameter_rejection_reason_table =
+    mk_index_table "output-parameter-rejection-reason-table"
   val output_parameter_status_table = mk_index_table "output-parameter-status-table"
   val assumption_table = mk_index_table "assumption-table"
   val ppo_type_table = mk_index_table "ppo-type-table"
@@ -96,6 +100,7 @@ object (self)
 
   initializer
     tables <- [
+      output_parameter_rejection_reason_table;
       output_parameter_status_table;
       assumption_table;
       ppo_type_table;
@@ -104,11 +109,43 @@ object (self)
 
   method fdecls = fdecls
 
+  method index_output_parameter_rejection_reason
+           (r: output_parameter_rejection_reason_t) =
+    let tags = [output_parameter_rejection_reason_mcts#ts r] in
+    let key = match r with
+      | OpConstQualifier ty -> (tags, [cd#index_typ ty])
+      | OpSystemStruct cinfo -> (tags, [cdecls#index_compinfo cinfo])
+      | OpArrayStruct cinfo -> (tags, [cdecls#index_compinfo cinfo])
+      | OpArrayType ty -> (tags, [cd#index_typ ty])
+      | OpVoidPointer -> (tags, [])
+      | OpPointerPointer ty -> (tags, [cd#index_typ ty])
+      | OpParameterRead linenumber -> (tags, [linenumber])
+      | OpOtherReason reason -> (tags, [cd#index_string reason]) in
+    output_parameter_rejection_reason_table#add key
+
+  method get_output_parameter_rejection_reason (index: int):
+           output_parameter_rejection_reason_t traceresult =
+    let name = "output_parameter_rejection_reason" in
+    let (tags, args) = output_parameter_rejection_reason_table#retrieve index in
+    let t = t name tags in
+    let a = a name args in
+    match (t 0) with
+    | "a" -> Ok (OpArrayStruct (cdecls#get_compinfo (a 0)))
+    | "at" -> Ok (OpArrayType (cd#get_typ (a 0)))
+    | "c" -> Ok (OpConstQualifier (cd#get_typ (a 0)))
+    | "o" -> Ok (OpOtherReason (cd#get_string (a 0)))
+    | "p" -> Ok (OpPointerPointer (cd#get_typ (a 0)))
+    | "r" -> Ok (OpParameterRead (a 0))
+    | "s" -> Ok (OpSystemStruct (cdecls#get_compinfo (a 0)))
+    | "v" -> Ok OpVoidPointer
+    | s -> Error [elocm __LINE__ name s output_parameter_rejection_reason_mcts#tags]
+
   method index_output_parameter_status (s: output_parameter_status_t) =
     let tags = [output_parameter_status_mcts#ts s] in
     let key = match s with
       | OpUnknown -> (tags, [])
-      | OpRejected rs -> (tags, (List.map cd#index_string rs))
+      | OpRejected rs ->
+         (tags, (List.map self#index_output_parameter_rejection_reason rs))
       | OpViable -> (tags, [])
       | OpWritten -> (tags, [])
       | OpUnaltered -> (tags, []) in
@@ -124,7 +161,10 @@ object (self)
     | "v" -> Ok OpViable
     | "w" -> Ok OpWritten
     | "a" -> Ok OpUnaltered
-    | "r" -> Ok (OpRejected (List.map cd#get_string args))
+    | "r" ->
+       let* reasons =
+         TR.tbind_map_list self#get_output_parameter_rejection_reason args in
+       Ok (OpRejected reasons)
     | s -> Error [elocm __LINE__ name s output_parameter_status_mcts#tags]
 
   method index_assumption (a:assumption_type_t) =

CodeHawk/CHC/cchpre/cCHPreSumTypeSerializer.ml

@@ -58,6 +58,33 @@ let address_type_mfts: address_type_t mfts_int =
   mk_mfts  "address_type_t" [(Heap, "h"); (Stack, "s"); (External, "x")]
 
 
+class output_parameter_rejection_reason_mcts_t:
+        [output_parameter_rejection_reason_t] mfts_int =
+object
+
+  inherit [output_parameter_rejection_reason_t] mcts_t
+            "output_parameter_rejection_reason_t"
+
+  method! ts (r: output_parameter_rejection_reason_t) =
+    match r with
+    | OpConstQualifier _ -> "c"
+    | OpSystemStruct _ -> "s"
+    | OpArrayStruct _ -> "a"
+    | OpArrayType _ -> "at"
+    | OpVoidPointer -> "v"
+    | OpPointerPointer _ -> "p"
+    | OpParameterRead _ -> "r"
+    | OpOtherReason _ -> "o"
+
+  method! tags = ["a"; "at"; "c"; "p"; "r"; "s"; "v"]
+
+end
+
+let output_parameter_rejection_reason_mcts:
+      output_parameter_rejection_reason_t mfts_int =
+  new output_parameter_rejection_reason_mcts_t
+
+
 class output_parameter_status_mcts_t: [output_parameter_status_t] mfts_int =
 object
 

CodeHawk/CHC/cchpre/cCHPreSumTypeSerializer.mli

@@ -41,6 +41,9 @@ val bound_type_mfts: bound_type_t mfts_int
 
 val dependencies_mcts: dependencies_t mfts_int
 
+val output_parameter_rejection_reason_mcts:
+  output_parameter_rejection_reason_t mfts_int
+
 val output_parameter_status_mcts: output_parameter_status_t mfts_int
 
 val po_status_mfts: po_status_t mfts_int