CHC: merge result-value migration with Errno changes

Author: sipma

CodeHawk/CHC/cchanalyze/cCHCallTranslator.ml

@@ -87,11 +87,21 @@ let is_assert_fail_function fname =  fname = "__assert_fail"
 
 let is_library_function (fname:string): bool =
   if CCHDeclarations.cdeclarations#has_varinfo_by_name fname then
-    let varinfo = CCHDeclarations.cdeclarations#get_varinfo_by_name fname in
-    (* starts with '/' ? *)
-    match String.index_opt varinfo.vdecl.file '/' with
-    | Some i -> i = 0
-    | _ -> false
+    TR.tfold
+      ~ok:(fun varinfo ->
+        (* starts with '/' ? *)
+        match String.index_opt varinfo.vdecl.file '/' with
+        | Some i -> i = 0
+        | _ -> false)
+      ~error:(fun err ->
+        begin
+          log_error_result
+            ~tag:"is_library_function"
+            __FILE__ __LINE__
+            [String.concat ", " err];
+          false
+        end)
+      (CCHDeclarations.cdeclarations#get_varinfo_by_name fname)
   else
     false
 
@@ -217,8 +227,8 @@ let is_not_writes_errno x = not (is_writes_errno x)
 let has_writes_errno = List.exists is_writes_errno
 
 let disjoint (p : annotated_xpredicate_t) (q : annotated_xpredicate_t) =
-  let int_of_ret op c = 
-    match op with 
+  let int_of_ret op c =
+    match op with
     | Eq -> CHIntervals.mkInterval c c
     | Lt -> new CHIntervals.interval_t CHBounds.minus_inf_bound (CHBounds.bound_of_num (c#sub numerical_one))
     | Le -> new CHIntervals.interval_t CHBounds.minus_inf_bound (CHBounds.bound_of_num c)
@@ -230,7 +240,7 @@ let disjoint (p : annotated_xpredicate_t) (q : annotated_xpredicate_t) =
   match fst p, fst q with
   | XNull ReturnValue, XNotNull ReturnValue -> true
 
-  | XRelationalExpr (op, ReturnValue, NumConstant v), 
+  | XRelationalExpr (op, ReturnValue, NumConstant v),
     XRelationalExpr (op', ReturnValue, NumConstant v') ->
     let pi = int_of_ret op v in
     let qi = int_of_ret op' v' in
@@ -1520,17 +1530,17 @@ object (self)
       let unknownSym = CCHErrnoWritePredicateSymbol.to_symbol CCHErrnoWritePredicateSymbol.Unknown in
       List.map (fun v -> make_c_cmd (ASSIGN_SYM (v, SYM unknownSym))) env#get_errno_write_vars
 
-  method private get_errno_sideeffect 
+  method private get_errno_sideeffect
                   (fname: string)
-                  (postconditions: annotated_xpredicate_t list * annotated_xpredicate_t list) 
+                  (postconditions: annotated_xpredicate_t list * annotated_xpredicate_t list)
                   (optrvar: variable_t option) =
-    let (pcs, epcs) = postconditions in 
+    let (pcs, epcs) = postconditions in
 
-    if not (is_library_function fname) then 
+    if not (is_library_function fname) then
       self#havoc_errno_write
-    else 
+    else
 
-    let non_errno_pcs, non_errno_epcs = 
+    let non_errno_pcs, non_errno_epcs =
           List.filter is_not_writes_errno pcs, List.filter is_not_writes_errno epcs in
 
     let rv_interval op c =
@@ -1544,12 +1554,12 @@ object (self)
     in
 
     (* We want to make sure that the success and failure cases are disjoint, otherwise
-       we may be able to prove that errno was written in the success case even though it wasn't specified. 
+       we may be able to prove that errno was written in the success case even though it wasn't specified.
        This is almost certainly an error in the specification, but we don't want that error to propagate here. *)
     let success_no_write p = List.exists (disjoint p) non_errno_pcs in
 
-    let errno_sideeffect = 
-      if has_writes_errno epcs then 
+    let errno_sideeffect =
+      if has_writes_errno epcs then
         match optrvar, non_errno_epcs with
         | Some rvar, [XNull ReturnValue, _ as p] when success_no_write p ->
             let idx = rvar#getName#getSeqNumber in
@@ -1562,18 +1572,18 @@ object (self)
             let idxNullSym = CCHErrnoWritePredicateSymbol.to_symbol (CCHErrnoWritePredicateSymbol.VarInt(idx, lb, ub)) in
             [ make_c_cmd (ASSIGN_SYM (env#get_errno_write_var context, SYM idxNullSym)) ]
 
-        |  _ -> 
+        |  _ ->
             []
       else
         []
-      
+
       in errno_sideeffect
 
   method private get_sideeffect
                    (fname:string)
                    (fvid:int)
                    (args:exp list)
-                   (fnargs:xpr_t list) 
+                   (fnargs:xpr_t list)
                    optrvar
                    =
     let vinfo = TR.tget_ok (fdecls#get_varinfo_by_vid fvid) in

CodeHawk/CHC/cchanalyze/cCHExpTranslator.ml

@@ -305,7 +305,7 @@ object (self)
     match op with
     | Neg -> XOp (XNeg, [self#translate_expr x])
     | BNot -> XOp (XBNot, [self#translate_expr x])
-    | LNot when is_pointer_type (type_of_exp fdecls x) ->
+    | LNot when TR.tfold_default is_pointer_type false (type_of_exp fdecls x) ->
       XOp (XEq, [self#translate_expr x; XConst (IntConst numerical_zero)])
     | LNot -> XOp (XLNot, [self#translate_expr x])
 
@@ -904,7 +904,8 @@ object (self)
       | CastE (_, e) -> is_zero e
       | _ -> false in
     match cond with
-    | UnOp (LNot, (Lval lval as e), _) when is_pointer_type (type_of_exp fdecls e) ->
+    | UnOp (LNot, (Lval lval as e), _)
+         when (TR.tfold_default is_pointer_type false (type_of_exp fdecls e)) ->
        let symvar = self#translate_lhs_lval lval in
        if symvar#isTmp then
          (SKIP, SKIP)

CodeHawk/CHC/cchpre/cCHCreateErrnoPOs.ml

@@ -30,6 +30,7 @@ open CHPretty
 open CHUtils
 
 (* chtuil *)
+open CHLogger
 open CHTimingLog
 open CHTraceResult
 
@@ -48,9 +49,11 @@ open CCHPreTypes
 open CCHProofScaffolding
 
 module H = Hashtbl
+module TR = CHTraceResult
+
 let (let* ) x f = CHTraceResult.tbind f x
 
-let result_of_option (msg: string) (o: 'a option): ('a, string list) result = 
+let result_of_option (msg: string) (o: 'a option): ('a, string list) result =
   match o with
   | None -> Error [msg]
   | Some r -> Ok r
@@ -65,11 +68,23 @@ let is_errno_location_call (e:exp): bool =
   | _ -> false
 
 let is_int_ptr (env: cfundeclarations_int) (v: int): bool =
-  let ty = (env#get_varinfo_by_vid v).vtype in
-  let ty_unroll = CCHFileEnvironment.file_environment#get_type_unrolled ty in
-  match ty_unroll with
-  | TPtr (TInt _, _) -> true
-  | _ -> false
+  TR.tfold
+    ~ok:(fun vinfo ->
+      let ty = vinfo.vtype in
+      let ty_unroll = CCHFileEnvironment.file_environment#get_type_unrolled ty in
+      match ty_unroll with
+      | TPtr (TInt _, _) -> true
+      | _ -> false)
+    ~error:(fun err ->
+      begin
+        log_error_result
+          ~tag:"is_int_ptr"
+          ~msg:env#functionname
+          __FILE__ __LINE__
+          [String.concat ", " err];
+        false
+      end)
+    (env#get_varinfo_by_vid v)
 
 (* Collect all pointers `x` from a target expression that have non-deref uses *)
 class pointer_use_expr_walker_t (env:cfundeclarations_int) =
@@ -93,9 +108,9 @@ let blacklistable_pointers_of_exp (env: cfundeclarations_int) (e: exp): int list
   let walker = new pointer_use_expr_walker_t env in
   let _ = walker#walk_exp e in
   walker#get_vars
-  
-(* Collect all variables that must alias __errno_location(). This fails if 
-   we see anything that makes this analysis non-trivial, 
+
+(* Collect all variables that must alias __errno_location(). This fails if
+   we see anything that makes this analysis non-trivial,
    like x = __errno_location(); y = x; ... *)
 class errno_location_block_walker_t (env:cfundeclarations_int) =
 object (self)
@@ -104,29 +119,29 @@ object (self)
   (* vids *)
   val errno_pointers = new IntCollections.set_t
 
-  (* 
+  (*
      These are vids of pointers, x, whose uses in the program are anything _EXCEPT_
      1) x = __errno_location()
      2) *x
 
      e.g. the following instructions or expressions would result in adding x
      to this set:
-     y = x, x + 1, 
+     y = x, x + 1,
   *)
   val blacklist_pointers = new IntCollections.set_t
 
   method invalid_errno_uses: IntCollections.set_t =
      errno_pointers#inter blacklist_pointers
-  
+
   method errno_pointers: IntCollections.set_t = errno_pointers
 
   method! walk_instr (i:instr) =
     match i with
-    | Call (Some (Var x, _), f, [], _) when is_errno_location_call f -> 
+    | Call (Some (Var x, _), f, [], _) when is_errno_location_call f ->
       self#add_errno_pointer (snd x);
       super#walk_instr i
 
-    | _ -> 
+    | _ ->
       super#walk_instr i
 
   method! walk_rhs (e:exp) = self#blacklist_exp_ptrs e
@@ -146,15 +161,15 @@ object (self)
 end
 
 (* Check that we can easily track aliases of __errno_location() *)
-let check_errno_pointer_uses_in_block (env: cfundeclarations_int) (b: block) = 
+let check_errno_pointer_uses_in_block (env: cfundeclarations_int) (b: block) =
   let block_walker = new errno_location_block_walker_t env in
   let _ = block_walker#walk_block b in
   if (block_walker#invalid_errno_uses)#isEmpty then
     Some (block_walker#errno_pointers)
   else
     None
 
-(* At every *read* of errno, check that we *must* observe a known local write, where 
+(* At every *read* of errno, check that we *must* observe a known local write, where
    such a write is either:
    1) a direct assignment (e.g. errno = 0)
    2) a write due to a library call (e.g. fopen in the branch where fopen returned NULL)
@@ -169,7 +184,7 @@ object (self)
     self#create_po_block (mk_program_context ()) self#f.sbody
 
   method private create_po_block (context: program_context_int) (b: block): unit=
-    List.iter (fun s -> self#create_po_stmt (context#add_stmt s.sid) s) b.bstmts 
+    List.iter (fun s -> self#create_po_stmt (context#add_stmt s.sid) s) b.bstmts
 
   method private create_po_stmt (context: program_context_int) (s: stmt): unit =
     self#create_po_stmtkind context s.skind
@@ -203,33 +218,33 @@ object (self)
   | Break _
   | Continue _
   | Goto _ -> ()
-  | TryFinally _ 
+  | TryFinally _
   | TryExcept _  ->
     pr_debug [ STR "Errno analysis does not currently support TryFinally or TryExcept "]
 
   method private create_po_instr (context: program_context_int) (i: instr): unit =
     match i with
     | Set (_, e, loc) -> self#create_po_exp context#add_rhs e loc
-    | Call (ret, callee, args, loc) -> 
+    | Call (ret, callee, args, loc) ->
       begin
         self#create_po_exp context#add_ftarget callee loc;
         (match ret with
         | None -> ()
         | Some r -> self#create_po_lval context#add_lhs r loc);
         List.iteri (fun i e -> self#create_po_exp (context#add_arg (i+1)) e loc) args;
       end
-    | VarDecl _ 
+    | VarDecl _
     | Asm _ -> ()
 
   method create_po_exp (context: program_context_int) (e: exp) (loc: location) =
     match e with
-    | Lval (Mem (Lval (Var x, NoOffset)), NoOffset) when errno_aliases#has (snd x) -> 
+    | Lval (Mem (Lval (Var x, NoOffset)), NoOffset) when errno_aliases#has (snd x) ->
       self#add_ppo PErrnoWritten loc context;
     | Lval (Mem e, _) -> self#create_po_exp context#add_lval#add_mem e loc
     | Lval (Var _, _) -> ()
     | UnOp (_, e, _) -> self#create_po_exp context#add_unop e loc
-    | BinOp (_, e1, e2, _) -> 
-      begin 
+    | BinOp (_, e1, e2, _) ->
+      begin
         self#create_po_exp (context#add_binop 1) e1 loc;
         self#create_po_exp (context#add_binop 2) e2 loc;
       end
@@ -252,7 +267,7 @@ object (self)
     | AddrOfLabel _
     | SizeOfE _ -> ()
 
-  method private create_po_lval context lval loc: unit = 
+  method private create_po_lval context lval loc: unit =
     match lval with
     | (Var _, _) -> ()
     | (Mem e, _) -> self#create_po_exp context#add_mem e loc
@@ -268,7 +283,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 _ = read_proof_files fname fundec.sdecls in
-  let* errnos = check_errno_pointer_uses_in_block fundec.sdecls fundec.sbody 
+  let* errnos = check_errno_pointer_uses_in_block fundec.sdecls fundec.sbody
              |> result_of_option "Can not run errno analysis, found code we can not analyze"
   in
   let _ = (new po_creator_t fundec errnos)#create_proof_obligations in