Use speculative comp wrapper instead of threading checkbounds through funs

Author: karoliineh

src/analyses/base.ml

@@ -523,18 +523,18 @@ struct
       CPA.find x st.cpa
     end
 
-  let rec get_mval ~man ?(full=false) ?(checkBounds=true) (st: store) ((x, offs): Addr.Mval.t) (exp:exp option) =
+  let rec get_mval ~man ?(full=false) (st: store) ((x, offs): Addr.Mval.t) (exp:exp option) =
     (* get hold of the variable value, either from local or global state *)
     let var = get_var ~man st x in
-    let v = VD.eval_offset ~checkBounds (Queries.to_value_domain_ask (Analyses.ask_of_man man)) (fun x -> get ~man st x exp) var offs exp (Some (Var x, Offs.to_cil_offset offs)) x.vtype in
+    let v = VD.eval_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) (fun x -> get ~man st x exp) var offs exp (Some (Var x, Offs.to_cil_offset offs)) x.vtype in
     if M.tracing then M.tracec "get" "var = %a, %a = %a" VD.pretty var AD.pretty (AD.of_mval (x, offs)) VD.pretty v;
     if full then var else match v with
       | Blob (c,s,_) -> c
       | x -> x
 
-  and get_addr ~man ?(top=VD.top ()) ?full ?(checkBounds=true) (st: store) (addr: Addr.t) (exp:exp option) =
+  and get_addr ~man ?(top=VD.top ()) ?full (st: store) (addr: Addr.t) (exp:exp option) =
     match addr with
-    | Addr.Addr mval -> get_mval ~man ?full ~checkBounds st mval exp
+    | Addr.Addr mval -> get_mval ~man ?full st mval exp
     | Addr.NullPtr ->
       begin match get_string "sem.null-pointer.dereference" with
         | "assume_none" -> VD.bot ()
@@ -603,7 +603,7 @@ struct
     | Union (f,e) -> reachable_from_value ask e t description
     (* For arrays, we ask to read from an unknown index, this will cause it
      * join all its values. *)
-    | Array a -> reachable_from_value ask (ValueDomain.CArrays.get ~checkBounds:false (Queries.to_value_domain_ask ask) a (None, ValueDomain.ArrIdxDomain.top ())) t description
+    | Array a -> reachable_from_value ask (ValueDomain.CArrays.get (Queries.to_value_domain_ask ask) a (None, ValueDomain.ArrIdxDomain.top ())) t description
     | Blob (e,_,_) -> reachable_from_value ask e t description
     | Struct s -> ValueDomain.Structs.fold (fun k v acc -> AD.join (reachable_from_value ask v t description) acc) s empty
     | Int _ -> empty
@@ -613,12 +613,17 @@ struct
     | JmpBuf _ -> empty (* Jump buffers are abstract and nothing known can be reached from them *)
     | Mutex -> empty (* mutexes are abstract and nothing known can be reached from them *)
 
+  let reachable_from_value ask (value: value) (t: typ) (description: string) =
+    let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
+    reachable_from_value ask value t description
+
   (* Get the list of addresses accessible immediately from a given address, thus
    * all pointers within a structure should be considered, but we don't follow
    * pointers. We return a flattend representation, thus simply an address (set). *)
   let reachable_from_addr ~man st (addr: Addr.t): address =
+    let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
     if M.tracing then M.tracei "reachability" "Checking for %a" Addr.pretty addr;
-    let res = reachable_from_value (Analyses.ask_of_man man) (get_addr ~man ~checkBounds:false st addr None) (Addr.type_of addr) (Addr.show addr) in
+    let res = reachable_from_value (Analyses.ask_of_man man) (get_addr ~man st addr None) (Addr.type_of addr) (Addr.show addr) in
     if M.tracing then M.traceu "reachability" "Reachable addresses: %a" AD.pretty res;
     res
 
@@ -696,6 +701,7 @@ struct
 
 
   let reachable_top_pointers_types man (ps: AD.t) : Queries.TS.t =
+    let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
     let module TS = Queries.TS in
     let empty = AD.empty () in
     let reachable_from_address (adr: address) =
@@ -721,7 +727,7 @@ struct
         | Address adrs when AD.is_top adrs -> (empty,TS.bot (), true)
         | Address adrs -> (adrs,TS.bot (), AD.may_be_unknown adrs)
         | Union (t,e) -> with_field (reachable_from_value e) t
-        | Array a -> reachable_from_value (ValueDomain.CArrays.get ~checkBounds:false (Queries.to_value_domain_ask (Analyses.ask_of_man man)) a (None, ValueDomain.ArrIdxDomain.top ()))
+        | Array a -> reachable_from_value (ValueDomain.CArrays.get (Queries.to_value_domain_ask (Analyses.ask_of_man man)) a (None, ValueDomain.ArrIdxDomain.top ()))
         | Blob (e,_,_) -> reachable_from_value e
         | Struct s ->
           let join_tr (a1,t1,_) (a2,t2,_) = AD.join a1 a2, TS.join t1 t2, false in

src/cdomain/value/cdomains/arrayDomain.ml

@@ -802,7 +802,9 @@ end
 
 (* This is the main array out of bounds check *)
 let array_oob_check ( type a ) (module Idx: IntDomain.Z with type t = a) (x, l) (e, v) =
-  if GobConfig.get_bool "ana.arrayoob" then (* The purpose of the following 2 lines is to give the user extra info about the array oob *)
+  if !AnalysisState.executing_speculative_computations then
+    ()
+  else if GobConfig.get_bool "ana.arrayoob" then (* The purpose of the following 2 lines is to give the user extra info about the array oob *)
     let idx_before_end = Idx.lt v l in (* check whether index is before the end of the array *)
     let idx_after_start = Idx.ge v (Idx.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero) in (* check whether the index is non-negative *)
     (* For an explanation of the warning types check the Pull Request #255 *)

src/cdomain/value/cdomains/valueDomain.ml

@@ -17,7 +17,7 @@ module type S =
 sig
   include Lattice.S
   type offs
-  val eval_offset: ?checkBounds:bool -> VDQ.t -> (AD.t -> t) -> t-> offs -> exp option -> lval option -> typ -> t
+  val eval_offset: VDQ.t -> (AD.t -> t) -> t-> offs -> exp option -> lval option -> typ -> t
   val update_offset: ?blob_destructive:bool -> VDQ.t -> t -> offs -> t -> exp option -> lval -> typ -> t
   val update_array_lengths: (exp -> t) -> t -> Cil.typ -> t
   val affect_move: ?replace_with_const:bool -> VDQ.t -> t -> varinfo -> (exp -> int option) -> t
@@ -901,7 +901,7 @@ struct
       x (* This already contains some value *)
 
   (* Funny, this does not compile without the final type annotation! *)
-  let rec eval_offset ?(checkBounds=true) (ask: VDQ.t) f (x: t) (offs:offs) (exp:exp option) (v:lval option) (t:typ): t =
+  let rec eval_offset (ask: VDQ.t) f (x: t) (offs:offs) (exp:exp option) (v:lval option) (t:typ): t =
     let rec do_eval_offset (x:t) (offs:offs) (l:lval option) (o:offset option): t =
       if M.tracing then M.traceli "eval_offset" "do_eval_offset %a %a (%a)" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp;
       let r =
@@ -958,7 +958,7 @@ struct
               match x with
               | Array x ->
                 let e = determine_offset ask l o exp v in
-                do_eval_offset (CArrays.get ~checkBounds ask x (e, idx)) offs l' o'
+                do_eval_offset (CArrays.get ask x (e, idx)) offs l' o'
               | Address _ ->
                 begin
                   do_eval_offset x offs l' o' (* this used to be `blob `address -> we ignore the index *)