From 7c50968b1487c8c72037eaf11b598388790cbf50 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 5 Jan 2024 13:39:44 +0200 Subject: [PATCH] Add st back everywhere (as for now) --- src/analyses/base.ml | 181 +++++++++++++++++----------------- src/analyses/baseInvariant.ml | 10 +- 2 files changed, 96 insertions(+), 95 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 86d45720e4..63f516c82c 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -680,14 +680,14 @@ struct !collected (* The evaluation function as mutually recursive eval_lv & eval_rv *) - let rec eval_rv ~(ctx: _ ctx) (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 ~ctx 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 @@ -696,8 +696,8 @@ 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 ~ctx exp = - let eval_next () = eval_rv_no_ask_evalint ~ctx 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 @@ -720,25 +720,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 ~ctx exp = - eval_rv_base ~ctx 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 ~ctx exp = + and eval_rv_back_up ~ctx st exp = if get_bool "ana.base.eval.deep-query" then - eval_rv ~ctx 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 ~ctx 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 ~ctx (exp:exp): value = - let st = ctx.local in + 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 = @@ -760,7 +759,7 @@ struct match constFold true exp with (* Integer literals *) (* seems like constFold already converts CChr to CInt *) - | Const (CChr x) -> eval_rv ~ctx (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))) @@ -780,8 +779,8 @@ struct (* 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 ~ctx e1 in - let a2 = eval_rv ~ctx 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 (Analyses.ask_of_ctx ctx) op t1 a1 t2 a2 typ with | Int i -> ID.to_bool i = Some true @@ -790,7 +789,7 @@ struct 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 ~ctx 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 *) @@ -823,8 +822,8 @@ struct let eqs_value: value option = let* eqs = split exp in let* (e, es) = find_common eqs in - let v = eval_rv ~ctx e in (* value of common exp *) - let vs = List.map (eval_rv ~ctx) 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 -> @@ -866,25 +865,25 @@ struct in begin match eqs_value with | Some x -> x - | None -> evalbinop ~ctx 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 ~ctx op ~e1 ~e2 typ + evalbinop ~ctx st op ~e1 ~e2 typ (* Unary operators *) | UnOp (op,arg1,typ) -> - let a1 = eval_rv ~ctx 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 ~ctx 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 ~ctx lval)) - | CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~ctx (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 ~ctx exp in + let v = eval_rv ~ctx st exp in VD.cast ~torg:(Cilfacade.typeOf exp) t v | SizeOf _ | Real _ @@ -902,7 +901,7 @@ struct and eval_rv_base_lval ~eval_lv ~ctx (st: store) (exp: exp) (lv: lval): value = match lv with - | (Var v, ofs) -> get ~ctx st (eval_lv ~ctx (Var v, ofs)) (Some exp) + | (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;*) @@ -915,7 +914,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 ~ctx 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 = @@ -953,20 +952,20 @@ struct 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 (Analyses.ask_of_ctx ctx)) (fun x -> get ~ctx st x (Some exp)) v' (convert_offset ~ctx 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 ~ctx (op: binop) ~(e1:exp) ?(t1:typ option) ~(e2:exp) ?(t2:typ option) (t:typ): value = - evalbinop_mustbeequal ~ctx 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 ~ctx (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 ask = Analyses.ask_of_ctx ctx in - let a1 = eval_rv ~ctx e1 in - let a2 = eval_rv ~ctx 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 ask op t1 a1 t2 a2 t in @@ -1005,48 +1004,48 @@ struct (* A hackish evaluation of expressions that should immediately yield an * address, e.g. when calling functions. *) - and eval_fv ~ctx (exp:exp): AD.t = + and eval_fv ~ctx st (exp:exp): AD.t = match exp with - | Lval lval -> eval_lv ~ctx lval - | _ -> eval_tv ~ctx exp + | Lval lval -> eval_lv ~ctx st lval + | _ -> eval_tv ~ctx st exp (* Used also for thread creation: *) - and eval_tv ~ctx (exp:exp): AD.t = - match eval_rv ~ctx 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 ~ctx exp = - match eval_rv ~ctx 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 ~ctx (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 ~ctx 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 ~ctx ofs) + `Index (IdxDom.top (), convert_offset ~ctx st ofs) | Index (exp, ofs) -> - match eval_rv ~ctx exp with - | Int i -> `Index (iDtoIdx i, convert_offset ~ctx ofs) - | Address add -> `Index (AD.to_int add, convert_offset ~ctx ofs) - | Top -> `Index (IdxDom.top (), convert_offset ~ctx ofs) - | Bot -> `Index (IdxDom.bot (), convert_offset ~ctx 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 ~ctx (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 ~ctx 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 ~ctx n with + match eval_rv ~ctx st n with | Address adr -> ( if AD.is_null adr then ( @@ -1059,14 +1058,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 ctx.local.cpa) && not (is_global (Analyses.ask_of_ctx ctx) 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 ~ctx 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 @@ -1080,15 +1079,15 @@ struct (* 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 ~ctx (st: store) (exp:exp): value = try - let r = eval_rv ~ctx 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 ~ctx 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 ~ctx 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 *) @@ -1109,7 +1108,7 @@ struct Queries.Result.top q (* query cycle *) else ( match q with - | EvalInt e -> query_evalint ~ctx e (* mimic EvalInt query since eval_rv needs it *) + | EvalInt e -> query_evalint ~ctx st e (* mimic EvalInt query since eval_rv needs it *) | _ -> Queries.Result.top q ) and gs = function `Left _ -> `Lifted1 (Priv.G.top ()) | `Right _ -> `Lifted2 (VD.top ()) (* the expression is guaranteed to not contain globals *) @@ -1133,7 +1132,7 @@ struct | _ -> None let eval_funvar ctx fval: Queries.AD.t = - let fp = eval_fv ~ctx 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 @@ -1264,7 +1263,7 @@ struct JmpBufDomain.JmpBufSet.top () end | Q.EvalInt e -> - query_evalint ~ctx 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 ~ctx ctx.local e with @@ -1723,7 +1722,7 @@ struct char_array_hack (); 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 ~ctx 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 = @@ -1755,7 +1754,7 @@ struct assert (offs = NoOffset); VD.Bot end else - eval_rv_keep_bot ~ctx (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 *) @@ -1866,7 +1865,7 @@ struct if not (Cil.isArrayType v.vtype) then ctx.local else - let lval = eval_lv ~ctx (Var v, NoOffset) in + 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 @@ -2005,7 +2004,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 ~ctx 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 @@ -2156,7 +2155,7 @@ struct in let addr_type_of_exp exp = let lval = mkMem ~addr:(Cil.stripCasts exp) ~off:NoOffset in - let addr = eval_lv ~ctx lval in + let addr = eval_lv ~ctx ctx.local lval in (addr, AD.type_of addr) in let forks, multiple = forkfun ctx lv f args in @@ -2182,7 +2181,7 @@ 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 ~ctx 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 @@ -2234,7 +2233,7 @@ 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 ~ctx 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 st lv_a lv_typ (f s1_a s2_a) @@ -2250,7 +2249,7 @@ struct (* else compute value in array domain *) else let lv_a, lv_typ = match lv with - | Some lv_val -> eval_lv ~ctx 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 ~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) @@ -2318,7 +2317,7 @@ struct | Strlen s, _ -> begin match lv with | Some lv_val -> - let dest_a = eval_lv ~ctx 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 ~ctx st s in let a = address_from_value v in @@ -2346,8 +2345,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 ~ctx (mkMem ~addr:(Cil.stripCasts haystack) ~off:NoOffset)) - | CArrays.IsMaybeSubstr -> Address (AD.join (eval_lv ~ctx + | 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 @@ -2381,12 +2380,12 @@ struct | MutexAttrSetType {attr = attr; typ = mtyp}, _ -> begin let get_type lval = - let address = eval_lv ~ctx 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 ~ctx dst_lval in + let dest_a = eval_lv ~ctx st dst_lval in match eval_rv ~ctx st mtyp with | Int x -> begin @@ -2471,7 +2470,7 @@ struct end in begin match lv with - | Some lv_val -> set ~ctx st (eval_lv ~ctx 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 *) @@ -2504,8 +2503,8 @@ struct | 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 size); *) - set_many ~ctx st [(heap_var, TVoid [], Blob (VD.bot (), eval_int ~ctx size, true)); - (eval_lv ~ctx lv, (Cilfacade.typeOfLval lv), Address heap_var)] + 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 @@ -2517,8 +2516,8 @@ struct else AD.of_var (heap_var false ctx) in (* 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 size, true)); - (eval_lv ~ctx lv, (Cilfacade.typeOfLval lv), Address heap_var)] + 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 }, _ -> @@ -2530,12 +2529,12 @@ 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 ~ctx size in - let countval = eval_int ~ctx 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 st [ (add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false)); - (eval_lv ~ctx 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 ( @@ -2543,7 +2542,7 @@ struct (* 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 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 ~ctx 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 @@ -2564,7 +2563,7 @@ struct 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 ~ctx st p_addr' None in (* implicitly includes join of malloc value (VD.bot) *) - let size_int = eval_int ~ctx size in + 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' = @@ -2573,7 +2572,7 @@ struct else heap_addr in - let lv_addr = eval_lv ~ctx lv in + 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'); @@ -2597,7 +2596,7 @@ struct in begin match lv with | Some lv -> - set ~ctx st' (eval_lv ~ctx 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}, _ -> @@ -2624,7 +2623,7 @@ struct begin match lv with | Some x -> let result:value = (Int (ID.starting IInt Z.zero)) in - set ~ctx st (eval_lv ~ctx x) (Cilfacade.typeOfLval x) result + set ~ctx st (eval_lv ~ctx st x) (Cilfacade.typeOfLval x) result | None -> st end | _, _ -> @@ -2746,7 +2745,7 @@ struct match lval with | None -> st - | Some lval -> set_savetop ~ctx st (eval_lv ~ctx 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 @@ -2844,11 +2843,13 @@ struct module V = V module G = G + let ost = octx.local + (* all evals happen in octx with non-top values *) - let eval_rv ~ctx e = eval_rv ~ctx:octx e - let eval_rv_address ~ctx e = eval_rv_address ~ctx:octx e - let eval_lv ~ctx lv = eval_lv ~ctx:octx lv - let convert_offset ~ctx o = convert_offset ~ctx:octx 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 @@ -2922,7 +2923,7 @@ struct Priv.enter_multithreaded ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st | Events.AssignSpawnedThread (lval, tid) -> (* TODO: is this type right? *) - set ~ctx ctx.local (eval_lv ~ctx 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 4d51895683..e66a431ccf 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -17,8 +17,8 @@ sig 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 -> lval -> AD.t - val convert_offset: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> offset -> ID.t Offset.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: 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 @@ -64,7 +64,7 @@ struct 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 ~ctx lval in + let addr = eval_lv ~ctx st lval in if (AD.is_top addr) then st else 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) *) @@ -92,13 +92,13 @@ struct else set st addr t_lval new_val ~ctx (* no *_raw because this is not a real assignment *) let refine_lv ctx st c x c' pretty exp = - let set' lval v st = set st (eval_lv ~ctx lval) (Cilfacade.typeOfLval lval) ~lval_raw:lval v ~ctx in + 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 ~ctx st var in let old_val = map_oldval old_val var.vtype in - let offs = convert_offset ~ctx o 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