diff --git a/src/analyses/base.ml b/src/analyses/base.ml index c66b53320e..42e43b623a 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -243,7 +243,7 @@ struct | _ -> false (* Evaluate binop for two abstract values: *) - let evalbinop_base (a: Q.ask) (st: store) (op: binop) (t1:typ) (a1:value) (t2:typ) (a2:value) (t:typ) :value = + let evalbinop_base ~ctx (op: binop) (t1:typ) (a1:value) (t2:typ) (a2:value) (t:typ) :value = if M.tracing then M.tracel "eval" "evalbinop %a %a %a\n" d_binop op VD.pretty a1 VD.pretty a2; (* We define a conversion function for the easy cases when we can just use * the integer domain operations. *) @@ -340,7 +340,7 @@ struct let ax = AD.choose x in let ay = AD.choose y in let handle_address_is_multiple addr = begin match Addr.to_var addr with - | Some v when a.f (Q.IsMultiple v) -> + | Some v when ctx.ask (Q.IsMultiple v) -> if M.tracing then M.tracel "addr" "IsMultiple %a\n" CilType.Varinfo.pretty v; None | _ -> @@ -437,9 +437,10 @@ struct let publish_all ctx reason = ignore (sync' reason ctx) - let get_var (a: Q.ask) (gs: glob_fun) (st: store) (x: varinfo): value = - if (!earlyglobs || ThreadFlag.has_ever_been_multi a) && is_global a x then - Priv.read_global a (priv_getg gs) st x + let get_var ~ctx (st: store) (x: varinfo): value = + let ask = Analyses.ask_of_ctx ctx in + if (!earlyglobs || ThreadFlag.has_ever_been_multi ask) && is_global ask x then + Priv.read_global ask (priv_getg ctx.global) st x else begin if M.tracing then M.tracec "get" "Singlethreaded mode.\n"; CPA.find x st.cpa @@ -449,7 +450,7 @@ struct * adding proper dependencies. * For the exp argument it is always ok to put None. This means not using precise information about * which part of an array is involved. *) - let rec get ?(top=VD.top ()) ?(full=false) a (gs: glob_fun) (st: store) (addrs:address) (exp:exp option): value = + let rec get ~ctx ?(top=VD.top ()) ?(full=false) (st: store) (addrs:address) (exp:exp option): value = let at = AD.type_of addrs in let firstvar = if M.tracing then match AD.to_var_may addrs with [] -> "" | x :: _ -> x.vname else "" in if M.tracing then M.traceli "get" ~var:firstvar "Address: %a\nState: %a\n" AD.pretty addrs CPA.pretty st.cpa; @@ -457,8 +458,8 @@ struct let res = let f_addr (x, offs) = (* get hold of the variable value, either from local or global state *) - let var = get_var a gs st x in - let v = VD.eval_offset (Queries.to_value_domain_ask a) (fun x -> get a gs st x exp) var offs exp (Some (Var x, Offs.to_cil_offset offs)) x.vtype in + let var = get_var ~ctx st x in + let v = VD.eval_offset (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) (fun x -> get ~ctx 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\n" 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 @@ -506,7 +507,7 @@ struct in List.fold_right f vals [] - let rec reachable_from_value (ask: Q.ask) (gs:glob_fun) st (value: value) (t: typ) (description: string) = + let rec reachable_from_value ask (value: value) (t: typ) (description: string) = let empty = AD.empty () in if M.tracing then M.trace "reachability" "Checking value %a\n" VD.pretty value; match value with @@ -518,12 +519,12 @@ struct (* The main thing is to track where pointers go: *) | Address adrs -> AD.remove Addr.NullPtr adrs (* Unions are easy, I just ingore the type info. *) - | Union (f,e) -> reachable_from_value ask gs st e t description + | 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 gs st (ValueDomain.CArrays.get (Queries.to_value_domain_ask ask) a (None, ValueDomain.ArrIdxDomain.top ())) t description - | Blob (e,_,_) -> reachable_from_value ask gs st e t description - | Struct s -> ValueDomain.Structs.fold (fun k v acc -> AD.join (reachable_from_value ask gs st v t description) acc) s empty + | 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 | Float _ -> empty | MutexAttr _ -> empty @@ -534,9 +535,9 @@ struct (* Get the list of addresses accessable 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_address (ask: Q.ask) (gs:glob_fun) st (adr: address): address = + let reachable_from_address ~ctx st (adr: address): address = if M.tracing then M.tracei "reachability" "Checking for %a\n" AD.pretty adr; - let res = reachable_from_value ask gs st (get ask gs st adr None) (AD.type_of adr) (AD.show adr) in + let res = reachable_from_value (Analyses.ask_of_ctx ctx) (get ~ctx st adr None) (AD.type_of adr) (AD.show adr) in if M.tracing then M.traceu "reachability" "Reachable addresses: %a\n" AD.pretty res; res @@ -544,7 +545,7 @@ struct * This section is very confusing, because I use the same construct, a set of * addresses, as both AD elements abstracting individual (ambiguous) addresses * and the workset of visited addresses. *) - let reachable_vars (ask: Q.ask) (args: address list) (gs:glob_fun) (st: store): address list = + let reachable_vars ~ctx (st: store) (args: address list): address list = if M.tracing then M.traceli "reachability" "Checking reachable arguments from [%a]!\n" (d_list ", " AD.pretty) args; let empty = AD.empty () in (* We begin looking at the parameters: *) @@ -557,7 +558,7 @@ struct (* ok, let's visit all the variables in the workset and collect the new variables *) let visit_and_collect var (acc: address): address = let var = AD.singleton var in (* Very bad hack! Pathetic really! *) - AD.union (reachable_from_address ask gs st var) acc in + AD.union (reachable_from_address ~ctx st var) acc in let collected = AD.fold visit_and_collect !workset empty in (* And here we remove the already visited variables *) workset := AD.diff collected !visited @@ -566,7 +567,7 @@ struct if M.tracing then M.traceu "reachability" "All reachable vars: %a\n" AD.pretty !visited; List.map AD.singleton (AD.elements !visited) - let reachable_vars ask args gs st = Timing.wrap "reachability" (reachable_vars ask args gs) st + let reachable_vars ~ctx st args = Timing.wrap "reachability" (reachable_vars ~ctx st) args let drop_non_ptrs (st:CPA.t) : CPA.t = if CPA.is_top st then st else @@ -653,7 +654,7 @@ struct | JmpBuf _ -> (empty, TS.bot (), false) (* TODO: is this right? *) | Mutex -> (empty, TS.bot (), false) (* TODO: is this right? *) in - reachable_from_value (get (Analyses.ask_of_ctx ctx) ctx.global ctx.local adr None) + reachable_from_value (get ~ctx ctx.local adr None) in let visited = ref empty in let work = ref ps in @@ -673,14 +674,14 @@ struct !collected (* The evaluation function as mutually recursive eval_lv & eval_rv *) - let rec eval_rv (a: Q.ask) (gs:glob_fun) (st: store) (exp:exp): value = + let rec eval_rv ~(ctx: _ ctx) (st: store) (exp:exp): value = if M.tracing then M.traceli "evalint" "base eval_rv %a\n" d_exp exp; let r = (* we have a special expression that should evaluate to top ... *) if exp = MyCFG.unknown_exp then VD.top () else - eval_rv_ask_evalint a gs st exp + eval_rv_ask_evalint ~ctx st exp in if M.tracing then M.traceu "evalint" "base eval_rv %a -> %a\n" d_exp exp VD.pretty r; r @@ -689,14 +690,14 @@ struct Base itself also answers EvalInt, so recursion goes indirectly through queries. This allows every subexpression to also meet more precise value from other analyses. Non-integer expression just delegate to next eval_rv function. *) - and eval_rv_ask_evalint a gs st exp = - let eval_next () = eval_rv_no_ask_evalint a gs st exp in + and eval_rv_ask_evalint ~ctx st exp = + let eval_next () = eval_rv_no_ask_evalint ~ctx st exp in if M.tracing then M.traceli "evalint" "base eval_rv_ask_evalint %a\n" d_exp exp; let r:value = match Cilfacade.typeOf exp with | typ when Cil.isIntegralType typ && not (Cil.isConstant exp) -> (* don't EvalInt integer constants, base can do them precisely itself *) if M.tracing then M.traceli "evalint" "base ask EvalInt %a\n" d_exp exp; - let a = a.f (Q.EvalInt exp) in (* through queries includes eval_next, so no (exponential) branching is necessary *) + let a = ctx.ask (Q.EvalInt exp) in (* through queries includes eval_next, so no (exponential) branching is necessary *) if M.tracing then M.traceu "evalint" "base ask EvalInt %a -> %a\n" d_exp exp Queries.ID.pretty a; begin match a with | `Bot -> eval_next () (* Base EvalInt returns bot on incorrect type (e.g. pthread_t); ignore and continue. *) @@ -713,24 +714,24 @@ struct (** Evaluate expression without EvalInt query on outermost expression. This is used by base responding to EvalInt to immediately directly avoid EvalInt query cycle, which would return top. Recursive [eval_rv] calls on subexpressions still go through [eval_rv_ask_evalint]. *) - and eval_rv_no_ask_evalint a gs st exp = - eval_rv_base a gs st exp (* just as alias, so query doesn't weirdly have to call eval_rv_base *) + and eval_rv_no_ask_evalint ~ctx st exp = + eval_rv_base ~ctx st exp (* just as alias, so query doesn't weirdly have to call eval_rv_base *) - and eval_rv_back_up a gs st exp = + and eval_rv_back_up ~ctx st exp = if get_bool "ana.base.eval.deep-query" then - eval_rv a gs st exp + eval_rv ~ctx st exp else ( (* duplicate unknown_exp check from eval_rv since we're bypassing it now *) if exp = MyCFG.unknown_exp then VD.top () else - eval_rv_base a gs st exp (* bypass all queries *) + eval_rv_base ~ctx st exp (* bypass all queries *) ) (** Evaluate expression structurally by base. This handles constants directly and variables using CPA. Subexpressions delegate to [eval_rv], which may use queries on them. *) - and eval_rv_base (a: Q.ask) (gs:glob_fun) (st: store) (exp:exp): value = + and eval_rv_base ~ctx (st: store) (exp:exp): value = let eval_rv = eval_rv_back_up in if M.tracing then M.traceli "evalint" "base eval_rv_base %a\n" d_exp exp; let binop_remove_same_casts ~extra_is_safe ~e1 ~e2 ~t1 ~t2 ~c1 ~c2 = @@ -752,7 +753,7 @@ struct match constFold true exp with (* Integer literals *) (* seems like constFold already converts CChr to CInt *) - | Const (CChr x) -> eval_rv a gs st (Const (charConstToInt x)) (* char becomes int, see Cil doc/ISO C 6.4.4.4.10 *) + | Const (CChr x) -> eval_rv ~ctx st (Const (charConstToInt x)) (* char becomes int, see Cil doc/ISO C 6.4.4.4.10 *) | Const (CInt (num,ikind,str)) -> (match str with Some x -> M.tracel "casto" "CInt (%s, %a, %s)\n" (Z.to_string num) d_ikind ikind x | None -> ()); Int (ID.cast_to ikind (IntDomain.of_const (num,ikind,str))) @@ -768,21 +769,21 @@ struct | Const _ -> VD.top () (* Variables and address expressions *) | Lval lv -> - eval_rv_base_lval ~eval_lv a gs st exp lv + eval_rv_base_lval ~eval_lv ~ctx st exp lv (* Binary operators *) (* Eq/Ne when both values are equal and casted to the same type *) | BinOp ((Eq | Ne) as op, (CastE (t1, e1) as c1), (CastE (t2, e2) as c2), typ) when typeSig t1 = typeSig t2 -> - let a1 = eval_rv a gs st e1 in - let a2 = eval_rv a gs st e2 in + let a1 = eval_rv ~ctx st e1 in + let a2 = eval_rv ~ctx st e2 in let extra_is_safe = - match evalbinop_base a st op t1 a1 t2 a2 typ with + match evalbinop_base ~ctx op t1 a1 t2 a2 typ with | Int i -> ID.to_bool i = Some true | _ | exception IntDomain.IncompatibleIKinds _ -> false in let (e1, e2) = binop_remove_same_casts ~extra_is_safe ~e1 ~e2 ~t1 ~t2 ~c1 ~c2 in (* re-evaluate e1 and e2 in evalbinop because might be with cast *) - evalbinop a gs st op ~e1 ~t1 ~e2 ~t2 typ + evalbinop ~ctx st op ~e1 ~t1 ~e2 ~t2 typ | BinOp (LOr, e1, e2, typ) as exp -> let open GobOption.Syntax in (* split nested LOr Eqs to equality pairs, if possible *) @@ -815,8 +816,8 @@ struct let eqs_value: value option = let* eqs = split exp in let* (e, es) = find_common eqs in - let v = eval_rv a gs st e in (* value of common exp *) - let vs = List.map (eval_rv a gs st) es in (* values of other sides *) + let v = eval_rv ~ctx st e in (* value of common exp *) + let vs = List.map (eval_rv ~ctx st) es in (* values of other sides *) let ik = Cilfacade.get_ikind typ in match v with | Address a -> @@ -858,25 +859,25 @@ struct in begin match eqs_value with | Some x -> x - | None -> evalbinop a gs st LOr ~e1 ~e2 typ (* fallback to general case *) + | None -> evalbinop ~ctx st LOr ~e1 ~e2 typ (* fallback to general case *) end | BinOp (op,e1,e2,typ) -> - evalbinop a gs st op ~e1 ~e2 typ + evalbinop ~ctx st op ~e1 ~e2 typ (* Unary operators *) | UnOp (op,arg1,typ) -> - let a1 = eval_rv a gs st arg1 in + let a1 = eval_rv ~ctx st arg1 in evalunop op typ a1 (* The &-operator: we create the address abstract element *) - | AddrOf lval -> Address (eval_lv a gs st lval) + | AddrOf lval -> Address (eval_lv ~ctx st lval) (* CIL's very nice implicit conversion of an array name [a] to a pointer * to its first element [&a[0]]. *) | StartOf lval -> let array_ofs = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset) in let array_start = add_offset_varinfo array_ofs in - Address (AD.map array_start (eval_lv a gs st lval)) - | CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv a gs st (Const (CStr (x,e))) (* TODO safe? *) + Address (AD.map array_start (eval_lv ~ctx st lval)) + | CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~ctx st (Const (CStr (x,e))) (* TODO safe? *) | CastE (t, exp) -> - let v = eval_rv a gs st exp in + let v = eval_rv ~ctx st exp in VD.cast ~torg:(Cilfacade.typeOf exp) t v | SizeOf _ | Real _ @@ -892,10 +893,10 @@ struct if M.tracing then M.traceu "evalint" "base eval_rv_base %a -> %a\n" d_exp exp VD.pretty r; r - and eval_rv_base_lval ~eval_lv (a: Q.ask) (gs:glob_fun) (st: store) (exp: exp) (lv: lval): value = + and eval_rv_base_lval ~eval_lv ~ctx (st: store) (exp: exp) (lv: lval): value = match lv with - | (Var v, ofs) -> get a gs st (eval_lv a gs st (Var v, ofs)) (Some exp) - (*| Lval (Mem e, ofs) -> get a gs st (eval_lv a gs st (Mem e, ofs)) *) + | (Var v, ofs) -> get ~ctx st (eval_lv ~ctx st (Var v, ofs)) (Some exp) + (* | Lval (Mem e, ofs) -> get ~ctx st (eval_lv ~ctx (Mem e, ofs)) *) | (Mem e, ofs) -> (*M.tracel "cast" "Deref: lval: %a\n" d_plainlval lv;*) let rec contains_vla (t:typ) = match t with @@ -907,7 +908,7 @@ struct in let b = Mem e, NoOffset in (* base pointer *) let t = Cilfacade.typeOfLval b in (* static type of base *) - let p = eval_lv a gs st b in (* abstract base addresses *) + let p = eval_lv ~ctx st b in (* abstract base addresses *) (* pre VLA: *) (* let cast_ok = function Addr a -> sizeOf t <= sizeOf (get_type_addr a) | _ -> false in *) let cast_ok a = @@ -939,35 +940,35 @@ struct let lookup_with_offs addr = let v = (* abstract base value *) if cast_ok addr then - get ~top:(VD.top_value t) a gs st (AD.singleton addr) (Some exp) (* downcasts are safe *) + get ~ctx ~top:(VD.top_value t) st (AD.singleton addr) (Some exp) (* downcasts are safe *) else VD.top () (* upcasts not! *) in let v' = VD.cast t v in (* cast to the expected type (the abstract type might be something other than t since we don't change addresses upon casts!) *) if M.tracing then M.tracel "cast" "Ptr-Deref: cast %a to %a = %a!\n" VD.pretty v d_type t VD.pretty v'; - let v' = VD.eval_offset (Queries.to_value_domain_ask a) (fun x -> get a gs st x (Some exp)) v' (convert_offset a gs st ofs) (Some exp) None t in (* handle offset *) + let v' = VD.eval_offset (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) (fun x -> get ~ctx st x (Some exp)) v' (convert_offset ~ctx st ofs) (Some exp) None t in (* handle offset *) v' in AD.fold (fun a acc -> VD.join acc (lookup_with_offs a)) p (VD.bot ()) - and evalbinop (a: Q.ask) (gs:glob_fun) (st: store) (op: binop) ~(e1:exp) ?(t1:typ option) ~(e2:exp) ?(t2:typ option) (t:typ): value = - evalbinop_mustbeequal a gs st op ~e1 ?t1 ~e2 ?t2 t + and evalbinop ~ctx (st: store) (op: binop) ~(e1:exp) ?(t1:typ option) ~(e2:exp) ?(t2:typ option) (t:typ): value = + evalbinop_mustbeequal ~ctx st op ~e1 ?t1 ~e2 ?t2 t (** Evaluate BinOp using MustBeEqual query as fallback. *) - and evalbinop_mustbeequal (a: Q.ask) (gs:glob_fun) (st: store) (op: binop) ~(e1:exp) ?(t1:typ option) ~(e2:exp) ?(t2:typ option) (t:typ): value = + and evalbinop_mustbeequal ~ctx (st: store) (op: binop) ~(e1:exp) ?(t1:typ option) ~(e2:exp) ?(t2:typ option) (t:typ): value = (* Evaluate structurally using base at first. *) - let a1 = eval_rv a gs st e1 in - let a2 = eval_rv a gs st e2 in + let a1 = eval_rv ~ctx st e1 in + let a2 = eval_rv ~ctx st e2 in let t1 = Option.default_delayed (fun () -> Cilfacade.typeOf e1) t1 in let t2 = Option.default_delayed (fun () -> Cilfacade.typeOf e2) t2 in - let r = evalbinop_base a st op t1 a1 t2 a2 t in + let r = evalbinop_base ~ctx op t1 a1 t2 a2 t in if Cil.isIntegralType t then ( match r with | Int i when ID.to_int i <> None -> r (* Avoid fallback, cannot become any more precise. *) | _ -> (* Fallback to MustBeEqual query, could get extra precision from exprelation/var_eq. *) let must_be_equal () = - let r = Q.must_be_equal a e1 e2 in + let r = Q.must_be_equal (Analyses.ask_of_ctx ctx) e1 e2 in if M.tracing then M.tracel "query" "MustBeEqual (%a, %a) = %b\n" d_exp e1 d_exp e2 r; r in @@ -996,48 +997,48 @@ struct (* A hackish evaluation of expressions that should immediately yield an * address, e.g. when calling functions. *) - and eval_fv a (gs:glob_fun) st (exp:exp): AD.t = + and eval_fv ~ctx st (exp:exp): AD.t = match exp with - | Lval lval -> eval_lv a gs st lval - | _ -> eval_tv a gs st exp + | Lval lval -> eval_lv ~ctx st lval + | _ -> eval_tv ~ctx st exp (* Used also for thread creation: *) - and eval_tv a (gs:glob_fun) st (exp:exp): AD.t = - match (eval_rv a gs st exp) with + and eval_tv ~ctx st (exp:exp): AD.t = + match eval_rv ~ctx st exp with | Address x -> x | _ -> failwith "Problems evaluating expression to function calls!" - and eval_int a gs st exp = - match eval_rv a gs st exp with + and eval_int ~ctx st exp = + match eval_rv ~ctx st exp with | Int x -> x | _ -> ID.top_of (Cilfacade.get_ikind_exp exp) (* A function to convert the offset to our abstract representation of * offsets, i.e. evaluate the index expression to the integer domain. *) - and convert_offset a (gs:glob_fun) (st: store) (ofs: offset) = + and convert_offset ~ctx (st: store) (ofs: offset) = let eval_rv = eval_rv_back_up in match ofs with | NoOffset -> `NoOffset - | Field (fld, ofs) -> `Field (fld, convert_offset a gs st ofs) + | Field (fld, ofs) -> `Field (fld, convert_offset ~ctx st ofs) | Index (exp, ofs) when CilType.Exp.equal exp Offset.Index.Exp.any -> (* special offset added by convertToQueryLval *) - `Index (IdxDom.top (), convert_offset a gs st ofs) + `Index (IdxDom.top (), convert_offset ~ctx st ofs) | Index (exp, ofs) -> - match eval_rv a gs st exp with - | Int i -> `Index (iDtoIdx i, convert_offset a gs st ofs) - | Address add -> `Index (AD.to_int add, convert_offset a gs st ofs) - | Top -> `Index (IdxDom.top (), convert_offset a gs st ofs) - | Bot -> `Index (IdxDom.bot (), convert_offset a gs st ofs) + match eval_rv ~ctx st exp with + | Int i -> `Index (iDtoIdx i, convert_offset ~ctx st ofs) + | Address add -> `Index (AD.to_int add, convert_offset ~ctx st ofs) + | Top -> `Index (IdxDom.top (), convert_offset ~ctx st ofs) + | Bot -> `Index (IdxDom.bot (), convert_offset ~ctx st ofs) | _ -> failwith "Index not an integer value" (* Evaluation of lvalues to our abstract address domain. *) - and eval_lv (a: Q.ask) (gs:glob_fun) st (lval:lval): AD.t = + and eval_lv ~ctx st (lval:lval): AD.t = let eval_rv = eval_rv_back_up in match lval with (* The simpler case with an explicit variable, e.g. for [x.field] we just * create the address { (x,field) } *) | Var x, ofs -> - AD.singleton (Addr.of_mval (x, convert_offset a gs st ofs)) + AD.singleton (Addr.of_mval (x, convert_offset ~ctx st ofs)) (* The more complicated case when [exp = & x.field] and we are asked to * evaluate [(\*exp).subfield]. We first evaluate [exp] to { (x,field) } * and then add the subfield to it: { (x,field.subfield) }. *) | Mem n, ofs -> begin - match (eval_rv a gs st n) with + match eval_rv ~ctx st n with | Address adr -> ( if AD.is_null adr then ( @@ -1050,14 +1051,14 @@ struct ); (* Warn if any of the addresses contains a non-local and non-global variable *) if AD.exists (function - | AD.Addr.Addr (v, _) -> not (CPA.mem v st.cpa) && not (is_global a v) + | AD.Addr.Addr (v, _) -> not (CPA.mem v st.cpa) && not (is_global (Analyses.ask_of_ctx ctx) v) | _ -> false ) adr then ( AnalysisStateUtil.set_mem_safety_flag InvalidDeref; M.warn "lval %a points to a non-local variable. Invalid pointer dereference may occur" d_lval lval ) ); - AD.map (add_offset_varinfo (convert_offset a gs st ofs)) adr + AD.map (add_offset_varinfo (convert_offset ~ctx st ofs)) adr | _ -> M.debug ~category:Analyzer "Failed evaluating %a to lvalue" d_lval lval; AD.unknown_ptr @@ -1069,17 +1070,17 @@ struct (* run eval_rv from above, but change bot to top to be sound for programs with undefined behavior. *) (* Previously we only gave sound results for programs without undefined behavior, so yielding bot for accessing an uninitialized array was considered ok. Now only [invariant] can yield bot/Deadcode if the condition is known to be false but evaluating an expression should not be bot. *) - let eval_rv (a: Q.ask) (gs:glob_fun) (st: store) (exp:exp): value = + let eval_rv ~ctx (st: store) (exp:exp): value = try - let r = eval_rv a gs st exp in + let r = eval_rv ~ctx st exp in if M.tracing then M.tracel "eval" "eval_rv %a = %a\n" d_exp exp VD.pretty r; if VD.is_bot r then VD.top_value (Cilfacade.typeOf exp) else r with IntDomain.ArithmeticOnIntegerBot _ -> ValueDomain.Compound.top_value (Cilfacade.typeOf exp) - let query_evalint ask gs st e = + let query_evalint ~ctx st e = if M.tracing then M.traceli "evalint" "base query_evalint %a\n" d_exp e; - let r = match eval_rv_no_ask_evalint ask gs st e with + let r = match eval_rv_no_ask_evalint ~ctx st e with | Int i -> `Lifted i (* cast should be unnecessary, eval_rv should guarantee right ikind already *) | Bot -> Queries.ID.top () (* out-of-scope variables cause bot, but query result should then be unknown *) | Top -> Queries.ID.top () (* some float computations cause top (57-float/01-base), but query result should then be unknown *) @@ -1099,19 +1100,32 @@ struct if Queries.Set.mem anyq asked then Queries.Result.top q (* query cycle *) else ( - let asked' = Queries.Set.add anyq asked in match q with - | EvalInt e -> query_evalint (ask asked') gs st e (* mimic EvalInt query since eval_rv needs it *) + | EvalInt e -> query_evalint ~ctx:(ctx' (Queries.Set.add anyq asked)) st e (* mimic EvalInt query since eval_rv needs it *) | _ -> Queries.Result.top q ) - and ask asked = { Queries.f = fun (type a) (q: a Queries.t) -> query asked q } (* our version of ask *) - and gs = function `Left _ -> `Lifted1 (Priv.G.top ()) | `Right _ -> `Lifted2 (VD.top ()) in (* the expression is guaranteed to not contain globals *) - match (eval_rv (ask Queries.Set.empty) gs st exp) with + and gs = function `Left _ -> `Lifted1 (Priv.G.top ()) | `Right _ -> `Lifted2 (VD.top ()) (* the expression is guaranteed to not contain globals *) + and ctx' asked = + { ask = (fun (type a) (q: a Queries.t) -> query asked q) + ; emit = (fun _ -> failwith "Cannot \"emit\" in base eval_exp context.") + ; node = MyCFG.dummy_node + ; prev_node = MyCFG.dummy_node + ; control_context = (fun () -> ctx_failwith "Base eval_exp has no context.") + ; context = (fun () -> ctx_failwith "Base eval_exp has no context.") + ; edge = MyCFG.Skip + ; local = st + ; global = gs + ; spawn = (fun ?(multiple=false) _ -> failwith "Base eval_exp should never spawn threads. What is going on?") + ; split = (fun _ -> failwith "Base eval_exp trying to split paths.") + ; sideg = (fun g d -> failwith "Base eval_exp trying to side effect.") + } + in + match eval_rv ~ctx:(ctx' Queries.Set.empty) st exp with | Int x -> ValueDomain.ID.to_int x | _ -> None let eval_funvar ctx fval: Queries.AD.t = - let fp = eval_fv (Analyses.ask_of_ctx ctx) ctx.global ctx.local fval in + let fp = eval_fv ~ctx ctx.local fval in if AD.is_top fp then ( if AD.cardinal fp = 1 then M.warn ~category:Imprecise ~tags:[Category Call] "Unknown call to function %a." d_exp fval @@ -1122,14 +1136,14 @@ struct (** Evaluate expression as address. Avoids expensive Apron EvalInt if the Int result would be useless to us anyway. *) - let eval_rv_address ask gs st e = + let eval_rv_address ~ctx st e = (* no way to do eval_rv with expected type, so filter expression beforehand *) match Cilfacade.typeOf e with | t when Cil.isArithmeticType t -> (* definitely not address *) VD.top_value t | exception Cilfacade.TypeOfError _ (* something weird, might be address *) | _ -> - eval_rv ask gs st e + eval_rv ~ctx st e (* interpreter end *) @@ -1148,7 +1162,7 @@ struct struct let context = context let scope = Node.find_fundec ctx.node - let find v = get_var ask ctx.global ctx.local v + let find v = get_var ~ctx ctx.local v end in let module I = ValueDomain.ValueInvariant (Arg) in @@ -1221,11 +1235,11 @@ struct | Q.EvalFunvar e -> eval_funvar ctx e | Q.EvalJumpBuf e -> - begin match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with + begin match eval_rv_address ~ctx ctx.local e with | Address jmp_buf -> if AD.mem Addr.UnknownPtr jmp_buf then M.warn ~category:Imprecise "Jump buffer %a may contain unknown pointers." d_exp e; - begin match get ~top:(VD.bot ()) (Analyses.ask_of_ctx ctx) ctx.global ctx.local jmp_buf None with + begin match get ~ctx ~top:(VD.bot ()) ctx.local jmp_buf None with | JmpBuf (x, copied) -> if copied then M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a contains values that were copied here instead of being set by setjmp. This is Undefined Behavior." d_exp e; @@ -1242,15 +1256,15 @@ struct JmpBufDomain.JmpBufSet.top () end | Q.EvalInt e -> - query_evalint (Analyses.ask_of_ctx ctx) ctx.global ctx.local e + query_evalint ~ctx ctx.local e | Q.EvalMutexAttr e -> begin let e:exp = Lval (Cil.mkMem ~addr:e ~off:NoOffset) in - match eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with + match eval_rv ~ctx ctx.local e with | MutexAttr a -> a | v -> MutexAttrDomain.top () end | Q.EvalLength e -> begin - match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with + match eval_rv_address ~ctx ctx.local e with | Address a -> let slen = Seq.map String.length (List.to_seq (AD.to_string a)) in let lenOf = function @@ -1265,9 +1279,9 @@ struct | _ -> Queries.Result.top q end | Q.EvalValue e -> - eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e + eval_rv ~ctx ctx.local e | Q.BlobSize {exp = e; base_address = from_base_addr} -> begin - let p = eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in + let p = eval_rv_address ~ctx ctx.local e in (* ignore @@ printf "BlobSize %a MayPointTo %a\n" d_plainexp e VD.pretty p; *) match p with | Address a -> @@ -1286,7 +1300,7 @@ struct else a in - let r = get ~full:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local a None in + let r = get ~ctx ~full:true ctx.local a None in (* ignore @@ printf "BlobSize %a = %a\n" d_plainexp e VD.pretty r; *) (match r with | Array a -> @@ -1301,14 +1315,14 @@ struct | _ -> Queries.Result.top q end | Q.MayPointTo e -> begin - match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with + match eval_rv_address ~ctx ctx.local e with | Address a -> a | Bot -> Queries.Result.bot q (* TODO: remove *) | Int i -> AD.of_int i | _ -> Queries.Result.top q end | Q.EvalThread e -> begin - let v = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in + let v = eval_rv ~ctx ctx.local e in (* ignore (Pretty.eprintf "evalthread %a (%a): %a" d_exp e d_plainexp e VD.pretty v); *) match v with | Thread a -> a @@ -1316,12 +1330,12 @@ struct | _ -> Queries.Result.top q end | Q.ReachableFrom e -> begin - match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with + match eval_rv_address ~ctx ctx.local e with | Top -> Queries.Result.top q | Bot -> Queries.Result.bot q (* TODO: remove *) | Address a -> let a' = AD.remove Addr.UnknownPtr a in (* run reachable_vars without unknown just to be safe: TODO why? *) - let addrs = reachable_vars (Analyses.ask_of_ctx ctx) [a'] ctx.global ctx.local in + let addrs = reachable_vars ~ctx ctx.local [a'] in let addrs' = List.fold_left (AD.join) (AD.empty ()) addrs in if AD.may_be_unknown a then AD.add UnknownPtr addrs' (* add unknown back *) @@ -1336,7 +1350,7 @@ struct | _ -> AD.empty () end | Q.ReachableUkTypes e -> begin - match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with + match eval_rv_address ~ctx ctx.local e with | Top -> Queries.Result.top q | Bot -> Queries.Result.bot q (* TODO: remove *) | Address a when AD.is_top a || AD.mem Addr.UnknownPtr a -> @@ -1346,7 +1360,7 @@ struct | _ -> Q.TS.empty () end | Q.EvalStr e -> begin - match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with + match eval_rv_address ~ctx ctx.local e with (* exactly one string in the set (works for assignments of string constants) *) | Address a when List.compare_length_with (AD.to_string a) 1 = 0 -> (* exactly one string *) `Lifted (List.hd (AD.to_string a)) @@ -1411,7 +1425,7 @@ struct (** [set st addr val] returns a state where [addr] is set to [val] * it is always ok to put None for lval_raw and rval_raw, this amounts to not using/maintaining * precise information about arrays. *) - let set (a: Q.ask) ~(ctx: _ ctx) ?(invariant=false) ?(blob_destructive=false) ?lval_raw ?rval_raw ?t_override (gs:glob_fun) (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store = + let set ~(ctx: _ ctx) ?(invariant=false) ?(blob_destructive=false) ?lval_raw ?rval_raw ?t_override (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store = let update_variable x t y z = if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a\n\n" x.vname VD.pretty y CPA.pretty z; let r = update_variable x t y z in (* refers to defintion that is outside of set *) @@ -1424,11 +1438,12 @@ struct (* Updating a single varinfo*offset pair. NB! This function's type does * not include the flag. *) let update_one_addr (x, offs) (st: store): store = + let ask = Analyses.ask_of_ctx ctx in let cil_offset = Offs.to_cil_offset offs in let t = match t_override with | Some t -> t | None -> - if a.f (Q.IsAllocVar x) then + if ctx.ask (Q.IsAllocVar x) then (* the vtype of heap vars will be TVoid, so we need to trust the pointer we got to this to be of the right type *) (* i.e. use the static type of the pointer here *) lval_type @@ -1443,8 +1458,8 @@ struct in let update_offset old_value = (* Projection globals to highest Precision *) - let projected_value = project_val (Queries.to_value_domain_ask a) None None value (is_global a x) in - let new_value = VD.update_offset ~blob_destructive (Queries.to_value_domain_ask a) old_value offs projected_value lval_raw ((Var x), cil_offset) t in + let projected_value = project_val (Queries.to_value_domain_ask ask) None None value (is_global ask x) in + let new_value = VD.update_offset ~blob_destructive (Queries.to_value_domain_ask ask) old_value offs projected_value lval_raw ((Var x), cil_offset) t in if WeakUpdates.mem x st.weak then VD.join old_value new_value else if invariant then ( @@ -1468,20 +1483,20 @@ struct end else (* Check if we need to side-effect this one. We no longer generate * side-effects here, but the code still distinguishes these cases. *) - if (!earlyglobs || ThreadFlag.has_ever_been_multi a) && is_global a x then begin + if (!earlyglobs || ThreadFlag.has_ever_been_multi ask) && is_global ask x then begin if M.tracing then M.tracel "set" ~var:x.vname "update_one_addr: update a global var '%s' ...\n" x.vname; - let priv_getg = priv_getg gs in + let priv_getg = priv_getg ctx.global in (* Optimization to avoid evaluating integer values when setting them. The case when invariant = true requires the old_value to be sound for the meet. Allocated blocks are representend by Blobs with additional information, so they need to be looked-up. *) - let old_value = if not invariant && Cil.isIntegralType x.vtype && not (a.f (IsAllocVar x)) && offs = `NoOffset then begin + let old_value = if not invariant && Cil.isIntegralType x.vtype && not (ctx.ask (IsAllocVar x)) && offs = `NoOffset then begin VD.bot_value ~varAttr:x.vattr lval_type end else - Priv.read_global a priv_getg st x + Priv.read_global ask priv_getg st x in let new_value = update_offset old_value in if M.tracing then M.tracel "set" "update_offset %a -> %a\n" VD.pretty old_value VD.pretty new_value; - let r = Priv.write_global ~invariant a priv_getg (priv_sideg ctx.sideg) st x new_value in + let r = Priv.write_global ~invariant ask priv_getg (priv_sideg ctx.sideg) st x new_value in if M.tracing then M.tracel "set" ~var:x.vname "update_one_addr: updated a global var '%s' \nstate:%a\n\n" x.vname D.pretty r; r end else begin @@ -1558,7 +1573,7 @@ struct else let x_updated = update_variable x t new_value st.cpa in let with_dep = add_partitioning_dependencies x new_value {st with cpa = x_updated } in - effect_on_arrays a with_dep + effect_on_arrays ask with_dep end in let update_one x store = @@ -1581,10 +1596,10 @@ struct (* if M.tracing then M.tracel "set" ~var:firstvar "set got an exception '%s'\n" x; *) M.info ~category:Unsound "Assignment to unknown address, assuming no write happened."; st - let set_many ~ctx a (gs:glob_fun) (st: store) lval_value_list: store = + let set_many ~ctx (st: store) lval_value_list: store = (* Maybe this can be done with a simple fold *) let f (acc: store) ((lval:AD.t),(typ:Cil.typ),(value:value)): store = - set ~ctx a gs acc lval typ value + set ~ctx acc lval typ value in (* And fold over the list starting from the store turned wstore: *) List.fold_left f st lval_value_list @@ -1633,12 +1648,12 @@ struct let convert_offset = convert_offset let get_var = get_var - let get a gs st addrs exp = get a gs st addrs exp - let set a ~ctx gs st lval lval_type ?lval_raw value = set a ~ctx ~invariant:true gs st lval lval_type ?lval_raw value + let get ~ctx st addrs exp = get ~ctx st addrs exp + let set ~ctx st lval lval_type ?lval_raw value = set ~ctx ~invariant:true st lval lval_type ?lval_raw value let refine_entire_var = true let map_oldval oldval _ = oldval - let eval_rv_lval_refine a gs st exp lval = eval_rv a gs st (Lval lval) + let eval_rv_lval_refine ~ctx st exp lval = eval_rv ~ctx st (Lval lval) let id_meet_down ~old ~c = ID.meet old c let fd_meet_down ~old ~c = FD.meet old c @@ -1651,11 +1666,11 @@ struct let invariant = Invariant.invariant - let set_savetop ~ctx ?lval_raw ?rval_raw ask (gs:glob_fun) st adr lval_t v : store = + let set_savetop ~ctx ?lval_raw ?rval_raw st adr lval_t v : store = if M.tracing then M.tracel "set" "savetop %a %a %a\n" AD.pretty adr d_type lval_t VD.pretty v; match v with - | Top -> set ~ctx ask gs st adr lval_t (VD.top_value (AD.type_of adr)) ?lval_raw ?rval_raw - | v -> set ~ctx ask gs st adr lval_t v ?lval_raw ?rval_raw + | Top -> set ~ctx st adr lval_t (VD.top_value (AD.type_of adr)) ?lval_raw ?rval_raw + | v -> set ~ctx st adr lval_t v ?lval_raw ?rval_raw (************************************************************************** @@ -1698,9 +1713,9 @@ struct | _ -> () in char_array_hack (); - let rval_val = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local rval in + let rval_val = eval_rv ~ctx ctx.local rval in let rval_val = VD.mark_jmpbufs_as_copied rval_val in - let lval_val = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval in + let lval_val = eval_lv ~ctx ctx.local lval in (* let sofa = AD.short 80 lval_val^" = "^VD.short 80 rval_val in *) (* M.debug ~category:Analyzer @@ sprint ~width:max_int @@ dprintf "%a = %a\n%s" d_plainlval lval d_plainexp rval sofa; *) let not_local xs = @@ -1732,7 +1747,7 @@ struct assert (offs = NoOffset); VD.Bot end else - eval_rv_keep_bot (Analyses.ask_of_ctx ctx) ctx.global ctx.local (Lval (Var v, NoOffset)) + eval_rv_keep_bot ~ctx ctx.local (Lval (Var v, NoOffset)) in begin match current_val with | Bot -> (* current value is VD Bot *) @@ -1742,28 +1757,28 @@ struct let iv = VD.bot_value ~varAttr:v.vattr t in (* correct bottom value for top level variable *) if M.tracing then M.tracel "set" "init bot value: %a\n" VD.pretty iv; let nv = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) iv offs rval_val (Some (Lval lval)) lval t in (* do desired update to value *) - set_savetop ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local (AD.of_var v) lval_t nv ~lval_raw:lval ~rval_raw:rval (* set top-level variable to updated value *) + set_savetop ~ctx ctx.local (AD.of_var v) lval_t nv ~lval_raw:lval ~rval_raw:rval (* set top-level variable to updated value *) | None -> - set_savetop ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval_val lval_t rval_val ~lval_raw:lval ~rval_raw:rval + set_savetop ~ctx ctx.local lval_val lval_t rval_val ~lval_raw:lval ~rval_raw:rval end | _ -> - set_savetop ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval_val lval_t rval_val ~lval_raw:lval ~rval_raw:rval + set_savetop ~ctx ctx.local lval_val lval_t rval_val ~lval_raw:lval ~rval_raw:rval end | _ -> - set_savetop ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval_val lval_t rval_val ~lval_raw:lval ~rval_raw:rval + set_savetop ~ctx ctx.local lval_val lval_t rval_val ~lval_raw:lval ~rval_raw:rval let branch ctx (exp:exp) (tv:bool) : store = - let valu = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp in + let valu = eval_rv ~ctx ctx.local exp in let refine () = - let res = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp tv in + let res = invariant ctx ctx.local exp tv in if M.tracing then M.tracec "branch" "EqualSet result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.EqualSet exp)); if M.tracing then M.tracec "branch" "CondVars result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.CondVars exp)); if M.tracing then M.traceu "branch" "Invariant enforced!\n"; match ctx.ask (Queries.CondVars exp) with | s when Queries.ES.cardinal s = 1 -> let e = Queries.ES.choose s in - invariant ctx (Analyses.ask_of_ctx ctx) ctx.global res e tv + invariant ctx res e tv | _ -> res in if M.tracing then M.traceli "branch" ~subsys:["invariant"] "Evaluating branch for expression %a with value %a\n" d_exp exp VD.pretty valu; @@ -1803,11 +1818,12 @@ struct let init_var v = (AD.of_var v, v.vtype, VD.init_value ~varAttr:v.vattr v.vtype) in (* Apply it to all the locals and then assign them all *) let inits = List.map init_var f.slocals in - set_many ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local inits + set_many ~ctx ctx.local inits let return ctx exp fundec: store = if Cil.hasAttribute "noreturn" fundec.svar.vattr then M.warn ~category:(Behavior (Undefined Other)) "Function declared 'noreturn' could return"; + let ask = Analyses.ask_of_ctx ctx in let st: store = ctx.local in match fundec.svar.vname with | "__goblint_dummy_init" -> @@ -1815,11 +1831,11 @@ struct publish_all ctx `Init; (* otherfun uses __goblint_dummy_init, where we can properly side effect global initialization *) (* TODO: move into sync `Init *) - Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st + Priv.enter_multithreaded ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st | _ -> let locals = List.filter (fun v -> not (WeakUpdates.mem v st.weak)) (fundec.sformals @ fundec.slocals) in - let nst_part = rem_many_partitioning (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) ctx.local locals in - let nst: store = rem_many (Analyses.ask_of_ctx ctx) nst_part locals in + let nst_part = rem_many_partitioning (Queries.to_value_domain_ask ask) ctx.local locals in + let nst: store = rem_many ask nst_part locals in match exp with | None -> nst | Some exp -> @@ -1827,64 +1843,65 @@ struct | TVoid _ -> M.warn ~category:M.Category.Program "Returning a value from a void function"; assert false | ret -> ret in - let rv = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp in - let st' = set ~ctx ~t_override (Analyses.ask_of_ctx ctx) ctx.global nst (return_var ()) t_override rv in - match ThreadId.get_current (Analyses.ask_of_ctx ctx) with - | `Lifted tid when ThreadReturn.is_current (Analyses.ask_of_ctx ctx) -> + let rv = eval_rv ~ctx ctx.local exp in + let st' = set ~ctx ~t_override nst (return_var ()) t_override rv in + match ThreadId.get_current ask with + | `Lifted tid when ThreadReturn.is_current ask -> (* Evaluate exp and cast the resulting value to the void-pointer-type. Casting to the right type here avoids precision loss on joins. *) let rv = VD.cast ~torg:(Cilfacade.typeOf exp) Cil.voidPtrType rv in ctx.sideg (V.thread tid) (G.create_thread rv); - Priv.thread_return (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) tid st' + Priv.thread_return ask (priv_getg ctx.global) (priv_sideg ctx.sideg) tid st' | _ -> st' let vdecl ctx (v:varinfo) = if not (Cil.isArrayType v.vtype) then ctx.local else - let lval = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local (Var v, NoOffset) in - let current_value = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local (Lval (Var v, NoOffset)) in - let new_value = VD.update_array_lengths (eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local) current_value v.vtype in - set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval v.vtype new_value + let lval = eval_lv ~ctx ctx.local (Var v, NoOffset) in + let current_value = eval_rv ~ctx ctx.local (Lval (Var v, NoOffset)) in + let new_value = VD.update_array_lengths (eval_rv ~ctx ctx.local) current_value v.vtype in + set ~ctx ctx.local lval v.vtype new_value (************************************************************************** * Function calls **************************************************************************) (** From a list of expressions, collect a list of addresses that they might point to, or contain pointers to. *) - let collect_funargs ask ?(warn=false) (gs:glob_fun) (st:store) (exps: exp list) = + let collect_funargs ~ctx ?(warn=false) (st:store) (exps: exp list) = + let ask = Analyses.ask_of_ctx ctx in let do_exp e = - let immediately_reachable = reachable_from_value ask gs st (eval_rv ask gs st e) (Cilfacade.typeOf e) (CilType.Exp.show e) in - reachable_vars ask [immediately_reachable] gs st + let immediately_reachable = reachable_from_value ask (eval_rv ~ctx st e) (Cilfacade.typeOf e) (CilType.Exp.show e) in + reachable_vars ~ctx st [immediately_reachable] in List.concat_map do_exp exps - let collect_invalidate ~deep ask ?(warn=false) (gs:glob_fun) (st:store) (exps: exp list) = + let collect_invalidate ~deep ~ctx ?(warn=false) (st:store) (exps: exp list) = if deep then - collect_funargs ask ~warn gs st exps + collect_funargs ~ctx ~warn st exps else ( - let mpt e = match eval_rv_address ask gs st e with + let mpt e = match eval_rv_address ~ctx st e with | Address a -> AD.remove NullPtr a | _ -> AD.empty () in List.map mpt exps ) - let invalidate ?(deep=true) ~ctx ask (gs:glob_fun) (st:store) (exps: exp list): store = + let invalidate ?(deep=true) ~ctx (st:store) (exps: exp list): store = if M.tracing && exps <> [] then M.tracel "invalidate" "Will invalidate expressions [%a]\n" (d_list ", " d_plainexp) exps; if exps <> [] then M.info ~category:Imprecise "Invalidating expressions: %a" (d_list ", " d_exp) exps; (* To invalidate a single address, we create a pair with its corresponding * top value. *) let invalidate_address st a = let t = AD.type_of a in - let v = get ask gs st a None in (* None here is ok, just causes us to be a bit less precise *) - let nv = VD.invalidate_value (Queries.to_value_domain_ask ask) t v in + let v = get ~ctx st a None in (* None here is ok, just causes us to be a bit less precise *) + let nv = VD.invalidate_value (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) t v in (a, t, nv) in (* We define the function that invalidates all the values that an address * expression e may point to *) let invalidate_exp exps = - let args = collect_invalidate ~deep ~warn:true ask gs st exps in + let args = collect_invalidate ~deep ~ctx ~warn:true st exps in List.map (invalidate_address st) args in let invalids = invalidate_exp exps in @@ -1897,13 +1914,14 @@ struct let vs = List.map (Tuple3.third) invalids' in M.tracel "invalidate" "Setting addresses [%a] to values [%a]\n" (d_list ", " AD.pretty) addrs (d_list ", " VD.pretty) vs ); - set_many ~ctx ask gs st invalids' + set_many ~ctx st invalids' let make_entry ?(thread=false) (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) fundec args: D.t = + let ask = Analyses.ask_of_ctx ctx in let st: store = ctx.local in (* Evaluate the arguments. *) - let vals = List.map (eval_rv (Analyses.ask_of_ctx ctx) ctx.global st) args in + let vals = List.map (eval_rv ~ctx st) args in (* generate the entry states *) (* If we need the globals, add them *) (* TODO: make this is_private PrivParam dependent? PerMutexOplusPriv should keep *) @@ -1913,12 +1931,12 @@ struct Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published... sync `Thread doesn't help us here, it's not specific to entering multithreaded mode. EnterMultithreaded events only execute after threadenter and threadspawn. *) - if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then - ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st); - Priv.threadenter (Analyses.ask_of_ctx ctx) st + if not (ThreadFlag.has_ever_been_multi ask) then + ignore (Priv.enter_multithreaded ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st); + Priv.threadenter ask st ) else (* use is_global to account for values that became globals because they were saved into global variables *) - let globals = CPA.filter (fun k v -> is_global (Analyses.ask_of_ctx ctx) k) st.cpa in + let globals = CPA.filter (fun k v -> is_global ask k) st.cpa in (* let new_cpa = if !earlyglobs || ThreadFlag.is_multi ctx.ask then CPA.filter (fun k v -> is_private ctx.ask ctx.local k) globals else globals in *) let new_cpa = globals in {st with cpa = new_cpa} @@ -1928,13 +1946,13 @@ struct add_to_array_map fundec pa; let new_cpa = CPA.add_list pa st'.cpa in (* List of reachable variables *) - let reachable = List.concat_map AD.to_var_may (reachable_vars (Analyses.ask_of_ctx ctx) (get_ptrs vals) ctx.global st) in + let reachable = List.concat_map AD.to_var_may (reachable_vars ~ctx st (get_ptrs vals)) in let reachable = List.filter (fun v -> CPA.mem v st.cpa) reachable in let new_cpa = CPA.add_list_fun reachable (fun v -> CPA.find v st.cpa) new_cpa in (* Projection to Precision of the Callee *) let p = PU.int_precision_from_fundec fundec in - let new_cpa = project (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) (Some p) new_cpa fundec in + let new_cpa = project (Queries.to_value_domain_ask ask) (Some p) new_cpa fundec in (* Identify locals of this fundec for which an outer copy (from a call down the callstack) is reachable *) let reachable_other_copies = List.filter (fun v -> match Cilfacade.find_scope_fundec v with Some scope -> CilType.Fundec.equal scope fundec | None -> false) reachable in @@ -1980,7 +1998,7 @@ struct (* extra sync so that we do not analyze new threads with bottom global invariant *) publish_all ctx `Thread; (* Collect the threads. *) - let start_addr = eval_tv (Analyses.ask_of_ctx ctx) ctx.global ctx.local start in + let start_addr = eval_tv ~ctx ctx.local start in let start_funvars = AD.to_var_may start_addr in let start_funvars_with_unknown = if AD.mem Addr.UnknownPtr start_addr then @@ -1997,8 +2015,8 @@ struct Need this to not have memmove spawn in SV-COMP. *) let shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = false } args in let deep_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = true } args in - let shallow_flist = collect_invalidate ~deep:false (Analyses.ask_of_ctx ctx) ctx.global ctx.local shallow_args in - let deep_flist = collect_invalidate ~deep:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local deep_args in + let shallow_flist = collect_invalidate ~deep:false ~ctx ctx.local shallow_args in + let deep_flist = collect_invalidate ~deep:true ~ctx ctx.local deep_args in let flist = shallow_flist @ deep_flist in let addrs = List.concat_map AD.to_var_may flist in if addrs <> [] then M.debug ~category:Analyzer "Spawning non-unique functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs; @@ -2008,13 +2026,13 @@ struct let assert_fn ctx e refine = (* make the state meet the assertion in the rest of the code *) if not refine then ctx.local else begin - let newst = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local e true in + let newst = invariant ctx ctx.local e true in (* if check_assert e newst <> `Lifted true then M.warn ~category:Assert ~msg:("Invariant \"" ^ expr ^ "\" does not stick.") (); *) newst end - let special_unknown_invalidate ctx ask gs st f args = + let special_unknown_invalidate ctx f args = (if CilType.Varinfo.equal f dummyFunDec.svar then M.warn ~category:Imprecise ~tags:[Category Call] "Unknown function ptr called"); let desc = LF.find f in let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in @@ -2035,8 +2053,8 @@ struct in (* TODO: what about escaped local variables? *) (* invalidate arguments and non-static globals for unknown functions *) - let st' = invalidate ~deep:false ~ctx (Analyses.ask_of_ctx ctx) gs st shallow_addrs in - invalidate ~deep:true ~ctx (Analyses.ask_of_ctx ctx) gs st' deep_addrs + let st' = invalidate ~deep:false ~ctx ctx.local shallow_addrs in + invalidate ~deep:true ~ctx st' deep_addrs let check_invalid_mem_dealloc ctx special_fn ptr = let has_non_heap_var = AD.exists (function @@ -2047,7 +2065,7 @@ struct | Addr (_,o) -> Offs.cmp_zero_offset o <> `MustZero | _ -> false) in - match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local ptr with + match eval_rv_address ~ctx ctx.local ptr with | Address a -> if AD.is_top a then ( AnalysisStateUtil.set_mem_safety_flag InvalidFree; @@ -2126,19 +2144,18 @@ struct let invalidate_ret_lv st = match lv with | Some lv -> if M.tracing then M.tracel "invalidate" "Invalidating lhs %a for function call %s\n" d_plainlval lv f.vname; - invalidate ~deep:false ~ctx (Analyses.ask_of_ctx ctx) ctx.global st [Cil.mkAddrOrStartOf lv] + invalidate ~deep:false ~ctx st [Cil.mkAddrOrStartOf lv] | None -> st in let addr_type_of_exp exp = let lval = mkMem ~addr:(Cil.stripCasts exp) ~off:NoOffset in - let addr = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval in + let addr = eval_lv ~ctx ctx.local lval in (addr, AD.type_of addr) in let forks = forkfun ctx lv f args in if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," CilType.Varinfo.pretty) (List.map BatTuple.Tuple4.second forks); List.iter (fun (lval, f, args, multiple) -> ctx.spawn ~multiple lval f args) forks; let st: store = ctx.local in - let gs = ctx.global in let desc = LF.find f in let memory_copying dst src n = let dest_size = get_size_of_ptr_target ctx dst in @@ -2158,21 +2175,21 @@ struct in let dest_a, dest_typ = addr_type_of_exp dst in let src_lval = mkMem ~addr:(Cil.stripCasts src) ~off:NoOffset in - let src_typ = eval_lv (Analyses.ask_of_ctx ctx) gs st src_lval + let src_typ = eval_lv ~ctx ctx.local src_lval |> AD.type_of in (* when src and destination type coincide, take value from the source, otherwise use top *) let value = if (typeSig dest_typ = typeSig src_typ) && dest_size_equal_n then let src_cast_lval = mkMem ~addr:(Cilfacade.mkCast ~e:src ~newt:(TPtr (dest_typ, []))) ~off:NoOffset in - eval_rv (Analyses.ask_of_ctx ctx) gs st (Lval src_cast_lval) + eval_rv ~ctx st (Lval src_cast_lval) else VD.top_value (unrollType dest_typ) in - set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value in + set ~ctx st dest_a dest_typ value in (* for string functions *) let eval_n = function (* if only n characters of a given string are needed, evaluate expression n to an integer option *) | Some n -> - begin match eval_rv (Analyses.ask_of_ctx ctx) gs st n with + begin match eval_rv ~ctx st n with | Int i -> begin match ID.to_int i with | Some x -> Some (Z.to_int x) @@ -2198,10 +2215,10 @@ struct | _ -> raise (Failure "String function: not an address") in let string_manipulation s1 s2 lv all op_addr op_array = - let s1_v = eval_rv (Analyses.ask_of_ctx ctx) gs st s1 in + let s1_v = eval_rv ~ctx st s1 in let s1_a = address_from_value s1_v in let s1_typ = AD.type_of s1_a in - let s2_v = eval_rv (Analyses.ask_of_ctx ctx) gs st s2 in + let s2_v = eval_rv ~ctx st s2 in let s2_a = address_from_value s2_v in let s2_typ = AD.type_of s2_a in (* compute value in string literals domain if s1 and s2 are both string literals *) @@ -2210,30 +2227,30 @@ struct begin match lv, op_addr with | Some lv_val, Some f -> (* when whished types coincide, compute result of operation op_addr, otherwise use top *) - let lv_a = eval_lv (Analyses.ask_of_ctx ctx) gs st lv_val in + let lv_a = eval_lv ~ctx st lv_val in let lv_typ = Cilfacade.typeOfLval lv_val in if all && typeSig s1_typ = typeSig s2_typ && typeSig s2_typ = typeSig lv_typ then (* all types need to coincide *) - set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (f s1_a s2_a) + set ~ctx st lv_a lv_typ (f s1_a s2_a) else if not all && typeSig s1_typ = typeSig s2_typ then (* only the types of s1 and s2 need to coincide *) - set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (f s1_a s2_a) + set ~ctx st lv_a lv_typ (f s1_a s2_a) else - set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (VD.top_value (unrollType lv_typ)) + set ~ctx st lv_a lv_typ (VD.top_value (unrollType lv_typ)) | _ -> (* check if s1 is potentially a string literal as writing to it would be undefined behavior; then return top *) let _ = AD.string_writing_defined s1_a in - set ~ctx (Analyses.ask_of_ctx ctx) gs st s1_a s1_typ (VD.top_value (unrollType s1_typ)) + set ~ctx st s1_a s1_typ (VD.top_value (unrollType s1_typ)) end (* else compute value in array domain *) else let lv_a, lv_typ = match lv with - | Some lv_val -> eval_lv (Analyses.ask_of_ctx ctx) gs st lv_val, Cilfacade.typeOfLval lv_val + | Some lv_val -> eval_lv ~ctx st lv_val, Cilfacade.typeOfLval lv_val | None -> s1_a, s1_typ in - begin match (get (Analyses.ask_of_ctx ctx) gs st s1_a None), get (Analyses.ask_of_ctx ctx) gs st s2_a None with - | Array array_s1, Array array_s2 -> set ~ctx ~blob_destructive:true (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array array_s1 array_s2) + begin match (get ~ctx st s1_a None), get ~ctx st s2_a None with + | Array array_s1, Array array_s2 -> set ~ctx ~blob_destructive:true st lv_a lv_typ (op_array array_s1 array_s2) | Array array_s1, _ when CilType.Typ.equal s2_typ charPtrType -> let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in let array_s2 = List.fold_left CArrays.join (CArrays.bot ()) s2_null_bytes in - set ~ctx ~blob_destructive:true (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array array_s1 array_s2) + set ~ctx ~blob_destructive:true st lv_a lv_typ (op_array array_s1 array_s2) | Bot, Array array_s2 -> (* If we have bot inside here, we assume the blob is used as a char array and create one inside *) let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in @@ -2242,7 +2259,7 @@ struct try ValueDomainQueries.ID.unlift (ID.cast_to ptrdiff_ik) size with Failure _ -> ID.top_of ptrdiff_ik in let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in - set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array empty_array array_s2) + set ~ctx st lv_a lv_typ (op_array empty_array array_s2) | Bot , _ when CilType.Typ.equal s2_typ charPtrType -> (* If we have bot inside here, we assume the blob is used as a char array and create one inside *) let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in @@ -2253,25 +2270,25 @@ struct let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in let array_s2 = List.fold_left CArrays.join (CArrays.bot ()) s2_null_bytes in - set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array empty_array array_s2) + set ~ctx st lv_a lv_typ (op_array empty_array array_s2) | _, Array array_s2 when CilType.Typ.equal s1_typ charPtrType -> (* if s1 is string literal, str(n)cpy and str(n)cat are undefined *) if op_addr = None then (* triggers warning, function only evaluated for side-effects *) let _ = AD.string_writing_defined s1_a in - set ~ctx (Analyses.ask_of_ctx ctx) gs st s1_a s1_typ (VD.top_value (unrollType s1_typ)) + set ~ctx st s1_a s1_typ (VD.top_value (unrollType s1_typ)) else let s1_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s1_a) in let array_s1 = List.fold_left CArrays.join (CArrays.bot ()) s1_null_bytes in - set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array array_s1 array_s2) + set ~ctx st lv_a lv_typ (op_array array_s1 array_s2) | _ -> - set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (VD.top_value (unrollType lv_typ)) + set ~ctx st lv_a lv_typ (VD.top_value (unrollType lv_typ)) end in let st = match desc.special args, f.vname with | Memset { dest; ch; count; }, _ -> (* TODO: check count *) - let eval_ch = eval_rv (Analyses.ask_of_ctx ctx) gs st ch in + let eval_ch = eval_rv ~ctx st ch in let dest_a, dest_typ = addr_type_of_exp dest in let value = match eval_ch with @@ -2280,13 +2297,13 @@ struct | _ -> VD.top_value dest_typ in - set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value + set ~ctx st dest_a dest_typ value | Bzero { dest; count; }, _ -> (* TODO: share something with memset special case? *) (* TODO: check count *) let dest_a, dest_typ = addr_type_of_exp dest in let value = VD.zero_init_value dest_typ in - set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value + set ~ctx st dest_a dest_typ value | Memcpy { dest = dst; src; n; }, _ -> (* TODO: use n *) memory_copying dst src (Some n) | Strcpy { dest = dst; src; n }, _ -> string_manipulation dst src None false None (fun ar1 ar2 -> Array (CArrays.string_copy ar1 ar2 (eval_n n))) @@ -2294,9 +2311,9 @@ struct | Strlen s, _ -> begin match lv with | Some lv_val -> - let dest_a = eval_lv (Analyses.ask_of_ctx ctx) gs st lv_val in + let dest_a = eval_lv ~ctx st lv_val in let dest_typ = Cilfacade.typeOfLval lv_val in - let v = eval_rv (Analyses.ask_of_ctx ctx) gs st s in + let v = eval_rv ~ctx st s in let a = address_from_value v in let value:value = (* if s string literal, compute strlen in string literals domain *) @@ -2305,11 +2322,11 @@ struct Int (AD.to_string_length a) (* else compute strlen in array domain *) else - begin match get (Analyses.ask_of_ctx ctx) gs st a None with + begin match get ~ctx st a None with | Array array_s -> Int (CArrays.to_string_length array_s) | _ -> VD.top_value (unrollType dest_typ) end in - set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value + set ~ctx st dest_a dest_typ value | None -> st end | Strstr { haystack; needle }, _ -> @@ -2322,8 +2339,8 @@ struct string_manipulation haystack needle lv true (Some (fun h_a n_a -> Address (AD.substring_extraction h_a n_a))) (fun h_ar n_ar -> match CArrays.substring_extraction h_ar n_ar with | CArrays.IsNotSubstr -> Address (AD.null_ptr) - | CArrays.IsSubstrAtIndex0 -> Address (eval_lv (Analyses.ask_of_ctx ctx) gs st (mkMem ~addr:(Cil.stripCasts haystack) ~off:NoOffset)) - | CArrays.IsMaybeSubstr -> Address (AD.join (eval_lv (Analyses.ask_of_ctx ctx) gs st + | CArrays.IsSubstrAtIndex0 -> Address (eval_lv ~ctx st (mkMem ~addr:(Cil.stripCasts haystack) ~off:NoOffset)) + | CArrays.IsMaybeSubstr -> Address (AD.join (eval_lv ~ctx st (mkMem ~addr:(Cil.stripCasts haystack) ~off:(Index (Offset.Index.Exp.any, NoOffset)))) (AD.null_ptr))) | None -> st end @@ -2341,14 +2358,15 @@ struct begin match ThreadId.get_current (Analyses.ask_of_ctx ctx) with | `Lifted tid -> ( - let rv = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp in + let rv = eval_rv ~ctx ctx.local exp in ctx.sideg (V.thread tid) (G.create_thread rv); (* TODO: emit thread return event so other analyses are aware? *) (* TODO: publish still needed? *) publish_all ctx `Return; (* like normal return *) - match ThreadId.get_current (Analyses.ask_of_ctx ctx) with - | `Lifted tid when ThreadReturn.is_current (Analyses.ask_of_ctx ctx) -> - ignore @@ Priv.thread_return (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) tid st + let ask = Analyses.ask_of_ctx ctx in + match ThreadId.get_current ask with + | `Lifted tid when ThreadReturn.is_current ask -> + ignore @@ Priv.thread_return ask (priv_getg ctx.global) (priv_sideg ctx.sideg) tid st | _ -> ()) | _ -> () end; @@ -2356,22 +2374,22 @@ struct | MutexAttrSetType {attr = attr; typ = mtyp}, _ -> begin let get_type lval = - let address = eval_lv (Analyses.ask_of_ctx ctx) gs st lval in + let address = eval_lv ~ctx st lval in AD.type_of address in let dst_lval = mkMem ~addr:(Cil.stripCasts attr) ~off:NoOffset in let dest_typ = get_type dst_lval in - let dest_a = eval_lv (Analyses.ask_of_ctx ctx) gs st dst_lval in - match eval_rv (Analyses.ask_of_ctx ctx) gs st mtyp with + let dest_a = eval_lv ~ctx st dst_lval in + match eval_rv ~ctx st mtyp with | Int x -> begin match ID.to_int x with | Some z -> if M.tracing then M.tracel "attr" "setting\n"; - set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.of_int z)) - | None -> set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.top ())) + set ~ctx st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.of_int z)) + | None -> set ~ctx st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.top ())) end - | _ -> set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.top ())) + | _ -> set ~ctx st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.top ())) end | Identity e, _ -> begin match lv with @@ -2381,22 +2399,22 @@ struct (**Floating point classification and trigonometric functions defined in c99*) | Math { fun_args; }, _ -> let apply_unary fk float_fun x = - let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in + let eval_x = eval_rv ~ctx st x in begin match eval_x with | Float float_x -> float_fun (FD.cast_to fk float_x) | _ -> failwith ("non-floating-point argument in call to function "^f.vname) end in let apply_binary fk float_fun x y = - let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in - let eval_y = eval_rv (Analyses.ask_of_ctx ctx) gs st y in + let eval_x = eval_rv ~ctx st x in + let eval_y = eval_rv ~ctx st y in begin match eval_x, eval_y with | Float float_x, Float float_y -> float_fun (FD.cast_to fk float_x) (FD.cast_to fk float_y) | _ -> failwith ("non-floating-point argument in call to function "^f.vname) end in let apply_abs ik x = - let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in + let eval_x = eval_rv ~ctx st x in begin match eval_x with | Int int_x -> let xcast = ID.cast_to ik int_x in @@ -2446,7 +2464,7 @@ struct end in begin match lv with - | Some lv_val -> set ~ctx (Analyses.ask_of_ctx ctx) gs st (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st lv_val) (Cilfacade.typeOfLval lv_val) result + | Some lv_val -> set ~ctx st (eval_lv ~ctx st lv_val) (Cilfacade.typeOfLval lv_val) result | None -> st end (* handling thread creations *) @@ -2456,18 +2474,18 @@ struct | ThreadJoin { thread = id; ret_var }, _ -> let st' = (* TODO: should invalidate shallowly? https://github.com/goblint/analyzer/pull/1224#discussion_r1405826773 *) - match (eval_rv (Analyses.ask_of_ctx ctx) gs st ret_var) with + match eval_rv ~ctx st ret_var with | Int n when GobOption.exists (BI.equal BI.zero) (ID.to_int n) -> st | Address ret_a -> - begin match eval_rv (Analyses.ask_of_ctx ctx) gs st id with - | Thread a when ValueDomain.Threads.is_top a -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var] + begin match eval_rv ~ctx st id with + | Thread a when ValueDomain.Threads.is_top a -> invalidate ~ctx st [ret_var] | Thread a -> let v = List.fold VD.join (VD.bot ()) (List.map (fun x -> G.thread (ctx.global (V.thread x))) (ValueDomain.Threads.elements a)) in (* TODO: is this type right? *) - set ~ctx (Analyses.ask_of_ctx ctx) gs st ret_a (Cilfacade.typeOf ret_var) v - | _ -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var] + set ~ctx st ret_a (Cilfacade.typeOf ret_var) v + | _ -> invalidate ~ctx st [ret_var] end - | _ -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var] + | _ -> invalidate ~ctx st [ret_var] in let st' = invalidate_ret_lv st' in Priv.thread_join (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) id st' @@ -2478,9 +2496,9 @@ struct match lv with | Some lv -> let heap_var = AD.of_var (heap_var true ctx) in - (* ignore @@ printf "alloca will allocate %a bytes\n" ID.pretty (eval_int ctx.ask gs st size); *) - set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(heap_var, TVoid [], Blob (VD.bot (), eval_int (Analyses.ask_of_ctx ctx) gs st size, true)); - (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address heap_var)] + (* ignore @@ printf "alloca will allocate %a bytes\n" ID.pretty (eval_int ~ctx size); *) + set_many ~ctx st [(heap_var, TVoid [], Blob (VD.bot (), eval_int ~ctx st size, true)); + (eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address heap_var)] | _ -> st end | Malloc size, _ -> begin @@ -2491,9 +2509,9 @@ struct then AD.join (AD.of_var (heap_var false ctx)) AD.null_ptr else AD.of_var (heap_var false ctx) in - (* ignore @@ printf "malloc will allocate %a bytes\n" ID.pretty (eval_int ctx.ask gs st size); *) - set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(heap_var, TVoid [], Blob (VD.bot (), eval_int (Analyses.ask_of_ctx ctx) gs st size, true)); - (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address heap_var)] + (* ignore @@ printf "malloc will allocate %a bytes\n" ID.pretty (eval_int ~ctx size); *) + set_many ~ctx st [(heap_var, TVoid [], Blob (VD.bot (), eval_int ~ctx st size, true)); + (eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address heap_var)] | _ -> st end | Calloc { count = n; size }, _ -> @@ -2505,20 +2523,20 @@ struct then AD.join addr AD.null_ptr (* calloc can fail and return NULL *) else addr in let ik = Cilfacade.ptrdiff_ikind () in - let sizeval = eval_int (Analyses.ask_of_ctx ctx) gs st size in - let countval = eval_int (Analyses.ask_of_ctx ctx) gs st n in + let sizeval = eval_int ~ctx st size in + let countval = eval_int ~ctx st n in if ID.to_int countval = Some Z.one then ( - set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [ + set_many ~ctx st [ (add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false)); - (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var))) + (eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var))) ] ) else ( let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *) - set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [ + set_many ~ctx st [ (add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (Blob (VD.bot (), blobsize, false)))); - (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset))))) + (eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset))))) ] ) | _ -> st @@ -2528,8 +2546,7 @@ struct check_invalid_mem_dealloc ctx f p; begin match lv with | Some lv -> - let ask = Analyses.ask_of_ctx ctx in - let p_rv = eval_rv ask gs st p in + let p_rv = eval_rv ~ctx st p in let p_addr = match p_rv with | Address a -> a @@ -2539,8 +2556,8 @@ struct | _ -> AD.top_ptr (* TODO: why does this ever happen? *) in let p_addr' = AD.remove NullPtr p_addr in (* realloc with NULL is same as malloc, remove to avoid unknown value from NullPtr access *) - let p_addr_get = get ask gs st p_addr' None in (* implicitly includes join of malloc value (VD.bot) *) - let size_int = eval_int ask gs st size in + let p_addr_get = get ~ctx st p_addr' None in (* implicitly includes join of malloc value (VD.bot) *) + let size_int = eval_int ~ctx st size in let heap_val:value = Blob (p_addr_get, size_int, true) in (* copy old contents with new size *) let heap_addr = AD.of_var (heap_var false ctx) in let heap_addr' = @@ -2549,8 +2566,8 @@ struct else heap_addr in - let lv_addr = eval_lv ask gs st lv in - set_many ~ctx ask gs st [ + let lv_addr = eval_lv ~ctx st lv in + set_many ~ctx st [ (heap_addr, TVoid [], heap_val); (lv_addr, Cilfacade.typeOfLval lv, Address heap_addr'); ] (* TODO: free (i.e. invalidate) old blob if successful? *) @@ -2563,22 +2580,20 @@ struct st | Assert { exp; refine; _ }, _ -> assert_fn ctx exp refine | Setjmp { env }, _ -> - let ask = Analyses.ask_of_ctx ctx in - let st' = match eval_rv ask gs st env with + let st' = match eval_rv ~ctx st env with | Address jmp_buf -> let value = VD.JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (ctx.prev_node, ctx.control_context ())), false) in - let r = set ~ctx ask gs st jmp_buf (Cilfacade.typeOf env) value in + let r = set ~ctx st jmp_buf (Cilfacade.typeOf env) value in if M.tracing then M.tracel "setjmp" "setting setjmp %a on %a -> %a\n" d_exp env D.pretty st D.pretty r; r | _ -> failwith "problem?!" in begin match lv with | Some lv -> - set ~ctx ask gs st' (eval_lv ask ctx.global st lv) (Cilfacade.typeOfLval lv) (Int (ID.of_int IInt BI.zero)) + set ~ctx st' (eval_lv ~ctx st lv) (Cilfacade.typeOfLval lv) (Int (ID.of_int IInt BI.zero)) | None -> st' end | Longjmp {env; value}, _ -> - let ask = Analyses.ask_of_ctx ctx in let ensure_not_zero (rv:value) = match rv with | Int i -> begin match ID.to_bool i with @@ -2595,19 +2610,19 @@ struct M.warn ~category:Program "Arguments to longjmp are strange!"; rv in - let rv = ensure_not_zero @@ eval_rv ask ctx.global ctx.local value in + let rv = ensure_not_zero @@ eval_rv ~ctx ctx.local value in let t = Cilfacade.typeOf value in - set ~ctx ~t_override:t ask ctx.global ctx.local (AD.of_var !longjmp_return) t rv (* Not raising Deadcode here, deadcode is raised at a higher level! *) + set ~ctx ~t_override:t ctx.local (AD.of_var !longjmp_return) t rv (* Not raising Deadcode here, deadcode is raised at a higher level! *) | Rand, _ -> begin match lv with | Some x -> let result:value = (Int (ID.starting IInt Z.zero)) in - set ~ctx (Analyses.ask_of_ctx ctx) gs st (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st x) (Cilfacade.typeOfLval x) result + set ~ctx st (eval_lv ~ctx st x) (Cilfacade.typeOfLval x) result | None -> st end | _, _ -> let st = - special_unknown_invalidate ctx (Analyses.ask_of_ctx ctx) gs st f args + special_unknown_invalidate ctx f args (* * TODO: invalidate vars reachable via args * publish globals @@ -2621,27 +2636,25 @@ struct if get_bool "sem.noreturn.dead_code" && Cil.hasAttribute "noreturn" f.vattr then raise Deadcode else st let combine_st ctx (local_st : store) (fun_st : store) (tainted_lvs : AD.t) : store = - let ask = (Analyses.ask_of_ctx ctx) in - AD.fold (fun addr st -> + AD.fold (fun addr (st: store) -> match addr with - | Addr.Addr (v,o) -> - if CPA.mem v fun_st.cpa then - let lval = Addr.Mval.to_cil (v,o) in - let address = eval_lv ask ctx.global st lval in + | Addr.Addr (v,o) when CPA.mem v fun_st.cpa -> + begin let lval_type = Addr.type_of addr in if M.tracing then M.trace "taintPC" "updating %a; type: %a\n" Addr.Mval.pretty (v,o) d_type lval_type; - match (CPA.find_opt v (fun_st.cpa)), lval_type with - | None, _ -> st + match CPA.find_opt v (fun_st.cpa) with + | None -> st (* partitioned arrays cannot be copied by individual lvalues, so if tainted just copy the whole callee value for the array variable *) - | Some (Array a), _ when (CArrays.domain_of_t a) = PartitionedDomain -> {st with cpa = CPA.add v (Array a) st.cpa} + | Some (Array a) when CArrays.domain_of_t a = PartitionedDomain -> {st with cpa = CPA.add v (Array a) st.cpa} (* "get" returned "unknown" when applied to a void type, so special case void types. This caused problems with some sv-comps (e.g. regtest 64 11) *) - | Some voidVal, TVoid _ -> {st with cpa = CPA.add v voidVal st.cpa} - | _, _ -> begin - let new_val = get ask ctx.global fun_st address None in + | Some voidVal when Addr.type_of addr = voidType -> {st with cpa = CPA.add v voidVal st.cpa} + | _ -> + begin + let address = AD.singleton addr in + let new_val = get ~ctx fun_st address None in if M.tracing then M.trace "taintPC" "update val: %a\n\n" VD.pretty new_val; - let st' = set_savetop ~ctx ask ctx.global st address lval_type new_val in - let partDep = Dep.find_opt v fun_st.deps in - match partDep with + let st' = set_savetop ~ctx st address lval_type new_val in + match Dep.find_opt v fun_st.deps with | None -> st' (* if a var partitions an array, all cpa-info for arrays it may partition are added from callee to caller *) | Some deps -> {st' with cpa = (Dep.VarSet.fold (fun v accCPA -> let val_opt = CPA.find_opt v fun_st.cpa in @@ -2649,7 +2662,7 @@ struct | None -> accCPA | Some new_val -> CPA.add v new_val accCPA ) deps st'.cpa)} end - else st + end | _ -> st ) tainted_lvs local_st @@ -2664,7 +2677,7 @@ struct let add_globals (st: store) (fun_st: store) = (* Remove the return value as this is dealt with separately. *) let cpa_noreturn = CPA.remove (return_varinfo ()) fun_st.cpa in - let ask = (Analyses.ask_of_ctx ctx) in + let ask = Analyses.ask_of_ctx ctx in let tainted = f_ask.f Q.MayBeTainted in if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a\n" f.svar.vname AD.pretty tainted; if M.tracing then M.trace "taintPC" "combine base:\ncaller: %a\ncallee: %a\n" CPA.pretty st.cpa CPA.pretty fun_st.cpa; @@ -2712,7 +2725,7 @@ struct let return_var = return_var () in let return_val = if CPA.mem (return_varinfo ()) fun_st.cpa - then get (Analyses.ask_of_ctx ctx) ctx.global fun_st return_var None + then get ~ctx fun_st return_var None else VD.top () in @@ -2726,7 +2739,7 @@ struct match lval with | None -> st - | Some lval -> set_savetop ~ctx (Analyses.ask_of_ctx ctx) ctx.global st (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st lval) (Cilfacade.typeOfLval lval) return_val + | Some lval -> set_savetop ~ctx st (eval_lv ~ctx st lval) (Cilfacade.typeOfLval lval) return_val in combine_one ctx.local after @@ -2736,8 +2749,7 @@ struct [make_entry ~thread:true ctx fd args] | exception Not_found -> (* Unknown functions *) - let st = ctx.local in - let st = special_unknown_invalidate ctx (Analyses.ask_of_ctx ctx) ctx.global st f args in + let st = special_unknown_invalidate ctx f args in [st] let threadspawn ctx ~multiple (lval: lval option) (f: varinfo) (args: exp list) fctx: D.t = @@ -2825,26 +2837,25 @@ struct module V = V module G = G - let oa = Analyses.ask_of_ctx octx let ost = octx.local (* all evals happen in octx with non-top values *) - let eval_rv a gs st e = eval_rv oa gs ost e - let eval_rv_address a gs st e = eval_rv_address oa gs ost e - let eval_lv a gs st lv = eval_lv oa gs ost lv - let convert_offset a gs st o = convert_offset oa gs ost o + let eval_rv ~ctx st e = eval_rv ~ctx:octx ost e + let eval_rv_address ~ctx st e = eval_rv_address ~ctx:octx ost e + let eval_lv ~ctx st lv = eval_lv ~ctx:octx ost lv + let convert_offset ~ctx st o = convert_offset ~ctx:octx ost o (* all updates happen in ctx with top values *) let get_var = get_var - let get a gs st addrs exp = get a gs st addrs exp - let set a ~ctx gs st lval lval_type ?lval_raw value = set a ~ctx ~invariant:false gs st lval lval_type ?lval_raw value (* TODO: should have invariant false? doesn't work with empty cpa then, because meets *) + let get ~ctx st addrs exp = get ~ctx st addrs exp + let set ~ctx st lval lval_type ?lval_raw value = set ~ctx ~invariant:false st lval lval_type ?lval_raw value (* TODO: should have invariant false? doesn't work with empty cpa then, because meets *) let refine_entire_var = false let map_oldval oldval t_lval = if VD.is_bot oldval then VD.top_value t_lval else oldval - let eval_rv_lval_refine a gs st exp lv = + let eval_rv_lval_refine ~ctx st exp lv = (* new, use different ctx for eval_lv (for Mem): *) - eval_rv_base_lval ~eval_lv a gs st exp lv + eval_rv_base_lval ~eval_lv ~ctx st exp lv (* don't meet with current octx values when propagating inverse operands down *) let id_meet_down ~old ~c = c @@ -2855,7 +2866,7 @@ struct in let module Unassume = BaseInvariant.Make (UnassumeEval) in try - Unassume.invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local e true + Unassume.invariant ctx ctx.local e true with Deadcode -> (* contradiction in unassume *) D.bot () in @@ -2881,31 +2892,32 @@ struct WideningTokens.with_side_tokens (WideningTokens.TS.of_list uuids) (fun () -> CPA.fold (fun x v acc -> let addr: AD.t = AD.of_mval (x, `NoOffset) in - set (Analyses.ask_of_ctx ctx) ~ctx ~invariant:false ctx.global acc addr x.vtype v + set ~ctx ~invariant:false acc addr x.vtype v ) e_d.cpa ctx.local ) in D.join ctx.local e_d' let event ctx e octx = + let ask = Analyses.ask_of_ctx ctx in let st: store = ctx.local in match e with - | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) + | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *) if M.tracing then M.tracel "priv" "LOCK EVENT %a\n" LockDomain.Addr.pretty addr; - Priv.lock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) st addr - | Events.Unlock addr when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) + Priv.lock ask (priv_getg ctx.global) st addr + | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *) if addr = UnknownPtr then M.info ~category:Unsound "Unknown mutex unlocked, base privatization unsound"; (* TODO: something more sound *) WideningTokens.with_local_side_tokens (fun () -> - Priv.unlock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st addr + Priv.unlock ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st addr ) | Events.Escape escaped -> - Priv.escape (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st escaped + Priv.escape ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st escaped | Events.EnterMultiThreaded -> - Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st + Priv.enter_multithreaded ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st | Events.AssignSpawnedThread (lval, tid) -> (* TODO: is this type right? *) - set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval) (Cilfacade.typeOfLval lval) (Thread (ValueDomain.Threads.singleton tid)) + set ~ctx ctx.local (eval_lv ~ctx ctx.local lval) (Cilfacade.typeOfLval lval) (Thread (ValueDomain.Threads.singleton tid)) | Events.Assert exp -> assert_fn ctx exp true | Events.Unassume {exp; uuids} -> diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index f18eeed24f..e66a431ccf 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -15,18 +15,18 @@ sig module V: Analyses.SpecSysVar module G: Lattice.S - val eval_rv: Queries.ask -> (V.t -> G.t) -> D.t -> exp -> VD.t - val eval_rv_address: Queries.ask -> (V.t -> G.t) -> D.t -> exp -> VD.t - val eval_lv: Queries.ask -> (V.t -> G.t) -> D.t -> lval -> AD.t - val convert_offset: Queries.ask -> (V.t -> G.t) -> D.t -> offset -> ID.t Offset.t + val eval_rv: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> exp -> VD.t + val eval_rv_address: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> exp -> VD.t + val eval_lv: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> lval -> AD.t + val convert_offset: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> offset -> ID.t Offset.t - val get_var: Queries.ask -> (V.t -> G.t) -> D.t -> varinfo -> VD.t - val get: Queries.ask -> (V.t -> G.t) -> D.t -> AD.t -> exp option -> VD.t - val set: Queries.ask -> ctx:(D.t, G.t, _, V.t) Analyses.ctx -> (V.t -> G.t) -> D.t -> AD.t -> typ -> ?lval_raw:lval -> VD.t -> D.t + val get_var: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> varinfo -> VD.t + val get: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> AD.t -> exp option -> VD.t + val set: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> AD.t -> typ -> ?lval_raw:lval -> VD.t -> D.t val refine_entire_var: bool val map_oldval: VD.t -> typ -> VD.t - val eval_rv_lval_refine: Queries.ask -> (V.t -> G.t) -> D.t -> exp -> lval -> VD.t + val eval_rv_lval_refine: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> exp -> lval -> VD.t val id_meet_down: old:ID.t -> c:ID.t -> ID.t val fd_meet_down: old:FD.t -> c:FD.t -> FD.t @@ -62,12 +62,12 @@ struct VD.meet old_val new_val with Lattice.Uncomparable -> old_val - let refine_lv_fallback ctx a gs st lval value tv = + let refine_lv_fallback ctx st lval value tv = if M.tracing then M.tracec "invariant" "Restricting %a with %a\n" d_lval lval VD.pretty value; - let addr = eval_lv a gs st lval in + let addr = eval_lv ~ctx st lval in if (AD.is_top addr) then st else - let old_val = get a gs st addr None in (* None is ok here, we could try to get more precise, but this is ok (reading at unknown position in array) *) + let old_val = get ~ctx st addr None in (* None is ok here, we could try to get more precise, but this is ok (reading at unknown position in array) *) let t_lval = Cilfacade.typeOfLval lval in let old_val = map_oldval old_val t_lval in let old_val = @@ -78,8 +78,8 @@ struct else old_val in - let state_with_excluded = set a gs st addr t_lval value ~ctx in - let value = get a gs state_with_excluded addr None in + let state_with_excluded = set st addr t_lval value ~ctx in + let value = get ~ctx state_with_excluded addr None in let new_val = apply_invariant ~old_val ~new_val:value in if M.tracing then M.traceu "invariant" "New value is %a\n" VD.pretty new_val; (* make that address meet the invariant, i.e exclusion sets will be joined *) @@ -88,18 +88,18 @@ struct contra st ) else if VD.is_bot new_val - then set a gs st addr t_lval value ~ctx (* no *_raw because this is not a real assignment *) - else set a gs st addr t_lval new_val ~ctx (* no *_raw because this is not a real assignment *) + then set st addr t_lval value ~ctx (* no *_raw because this is not a real assignment *) + else set st addr t_lval new_val ~ctx (* no *_raw because this is not a real assignment *) - let refine_lv ctx a gs st c x c' pretty exp = - let set' lval v st = set a gs st (eval_lv a gs st lval) (Cilfacade.typeOfLval lval) ~lval_raw:lval v ~ctx in + let refine_lv ctx st c x c' pretty exp = + let set' lval v st = set st (eval_lv ~ctx st lval) (Cilfacade.typeOfLval lval) ~lval_raw:lval v ~ctx in match x with | Var var, o when refine_entire_var -> (* For variables, this is done at to the level of entire variables to benefit e.g. from disjunctive struct domains *) - let old_val = get_var a gs st var in + let old_val = get_var ~ctx st var in let old_val = map_oldval old_val var.vtype in - let offs = convert_offset a gs st o in - let new_val = VD.update_offset (Queries.to_value_domain_ask a) old_val offs c' (Some exp) x (var.vtype) in + let offs = convert_offset ~ctx st o in + let new_val = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) old_val offs c' (Some exp) x (var.vtype) in let v = apply_invariant ~old_val ~new_val in if is_some_bot v then contra st else ( @@ -111,7 +111,7 @@ struct | Var _, _ | Mem _, _ -> (* For accesses via pointers, not yet *) - let old_val = eval_rv_lval_refine a gs st exp x in + let old_val = eval_rv_lval_refine ~ctx st exp x in let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in let v = apply_invariant ~old_val ~new_val:c' in if is_some_bot v then contra st @@ -120,7 +120,7 @@ struct set' x v st ) - let invariant_fallback ctx a (gs:V.t -> G.t) st exp tv = + let invariant_fallback ctx st exp tv = (* We use a recursive helper function so that x != 0 is false can be handled * as x == 0 is true etc *) let rec helper (op: binop) (lval: lval) (value: VD.t) (tv: bool): (lval * VD.t) option = @@ -147,7 +147,7 @@ struct end | Address n -> begin if M.tracing then M.tracec "invariant" "Yes, %a is not %a\n" d_lval x AD.pretty n; - match eval_rv_address a gs st (Lval x) with + match eval_rv_address ~ctx st (Lval x) with | Address a when AD.is_definite n -> Some (x, Address (AD.diff a n)) | Top when AD.is_null n -> @@ -211,12 +211,12 @@ struct let switchedOp = function Lt -> Gt | Gt -> Lt | Le -> Ge | Ge -> Le | x -> x in (* a op b <=> b (switchedOp op) b *) match exp with (* Since we handle not only equalities, the order is important *) - | BinOp(op, Lval x, rval, typ) -> helper op x (VD.cast (Cilfacade.typeOfLval x) (eval_rv a gs st rval)) tv + | BinOp(op, Lval x, rval, typ) -> helper op x (VD.cast (Cilfacade.typeOfLval x) (eval_rv ~ctx st rval)) tv | BinOp(op, rval, Lval x, typ) -> derived_invariant (BinOp(switchedOp op, Lval x, rval, typ)) tv | BinOp(op, CastE (t1, c1), CastE (t2, c2), t) when (op = Eq || op = Ne) && typeSig t1 = typeSig t2 && VD.is_safe_cast t1 (Cilfacade.typeOf c1) && VD.is_safe_cast t2 (Cilfacade.typeOf c2) -> derived_invariant (BinOp (op, c1, c2, t)) tv | BinOp(op, CastE (TInt (ik, _) as t1, Lval x), rval, typ) -> - (match eval_rv a gs st (Lval x) with + (match eval_rv ~ctx st (Lval x) with | Int v -> (* This is tricky: It it is not sufficient to check that ID.cast_to_ik v = v * If there is one domain that knows this to be true and the other does not, we @@ -240,16 +240,16 @@ struct in match derived_invariant exp tv with | Some (lval, value) -> - refine_lv_fallback ctx a gs st lval value tv + refine_lv_fallback ctx st lval value tv | None -> if M.tracing then M.traceu "invariant" "Doing nothing.\n"; M.debug ~category:Analyzer "Invariant failed: expression \"%a\" not understood." d_exp exp; st - let invariant ctx a gs st exp tv: D.t = + let invariant ctx st exp tv: D.t = let fallback reason st = if M.tracing then M.tracel "inv" "Can't handle %a.\n%t\n" d_plainexp exp reason; - invariant_fallback ctx a gs st exp tv + invariant_fallback ctx st exp tv in (* inverse values for binary operation a `op` b == c *) (* ikind is the type of a for limiting ranges of the operands a, b. The only binops which can have different types for a, b are Shiftlt, Shiftrt (not handled below; don't use ikind to limit b there). *) @@ -555,7 +555,7 @@ struct a, b with FloatDomain.ArithmeticOnFloatBot _ -> raise Analyses.Deadcode in - let eval e st = eval_rv a gs st e in + let eval e st = eval_rv ~ctx st e in let eval_bool e st = match eval e st with Int i -> ID.to_bool i | _ -> None in let unroll_fk_of_exp e = match unrollType (Cilfacade.typeOf e) with @@ -696,7 +696,7 @@ struct | Float c -> invert_binary_op c FD.pretty (fun ik -> FD.to_int ik c) (fun fk -> FD.cast_to fk c) | _ -> failwith "unreachable") | Lval x, (Int _ | Float _ | Address _) -> (* meet x with c *) - let update_lval c x c' pretty = refine_lv ctx a gs st c x c' pretty exp in + let update_lval c x c' pretty = refine_lv ctx st c x c' pretty exp in let t = Cil.unrollType (Cilfacade.typeOfLval x) in (* unroll type to deal with TNamed *) if M.tracing then M.trace "invSpecial" "invariant with Lval %a, c_typed %a, type %a\n" d_lval x VD.pretty c_typed d_type t; begin match c_typed with