diff --git a/goblint.opam b/goblint.opam index 661222805b..bf51924626 100644 --- a/goblint.opam +++ b/goblint.opam @@ -74,12 +74,11 @@ dev-repo: "git+https://github.com/goblint/analyzer.git" # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project # also remember to generate/adjust goblint.opam.locked! available: os-distribution != "alpine" & arch != "arm64" -# pin-depends: [ - # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed - # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ] +pin-depends: [ + [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331" ] # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) - # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] -# ] + [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] +] post-messages: [ "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"} ] diff --git a/goblint.opam.locked b/goblint.opam.locked index bb59c41dd1..2744d2fe92 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -128,3 +128,14 @@ conflicts: [ post-messages: [ "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"} ] +# TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936 +pin-depends: [ + [ + "goblint-cil.2.0.2" + "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331" + ] + [ + "ppx_deriving.5.2.1" + "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" + ] +] diff --git a/goblint.opam.template b/goblint.opam.template index 6259c4d498..d8e25cde38 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -1,12 +1,11 @@ # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project # also remember to generate/adjust goblint.opam.locked! available: os-distribution != "alpine" & arch != "arm64" -# pin-depends: [ - # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed - # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ] +pin-depends: [ + [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331" ] # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) - # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] -# ] + [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] +] post-messages: [ "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"} ] diff --git a/src/analyses/base.ml b/src/analyses/base.ml index c8c13fe3ef..f69f93a097 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -150,8 +150,8 @@ struct let longjmp_return = ref dummyFunDec.svar - let heap_var ctx = - let info = match (ctx.ask Q.HeapVar) with + let heap_var on_stack ctx = + let info = match (ctx.ask (Q.AllocVar {on_stack})) with | `Lifted vinfo -> vinfo | _ -> failwith("Ran without a malloc analysis.") in info @@ -570,6 +570,8 @@ 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 drop_non_ptrs (st:CPA.t) : CPA.t = if CPA.is_top st then st else let rec replace_val = function @@ -759,7 +761,8 @@ struct (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))) | Const (CReal (_,fkind, Some str)) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.of_string fkind str) (* prefer parsing from string due to higher precision *) - | Const (CReal (num, fkind, None)) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.of_const fkind num) + | Const (CReal (num, fkind, None)) when not (Cilfacade.isComplexFKind fkind) && num = 0.0 -> Float (FD.of_const fkind num) (* constant 0 is ok, CIL creates these for zero-initializers; it is safe across float types *) + | Const (CReal (_, fkind, None)) when not (Cilfacade.isComplexFKind fkind) -> assert false (* Cil does not create other CReal without string representation *) (* String literals *) | Const (CStr (x,_)) -> Address (AD.of_string x) (* normal 8-bit strings, type: char* *) | Const (CWStr (xs,_) as c) -> (* wide character strings, type: wchar_t* *) @@ -1097,20 +1100,15 @@ struct | Int x -> ValueDomain.ID.to_int x | _ -> None - let eval_funvar ctx fval: varinfo list = - let exception OnlyUnknown in - try - let fp = eval_fv (Analyses.ask_of_ctx ctx) ctx.global ctx.local fval in - if AD.mem Addr.UnknownPtr fp then begin - let others = AD.to_var_may fp in - if others = [] then raise OnlyUnknown; - M.warn ~category:Imprecise "Function pointer %a may contain unknown functions." d_exp fval; - dummyFunDec.svar :: others - end else - AD.to_var_may fp - with SetDomain.Unsupported _ | OnlyUnknown -> - M.warn ~category:Unsound "Unknown call to function %a." d_exp fval; - [dummyFunDec.svar] + let eval_funvar ctx fval: Queries.AD.t = + let fp = eval_fv (Analyses.ask_of_ctx ctx) ctx.global 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 + else + M.warn ~category:Imprecise ~tags:[Category Call] "Function pointer %a may contain unknown functions." d_exp fval + ); + fp (** Evaluate expression as address. Avoids expensive Apron EvalInt if the Int result would be useless to us anyway. *) @@ -1125,6 +1123,10 @@ struct (* interpreter end *) + let is_not_heap_alloc_var ctx v = + let is_alloc = ctx.ask (Queries.IsAllocVar v) in + not is_alloc || (is_alloc && not (ctx.ask (Queries.IsHeapVar v))) + let query_invariant ctx context = let cpa = ctx.local.BaseDomain.cpa in let ask = Analyses.ask_of_ctx ctx in @@ -1204,10 +1206,7 @@ struct let query ctx (type a) (q: a Q.t): a Q.result = match q with | Q.EvalFunvar e -> - begin - let fs = eval_funvar ctx e in - List.fold_left (fun xs v -> Q.LS.add (v,`NoOffset) xs) (Q.LS.empty ()) fs - end + eval_funvar ctx e | Q.EvalJumpBuf e -> begin match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with | Address jmp_buf -> @@ -1247,17 +1246,26 @@ struct end | Q.EvalValue e -> eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e - | Q.BlobSize e -> begin + | 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 (* ignore @@ printf "BlobSize %a MayPointTo %a\n" d_plainexp e VD.pretty p; *) match p with | Address a -> (* If there's a non-heap var or an offset in the lval set, we answer with bottom *) + (* If we're asking for the BlobSize from the base address, then don't check for offsets => we want to avoid getting bot *) if AD.exists (function - | Addr (v,o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || o <> `NoOffset + | Addr (v,o) -> is_not_heap_alloc_var ctx v || (if not from_base_addr then o <> `NoOffset else false) | _ -> false) a then Queries.Result.bot q else ( + (* If we need the BlobSize from the base address, then remove any offsets *) + let a = + if from_base_addr then AD.map (function + | Addr (v, o) -> Addr (v, `NoOffset) + | addr -> addr) a + else + a + in let r = get ~full:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local a None in (* ignore @@ printf "BlobSize %a = %a\n" d_plainexp e VD.pretty r; *) (match r with @@ -1270,6 +1278,7 @@ struct match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global 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 @@ -1287,7 +1296,17 @@ struct | 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 - List.fold_left (AD.join) (AD.empty ()) addrs + 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 *) + else + addrs' + | Int i -> + begin match Cilfacade.typeOf e with + | t when Cil.isPointerType t -> AD.of_int i (* integer used as pointer *) + | _ + | exception Cilfacade.TypeOfError _ -> AD.empty () (* avoid unknown pointer result for non-pointer expression *) + end | _ -> AD.empty () end | Q.ReachableUkTypes e -> begin @@ -1383,7 +1402,7 @@ struct let t = match t_override with | Some t -> t | None -> - if a.f (Q.IsHeapVar x) then + if a.f (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 @@ -1429,7 +1448,7 @@ struct (* 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 (IsHeapVar x)) && offs = `NoOffset then begin + let old_value = if not invariant && Cil.isIntegralType x.vtype && not (a.f (IsAllocVar x)) && offs = `NoOffset then begin VD.bot_value ~varAttr:x.vattr lval_type end else Priv.read_global a priv_getg st x @@ -1970,7 +1989,7 @@ struct end let special_unknown_invalidate ctx ask gs st f args = - (if CilType.Varinfo.equal f dummyFunDec.svar then M.warn ~category:Imprecise "Unknown function ptr called"); + (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 let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in @@ -1995,7 +2014,7 @@ struct let check_invalid_mem_dealloc ctx special_fn ptr = let has_non_heap_var = AD.exists (function - | Addr (v,_) -> not (ctx.ask (Q.IsHeapVar v)) + | Addr (v,_) -> is_not_heap_alloc_var ctx v | _ -> false) in let has_non_zero_offset = AD.exists (function @@ -2012,6 +2031,7 @@ struct M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 761] "Free of memory not at start of buffer in function %s for pointer %a" special_fn.vname d_exp ptr | _ -> M.warn ~category:MessageCategory.Analyzer "Pointer %a in function %s doesn't evaluate to a valid address." d_exp ptr special_fn.vname + let special ctx (lv:lval option) (f: varinfo) (args: exp list) = let invalidate_ret_lv st = match lv with | Some lv -> @@ -2147,7 +2167,7 @@ struct 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 - | Memcpy { dest = dst; src }, _ -> + | Memcpy { dest = dst; src; n; }, _ -> (* TODO: use n *) 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 @@ -2322,13 +2342,22 @@ struct | Unknown, "__goblint_assume_join" -> let id = List.hd args in Priv.thread_join ~force:true (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) id st + | Alloca size, _ -> begin + 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)] + | _ -> st + end | Malloc size, _ -> begin match lv with | Some lv -> let heap_var = if (get_bool "sem.malloc.fail") - then AD.join (AD.of_var (heap_var ctx)) AD.null_ptr - else AD.of_var (heap_var ctx) + 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)); @@ -2338,7 +2367,7 @@ struct | Calloc { count = n; size }, _ -> begin match lv with | Some lv -> (* array length is set to one, as num*size is done when turning into `Calloc *) - let heap_var = heap_var ctx in + let heap_var = heap_var false ctx in let add_null addr = if get_bool "sem.malloc.fail" then AD.join addr AD.null_ptr (* calloc can fail and return NULL *) @@ -2381,7 +2410,7 @@ struct 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 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 ctx) in + let heap_addr = AD.of_var (heap_var false ctx) in let heap_addr' = if get_bool "sem.malloc.fail" then AD.join heap_addr AD.null_ptr @@ -2459,34 +2488,38 @@ struct in 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 : Q.LS.t) : store = + let combine_st ctx (local_st : store) (fun_st : store) (tainted_lvs : AD.t) : store = let ask = (Analyses.ask_of_ctx ctx) in - Q.LS.fold (fun (v, o) st -> - if CPA.mem v fun_st.cpa then - let lval = Mval.Exp.to_cil (v,o) in - let address = eval_lv ask ctx.global st lval in - let lval_type = (AD.type_of address) in - if M.tracing then M.trace "taintPC" "updating %a; type: %a\n" Mval.Exp.pretty (v, o) d_type lval_type; - match (CPA.find_opt v (fun_st.cpa)), lval_type 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} - (* "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 - 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 - | 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 - match val_opt with - | None -> accCPA - | Some new_val -> CPA.add v new_val accCPA ) deps st'.cpa)} - end - else st) tainted_lvs local_st + AD.fold (fun addr st -> + 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 + 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 + (* 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} + (* "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 + 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 + | 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 + match val_opt with + | None -> accCPA + | Some new_val -> CPA.add v new_val accCPA ) deps st'.cpa)} + end + else st + | _ -> st + ) tainted_lvs local_st let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) = let combine_one (st: D.t) (fun_st: D.t) = @@ -2501,9 +2534,9 @@ struct let cpa_noreturn = CPA.remove (return_varinfo ()) fun_st.cpa 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 Q.LS.pretty tainted; + 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; - if Q.LS.is_top tainted then + if AD.is_top tainted then let cpa_local = CPA.filter (fun x _ -> not (is_global ask x)) st.cpa in let cpa' = CPA.fold CPA.add cpa_noreturn cpa_local in (* add cpa_noreturn to cpa_local *) if M.tracing then M.trace "taintPC" "combined: %a\n" CPA.pretty cpa'; @@ -2518,7 +2551,10 @@ struct let cpa_caller' = CPA.fold CPA.add cpa_new cpa_caller in if M.tracing then M.trace "taintPC" "cpa_caller': %a\n" CPA.pretty cpa_caller'; (* remove lvals from the tainted set that correspond to variables for which we just added a new mapping from the callee*) - let tainted = Q.LS.filter (fun (v, _) -> not (CPA.mem v cpa_new)) tainted in + let tainted = AD.filter (function + | Addr.Addr (v,_) -> not (CPA.mem v cpa_new) + | _ -> false + ) tainted in let st_combined = combine_st ctx {st with cpa = cpa_caller'} fun_st tainted in if M.tracing then M.trace "taintPC" "combined: %a\n" CPA.pretty st_combined.cpa; { fun_st with cpa = st_combined.cpa } @@ -2622,6 +2658,7 @@ struct | MayBeThreadReturn | PartAccess _ | IsHeapVar _ + | IsAllocVar _ | IsMultiple _ | CreatedThreads | MustJoinedThreads -> diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 70c6ed9101..72e00efbb1 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -805,15 +805,15 @@ struct | BinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _, _) -> true | _ -> false in - try - let ik = Cilfacade.get_ikind_exp exp in + match Cilfacade.get_ikind_exp exp with + | ik -> let itv = if not tv || is_cmp exp then (* false is 0, but true can be anything that is not 0, except for comparisons which yield 1 *) ID.of_bool ik tv (* this will give 1 for true which is only ok for comparisons *) else ID.of_excl_list ik [BI.zero] (* Lvals, Casts, arithmetic operations etc. should work with true = non_zero *) in inv_exp (Int itv) exp st - with Invalid_argument _ -> + | exception Invalid_argument _ -> let fk = Cilfacade.get_fkind_exp exp in let ftv = if not tv then (* false is 0, but true can be anything that is not 0, except for comparisons which yield 1 *) FD.of_const fk 0. diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 1b92cb320d..db75455b40 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -60,14 +60,10 @@ struct ask.f (Q.MustBeProtectedBy {mutex=m; global=x; write=true; protection}) let protected_vars (ask: Q.ask): varinfo list = - let module VS = Set.Make (CilType.Varinfo) in - Q.LS.fold (fun (v, _) acc -> - let m = ValueDomain.Addr.of_var v in (* TODO: don't ignore offsets *) - Q.LS.fold (fun l acc -> - VS.add (fst l) acc (* always `NoOffset from mutex analysis *) - ) (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc - ) (ask.f Q.MustLockset) VS.empty - |> VS.elements + Q.AD.fold (fun m acc -> + Q.VS.join (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc + ) (ask.f Q.MustLockset) (Q.VS.empty ()) + |> Q.VS.elements end module MutexGlobals = @@ -126,10 +122,8 @@ struct if !AnalysisState.global_initialization then Lockset.empty () else - let ls = ask.f Queries.MustLockset in - Q.LS.fold (fun (var, offs) acc -> - Lockset.add (Lock.of_mval (var, Lock.Offs.of_exp offs)) acc - ) ls (Lockset.empty ()) + let ad = ask.f Queries.MustLockset in + Q.AD.fold (fun mls acc -> Lockset.add mls acc) ad (Lockset.empty ()) (* TODO: use AD as Lockset *) (* TODO: reversed SetDomain.Hoare *) module MinLocksets = HoareDomain.Set_LiftTop (MustLockset) (struct let topname = "All locksets" end) (* reverse Lockset because Hoare keeps maximal, but we need minimal *) diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 94de4fbf82..72a4261cb5 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -43,6 +43,7 @@ type math = (** Type of special function, or {!Unknown}. *) (* Use inline record if not single {!Cil.exp} argument. *) type special = + | Alloca of Cil.exp | Malloc of Cil.exp | Calloc of { count: Cil.exp; size: Cil.exp; } | Realloc of { ptr: Cil.exp; size: Cil.exp; } @@ -57,12 +58,17 @@ type special = | Broadcast of Cil.exp | MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; } | MutexInit of { mutex:Cil.exp; attr: Cil.exp; } + (* All Sem specials are not used yet. *) + | SemInit of { sem: Cil.exp; pshared: Cil.exp; value: Cil.exp; } + | SemWait of { sem: Cil.exp; try_:bool; timeout: Cil.exp option;} + | SemPost of Cil.exp + | SemDestroy of Cil.exp | Wait of { cond: Cil.exp; mutex: Cil.exp; } | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) } | Math of { fun_args: math; } | Memset of { dest: Cil.exp; ch: Cil.exp; count: Cil.exp; } | Bzero of { dest: Cil.exp; count: Cil.exp; } - | Memcpy of { dest: Cil.exp; src: Cil.exp } + | Memcpy of { dest: Cil.exp; src: Cil.exp; n: Cil.exp; } | Strcpy of { dest: Cil.exp; src: Cil.exp; n: Cil.exp option; } | Strcat of { dest: Cil.exp; src: Cil.exp; n: Cil.exp option; } | Strlen of Cil.exp @@ -126,31 +132,10 @@ type t = { attrs: attr list; (** Attributes of function. *) } -let special_of_old classify_name = fun args -> - match classify_name args with - | `Malloc e -> Malloc e - | `Calloc (count, size) -> Calloc { count; size; } - | `Realloc (ptr, size) -> Realloc { ptr; size; } - | `Lock (try_, write, return_on_success) -> - begin match args with - | [lock] -> Lock { lock ; try_; write; return_on_success; } - | [] -> failwith "lock has no arguments" - | _ -> failwith "lock has multiple arguments" - end - | `Unlock -> - begin match args with - | [arg] -> Unlock arg - | [] -> failwith "unlock has no arguments" - | _ -> failwith "unlock has multiple arguments" - end - | `ThreadCreate (thread, start_routine, arg) -> ThreadCreate { thread; start_routine; arg; } - | `ThreadJoin (thread, ret_var) -> ThreadJoin { thread; ret_var; } - | `Unknown _ -> Unknown - -let of_old ?(attrs: attr list=[]) (old_accesses: Accesses.old) (classify_name): t = { +let of_old ?(attrs: attr list=[]) (old_accesses: Accesses.old): t = { attrs; accs = Accesses.of_old old_accesses; - special = special_of_old classify_name; + special = fun _ -> Unknown; } module MathPrintable = struct diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 137a3103a5..c4d1acf76a 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -12,12 +12,13 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("memset", special [__ "dest" [w]; __ "ch" []; __ "count" []] @@ fun dest ch count -> Memset { dest; ch; count; }); ("__builtin_memset", special [__ "dest" [w]; __ "ch" []; __ "count" []] @@ fun dest ch count -> Memset { dest; ch; count; }); ("__builtin___memset_chk", special [__ "dest" [w]; __ "ch" []; __ "count" []; drop "os" []] @@ fun dest ch count -> Memset { dest; ch; count; }); - ("memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src }); - ("__builtin_memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src }); - ("__builtin___memcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "n" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src }); - ("memmove", special [__ "dest" [w]; __ "src" [r]; drop "count" []] @@ fun dest src -> Memcpy { dest; src }); - ("__builtin_memmove", special [__ "dest" [w]; __ "src" [r]; drop "count" []] @@ fun dest src -> Memcpy { dest; src }); - ("__builtin___memmove_chk", special [__ "dest" [w]; __ "src" [r]; drop "count" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src }); + ("memcpy", special [__ "dest" [w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Memcpy { dest; src; n; }); + ("__builtin_memcpy", special [__ "dest" [w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Memcpy { dest; src; n; }); + ("__builtin___memcpy_chk", special [__ "dest" [w]; __ "src" [r]; __ "n" []; drop "os" []] @@ fun dest src n -> Memcpy { dest; src; n; }); + ("memccpy", special [__ "dest" [w]; __ "src" [r]; drop "c" []; __ "n" []] @@ fun dest src n -> Memcpy {dest; src; n; }); (* C23 *) (* TODO: use c *) + ("memmove", special [__ "dest" [w]; __ "src" [r]; __ "count" []] @@ fun dest src count -> Memcpy { dest; src; n = count; }); + ("__builtin_memmove", special [__ "dest" [w]; __ "src" [r]; __ "count" []] @@ fun dest src count -> Memcpy { dest; src; n = count; }); + ("__builtin___memmove_chk", special [__ "dest" [w]; __ "src" [r]; __ "count" []; drop "os" []] @@ fun dest src count -> Memcpy { dest; src; n = count; }); ("strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src; n = None; }); ("__builtin_strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src; n = None; }); ("__builtin___strcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "os" []] @@ fun dest src -> Strcpy { dest; src; n = None; }); @@ -30,6 +31,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strncat", special [__ "dest" [r; w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Strcat { dest; src; n = Some n; }); ("__builtin_strncat", special [__ "dest" [r; w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Strcat { dest; src; n = Some n; }); ("__builtin___strncat_chk", special [__ "dest" [r; w]; __ "src" [r]; __ "n" []; drop "os" []] @@ fun dest src n -> Strcat { dest; src; n = Some n; }); + ("memcmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]); + ("memchr", unknown [drop "s" [r]; drop "c" []; drop "n" []]); ("asctime", unknown ~attrs:[ThreadUnsafe] [drop "time_ptr" [r_deep]]); ("fclose", unknown [drop "stream" [r_deep; w_deep; f_deep]]); ("feof", unknown [drop "stream" [r_deep; w_deep]]); @@ -63,7 +66,11 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strtok", unknown ~attrs:[ThreadUnsafe] [drop "str" [r; w]; drop "delim" [r]]); ("__builtin_strcmp", special [__ "s1" [r]; __ "s2" [r]] @@ fun s1 s2 -> Strcmp { s1; s2; n = None; }); ("strncmp", special [__ "s1" [r]; __ "s2" [r]; __ "n" []] @@ fun s1 s2 n -> Strcmp { s1; s2; n = Some n; }); + ("strchr", unknown [drop "s" [r]; drop "c" []]); + ("__builtin_strchr", unknown [drop "s" [r]; drop "c" []]); + ("strrchr", unknown [drop "s" [r]; drop "c" []]); ("malloc", special [__ "size" []] @@ fun size -> Malloc size); + ("calloc", special [__ "n" []; __ "size" []] @@ fun n size -> Calloc {count = n; size}); ("realloc", special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size }); ("free", special [__ "ptr" [f]] @@ fun ptr -> Free ptr); ("abort", special [] Abort); @@ -84,6 +91,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("getchar", unknown []); ("putchar", unknown [drop "ch" []]); ("puts", unknown [drop "s" [r]]); + ("srand", unknown [drop "seed" []]); ("rand", special ~attrs:[ThreadUnsafe] [] Rand); ("strerror", unknown ~attrs:[ThreadUnsafe] [drop "errnum" []]); ("strspn", unknown [drop "s" [r]; drop "accept" [r]]); @@ -117,12 +125,25 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("wcrtomb", unknown ~attrs:[ThreadUnsafe] [drop "s" [w]; drop "wc" []; drop "ps" [r_deep; w_deep]]); ("wcstombs", unknown ~attrs:[ThreadUnsafe] [drop "dst" [w]; drop "src" [r]; drop "size" []]); ("wcsrtombs", unknown ~attrs:[ThreadUnsafe] [drop "dst" [w]; drop "src" [r_deep; w]; drop "size" []; drop "ps" [r_deep; w_deep]]); + ("mbstowcs", unknown [drop "dest" [w]; drop "src" [r]; drop "n" []]); ("abs", unknown [drop "j" []]); ("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]); ("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]); ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *) ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value }); + ("atexit", unknown [drop "function" [s]]); + ("atoi", unknown [drop "nptr" [r]]); + ("atol", unknown [drop "nptr" [r]]); + ("atoll", unknown [drop "nptr" [r]]); + ("setlocale", unknown [drop "category" []; drop "locale" [r]]); + ("clock", unknown []); + ("atomic_flag_clear", unknown [drop "obj" [w]]); + ("atomic_flag_clear_explicit", unknown [drop "obj" [w]; drop "order" []]); + ("atomic_flag_test_and_set", unknown [drop "obj" [r; w]]); + ("atomic_flag_test_and_set_explicit", unknown [drop "obj" [r; w]; drop "order" []]); + ("atomic_load", unknown [drop "obj" [r]]); + ("atomic_store", unknown [drop "obj" [w]; drop "desired" []]); ] (** C POSIX library functions. @@ -144,7 +165,6 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("dbm_nextkey", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep]]); ("dbm_open", unknown ~attrs:[ThreadUnsafe] [drop "file" [r; w]; drop "open_flags" []; drop "file_mode" []]); ("dbm_store", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep; w_deep]; drop "key" []; drop "content" []; drop "store_mode" []]); - ("dlerror", unknown ~attrs:[ThreadUnsafe] []); ("drand48", unknown ~attrs:[ThreadUnsafe] []); ("encrypt", unknown ~attrs:[ThreadUnsafe] [drop "block" [r; w]; drop "edflag" []]); ("setkey", unknown ~attrs:[ThreadUnsafe] [drop "key" [r]]); @@ -203,6 +223,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("fileno", unknown [drop "stream" [r_deep; w_deep]]); ("fdopen", unknown [drop "fd" []; drop "mode" [r]]); ("getopt", unknown ~attrs:[ThreadUnsafe] [drop "argc" []; drop "argv" [r_deep]; drop "optstring" [r]]); + ("getopt_long", unknown ~attrs:[ThreadUnsafe] [drop "argc" []; drop "argv" [r_deep]; drop "optstring" [r_deep]; drop "longopts" [r]; drop "longindex" [w]]); ("iconv_open", unknown [drop "tocode" [r]; drop "fromcode" [r]]); ("iconv", unknown [drop "cd" [r]; drop "inbuf" [r]; drop "inbytesleft" [r;w]; drop "outbuf" [w]; drop "outbytesleft" [r;w]]); ("iconv_close", unknown [drop "cd" [f]]); @@ -229,9 +250,15 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("hstrerror", unknown [drop "err" []]); ("inet_ntoa", unknown ~attrs:[ThreadUnsafe] [drop "in" []]); ("getsockopt", unknown [drop "sockfd" []; drop "level" []; drop "optname" []; drop "optval" [w]; drop "optlen" [w]]); + ("setsockopt", unknown [drop "sockfd" []; drop "level" []; drop "optname" []; drop "optval" [r]; drop "optlen" []]); + ("getsockname", unknown [drop "sockfd" []; drop "addr" [w_deep]; drop "addrlen" [w]]); ("gethostbyaddr", unknown ~attrs:[ThreadUnsafe] [drop "addr" [r_deep]; drop "len" []; drop "type" []]); ("gethostbyaddr_r", unknown [drop "addr" [r_deep]; drop "len" []; drop "type" []; drop "ret" [w_deep]; drop "buf" [w]; drop "buflen" []; drop "result" [w]; drop "h_errnop" [w]]); ("gethostbyname", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); + ("gethostbyname_r", unknown [drop "name" [r]; drop "result_buf" [w_deep]; drop "buf" [w]; drop "buflen" []; drop "result" [w]; drop "h_errnop" [w]]); + ("gethostname", unknown [drop "name" [w]; drop "len" []]); + ("getpeername", unknown [drop "sockfd" []; drop "addr" [w_deep]; drop "addrlen" [r; w]]); + ("socket", unknown [drop "domain" []; drop "type" []; drop "protocol" []]); ("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]); ("tcgetattr", unknown [drop "fd" []; drop "termios_p" [w_deep]]); ("tcsetattr", unknown [drop "fd" []; drop "optional_actions" []; drop "termios_p" [r_deep]]); @@ -246,6 +273,8 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("timer_gettime", unknown [drop "timerid" []; drop "curr_value" [w_deep]]); ("timer_getoverrun", unknown [drop "timerid" []]); ("lstat", unknown [drop "pathname" [r]; drop "statbuf" [w]]); + ("fstat", unknown [drop "fd" []; drop "buf" [w]]); + ("fstatat", unknown [drop "dirfd" []; drop "pathname" [r]; drop "buf" [w]; drop "flags" []]); ("getpwnam", unknown [drop "name" [r]]); ("chdir", unknown [drop "path" [r]]); ("closedir", unknown [drop "dirp" [r]]); @@ -256,7 +285,9 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("read", unknown [drop "fd" []; drop "buf" [w]; drop "count" []]); ("write", unknown [drop "fd" []; drop "buf" [r]; drop "count" []]); ("recv", unknown [drop "sockfd" []; drop "buf" [w]; drop "len" []; drop "flags" []]); + ("recvfrom", unknown [drop "sockfd" []; drop "buf" [w]; drop "len" []; drop "flags" []; drop "src_addr" [w_deep]; drop "addrlen" [r; w]]); ("send", unknown [drop "sockfd" []; drop "buf" [r]; drop "len" []; drop "flags" []]); + ("sendto", unknown [drop "sockfd" []; drop "buf" [r]; drop "len" []; drop "flags" []; drop "dest_addr" [r_deep]; drop "addrlen" []]); ("strdup", unknown [drop "s" [r]]); ("strndup", unknown [drop "s" [r]; drop "n" []]); ("syscall", unknown (drop "number" [] :: VarArgs (drop' [r; w]))); @@ -292,12 +323,78 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("getaddrinfo", unknown [drop "node" [r]; drop "service" [r]; drop "hints" [r_deep]; drop "res" [w]]); (* only write res non-deep because it doesn't write to existing fields of res *) ("fnmatch", unknown [drop "pattern" [r]; drop "string" [r]; drop "flags" []]); ("realpath", unknown [drop "path" [r]; drop "resolved_path" [w]]); + ("dprintf", unknown (drop "fd" [] :: drop "format" [r] :: VarArgs (drop' [r]))); + ("vdprintf", unknown [drop "fd" []; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) + ("mkdtemp", unknown [drop "template" [r; w]]); + ("mkstemp", unknown [drop "template" [r; w]]); + ("regcomp", unknown [drop "preg" [w_deep]; drop "regex" [r]; drop "cflags" []]); + ("regexec", unknown [drop "preg" [r_deep]; drop "string" [r]; drop "nmatch" []; drop "pmatch" [w_deep]; drop "eflags" []]); + ("regfree", unknown [drop "preg" [f_deep]]); + ("ffs", unknown [drop "i" []]); + ("_exit", special [drop "status" []] Abort); + ("execvp", unknown [drop "file" [r]; drop "argv" [r_deep]]); + ("execl", unknown (drop "path" [r] :: drop "arg" [r] :: VarArgs (drop' [r]))); + ("statvfs", unknown [drop "path" [r]; drop "buf" [w]]); + ("readlink", unknown [drop "path" [r]; drop "buf" [w]; drop "bufsz" []]); + ("wcswidth", unknown [drop "s" [r]; drop "n" []]); + ("link", unknown [drop "oldpath" [r]; drop "newpath" [r]]); + ("renameat", unknown [drop "olddirfd" []; drop "oldpath" [r]; drop "newdirfd" []; drop "newpath" [r]]); + ("posix_fadvise", unknown [drop "fd" []; drop "offset" []; drop "len" []; drop "advice" []]); + ("lockf", unknown [drop "fd" []; drop "cmd" []; drop "len" []]); + ("htonl", unknown [drop "hostlong" []]); + ("htons", unknown [drop "hostshort" []]); + ("ntohl", unknown [drop "netlong" []]); + ("ntohs", unknown [drop "netshort" []]); + ("sleep", unknown [drop "seconds" []]); + ("usleep", unknown [drop "usec" []]); + ("nanosleep", unknown [drop "req" [r]; drop "rem" [w]]); + ("setpriority", unknown [drop "which" []; drop "who" []; drop "prio" []]); + ("getpriority", unknown [drop "which" []; drop "who" []]); + ("sched_yield", unknown []); + ("getpid", unknown []); + ("getppid", unknown []); + ("getuid", unknown []); + ("geteuid", unknown []); + ("getpgrp", unknown []); + ("setrlimit", unknown [drop "resource" []; drop "rlim" [r]]); + ("getrlimit", unknown [drop "resource" []; drop "rlim" [w]]); + ("setsid", unknown []); + ("isatty", unknown [drop "fd" []]); + ("sigemptyset", unknown [drop "set" [w]]); + ("sigfillset", unknown [drop "set" [w]]); + ("sigaddset", unknown [drop "set" [r; w]; drop "signum" []]); + ("sigdelset", unknown [drop "set" [r; w]; drop "signum" []]); + ("sigismember", unknown [drop "set" [r]; drop "signum" []]); + ("sigprocmask", unknown [drop "how" []; drop "set" [r]; drop "oldset" [w]]); + ("fork", unknown []); + ("dlopen", unknown [drop "filename" [r]; drop "flag" []]); + ("dlerror", unknown ~attrs:[ThreadUnsafe] []); + ("dlsym", unknown [drop "handle" [r]; drop "symbol" [r]]); + ("dlclose", unknown [drop "handle" [r]]); + ("inet_addr", unknown [drop "cp" [r]]); + ("uname", unknown [drop "buf" [w_deep]]); + ("strcasecmp", unknown [drop "s1" [r]; drop "s2" [r]]); + ("strncasecmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]); + ("connect", unknown [drop "sockfd" []; drop "sockaddr" [r_deep]; drop "addrlen" []]); + ("bind", unknown [drop "sockfd" []; drop "sockaddr" [r_deep]; drop "addrlen" []]); + ("listen", unknown [drop "sockfd" []; drop "backlog" []]); + ("select", unknown [drop "nfds" []; drop "readfds" [r; w]; drop "writefds" [r; w]; drop "exceptfds" [r; w]; drop "timeout" [r; w]]); + ("accept", unknown [drop "sockfd" []; drop "addr" [w_deep]; drop "addrlen" [r; w]]); + ("close", unknown [drop "fd" []]); + ("writev", unknown [drop "fd" []; drop "iov" [r_deep]; drop "iovcnt" []]); + ("readv", unknown [drop "fd" []; drop "iov" [w_deep]; drop "iovcnt" []]); + ("unlink", unknown [drop "pathname" [r]]); + ("popen", unknown [drop "command" [r]; drop "type" [r]]); + ("stat", unknown [drop "pathname" [r]; drop "statbuf" [w]]); + ("statfs", unknown [drop "path" [r]; drop "buf" [w]]); ] (** Pthread functions. *) let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pthread_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg }); (* For precision purposes arg is not considered accessed here. Instead all accesses (if any) come from actually analyzing start_routine. *) ("pthread_exit", special [__ "retval" []] @@ fun retval -> ThreadExit { ret_val = retval }); (* Doesn't dereference the void* itself, but just passes to pthread_join. *) + ("pthread_join", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval}); + ("pthread_kill", unknown [drop "thread" []; drop "sig" []]); ("pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]); ("__pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]); ("pthread_cond_signal", special [__ "cond" []] @@ fun cond -> Signal cond); @@ -322,16 +419,16 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pthread_mutexattr_destroy", unknown [drop "attr" [f]]); ("pthread_rwlock_init", unknown [drop "rwlock" [w]; drop "attr" [r]]); ("pthread_rwlock_destroy", unknown [drop "rwlock" [f]]); - ("pthread_rwlock_rdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = true}); - ("pthread_rwlock_tryrdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = true}); - ("pthread_rwlock_wrlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true}); + ("pthread_rwlock_rdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = false}); + ("pthread_rwlock_tryrdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = true; write = false; return_on_success = false}); + ("pthread_rwlock_wrlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = false}); ("pthread_rwlock_trywrlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = true; write = true; return_on_success = false}); ("pthread_rwlock_unlock", special [__ "rwlock" []] @@ fun rwlock -> Unlock rwlock); ("pthread_rwlockattr_init", unknown [drop "attr" [w]]); ("pthread_rwlockattr_destroy", unknown [drop "attr" [f]]); ("pthread_spin_init", unknown [drop "lock" [w]; drop "pshared" []]); ("pthread_spin_destroy", unknown [drop "lock" [f]]); - ("pthread_spin_lock", special [__ "lock" []] @@ fun lock -> Lock {lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true}); + ("pthread_spin_lock", special [__ "lock" []] @@ fun lock -> Lock {lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = false}); ("pthread_spin_trylock", special [__ "lock" []] @@ fun lock -> Lock {lock = lock; try_ = true; write = true; return_on_success = false}); ("pthread_spin_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock); ("pthread_attr_init", unknown [drop "attr" [w]]); @@ -356,9 +453,15 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pthread_condattr_setclock", unknown [drop "attr" [w]; drop "clock_id" []]); ("pthread_mutexattr_destroy", unknown [drop "attr" [f]]); ("pthread_attr_setschedparam", unknown [drop "attr" [r; w]; drop "param" [r]]); - ("sem_timedwait", unknown [drop "sem" [r]; drop "abs_timeout" [r]]); (* no write accesses to sem because sync primitive itself has no race *) ("pthread_setaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [r]]); ("pthread_getaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [w]]); + (* Not recording read accesses to sem as these are thread-safe anyway not to clutter messages (as for mutexes) **) + ("sem_init", special [__ "sem" []; __ "pshared" []; __ "value" []] @@ fun sem pshared value -> SemInit {sem; pshared; value}); + ("sem_wait", special [__ "sem" []] @@ fun sem -> SemWait {sem; try_ = false; timeout = None}); + ("sem_trywait", special [__ "sem" []] @@ fun sem -> SemWait {sem; try_ = true; timeout = None}); + ("sem_timedwait", special [__ "sem" []; __ "abs_timeout" [r]] @@ fun sem abs_timeout-> SemWait {sem; try_ = true; timeout = Some abs_timeout}); (* no write accesses to sem because sync primitive itself has no race *) + ("sem_post", special [__ "sem" []] @@ fun sem -> SemPost sem); + ("sem_destroy", special [__ "sem" []] @@ fun sem -> SemDestroy sem); ] (** GCC builtin functions. @@ -408,10 +511,25 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__builtin_popcountl", unknown [drop "x" []]); ("__builtin_popcountll", unknown [drop "x" []]); ("__atomic_store_n", unknown [drop "ptr" [w]; drop "val" []; drop "memorder" []]); + ("__atomic_store", unknown [drop "ptr" [w]; drop "val" [r]; drop "memorder" []]); ("__atomic_load_n", unknown [drop "ptr" [r]; drop "memorder" []]); + ("__atomic_load", unknown [drop "ptr" [r]; drop "ret" [w]; drop "memorder" []]); + ("__atomic_clear", unknown [drop "ptr" [w]; drop "memorder" []]); + ("__atomic_compare_exchange_n", unknown [drop "ptr" [r; w]; drop "expected" [r; w]; drop "desired" []; drop "weak" []; drop "success_memorder" []; drop "failure_memorder" []]); + ("__atomic_compare_exchange", unknown [drop "ptr" [r; w]; drop "expected" [r; w]; drop "desired" [r]; drop "weak" []; drop "success_memorder" []; drop "failure_memorder" []]); + ("__atomic_fetch_add", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]); + ("__atomic_fetch_sub", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]); + ("__atomic_fetch_and", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]); + ("__atomic_fetch_xor", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]); + ("__atomic_fetch_or", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]); + ("__atomic_fetch_nand", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]); + ("__atomic_test_and_set", unknown [drop "ptr" [r; w]; drop "memorder" []]); + ("__atomic_thread_fence", unknown [drop "memorder" []]); ("__sync_fetch_and_add", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' []))); ("__sync_fetch_and_sub", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' []))); ("__builtin_va_copy", unknown [drop "dest" [w]; drop "src" [r]]); + ("alloca", special [__ "size" []] @@ fun size -> Alloca size); + ("__builtin_alloca", special [__ "size" []] @@ fun size -> Alloca size); ] let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ @@ -452,8 +570,16 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strcasestr", unknown [drop "haystack" [r]; drop "needle" [r]]); ("inet_aton", unknown [drop "cp" [r]; drop "inp" [w]]); ("fopencookie", unknown [drop "cookie" []; drop "mode" [r]; drop "io_funcs" [s_deep]]); (* doesn't access cookie but passes it to io_funcs *) - ("mempcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src }); - ("__builtin___mempcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "n" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src }); + ("mempcpy", special [__ "dest" [w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Memcpy { dest; src; n; }); + ("__builtin___mempcpy_chk", special [__ "dest" [w]; __ "src" [r]; __ "n" []; drop "os" []] @@ fun dest src n -> Memcpy { dest; src; n; }); + ("rawmemchr", unknown [drop "s" [r]; drop "c" []]); + ("memrchr", unknown [drop "s" [r]; drop "c" []; drop "n" []]); + ("memmem", unknown [drop "haystack" [r]; drop "haystacklen" []; drop "needle" [r]; drop "needlelen" [r]]); + ("getifaddrs", unknown [drop "ifap" [w]]); + ("freeifaddrs", unknown [drop "ifa" [f_deep]]); + ("atoq", unknown [drop "nptr" [r]]); + ("strchrnul", unknown [drop "s" [r]; drop "c" []]); + ("getdtablesize", unknown []); ] let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ @@ -470,6 +596,15 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__xpg_basename", unknown [drop "path" [r]]); ("ptrace", unknown (drop "request" [] :: VarArgs (drop' [r_deep; w_deep]))); (* man page has 4 arguments, but header has varargs and real-world programs may call with <4 *) ("madvise", unknown [drop "addr" []; drop "length" []; drop "advice" []]); + ("inotify_init1", unknown [drop "flags" []]); + ("inotify_add_watch", unknown [drop "fd" []; drop "pathname" [r]; drop "mask" []]); + ("inotify_rm_watch", unknown [drop "fd" []; drop "wd" []]); + ("fts_open", unknown [drop "path_argv" [r_deep]; drop "options" []; drop "compar" [s]]); (* TODO: use Call instead of Spawn *) + ("fts_read", unknown [drop "ftsp" [r_deep; w_deep]]); + ("fts_close", unknown [drop "ftsp" [f_deep]]); + ("mount", unknown [drop "source" [r]; drop "target" [r]; drop "filesystemtype" [r]; drop "mountflags" []; drop "data" [r]]); + ("umount", unknown [drop "target" [r]]); + ("umount2", unknown [drop "target" [r]; drop "flags" []]); ] let big_kernel_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[big kernel lock]" intType))) @@ -530,6 +665,10 @@ let linux_kernel_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__cmpxchg_wrong_size", special [] Abort); ("__xadd_wrong_size", special [] Abort); ("__put_user_bad", special [] Abort); + ("kmalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Malloc size); + ("__kmalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Malloc size); + ("kzalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Calloc {count = Cil.one; size}); + ("usb_alloc_urb", special [__ "iso_packets" []; drop "mem_flags" []] @@ fun iso_packets -> Malloc MyCFG.unknown_exp); ] (** Goblint functions. *) @@ -793,6 +932,7 @@ let svcomp_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__VERIFIER_atomic_begin", special [] @@ Lock { lock = verifier_atomic; try_ = false; write = true; return_on_success = true }); ("__VERIFIER_atomic_end", special [] @@ Unlock verifier_atomic); ("__VERIFIER_nondet_loff_t", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *) + ("__VERIFIER_nondet_int", unknown []); (* declare invalidate actions to prevent invalidating globals when extern in regression tests *) ] let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ @@ -801,10 +941,14 @@ let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("wattrset", unknown [drop "win" [r_deep; w_deep]; drop "attrs" []]); ("endwin", unknown []); ("wgetch", unknown [drop "win" [r_deep; w_deep]]); + ("wget_wch", unknown [drop "win" [r_deep; w_deep]; drop "wch" [w]]); + ("unget_wch", unknown [drop "wch" []]); ("wmove", unknown [drop "win" [r_deep; w_deep]; drop "y" []; drop "x" []]); ("waddch", unknown [drop "win" [r_deep; w_deep]; drop "ch" []]); + ("waddnstr", unknown [drop "win" [r_deep; w_deep]; drop "str" [r]; drop "n" []]); ("waddnwstr", unknown [drop "win" [r_deep; w_deep]; drop "wstr" [r]; drop "n" []]); ("wattr_on", unknown [drop "win" [r_deep; w_deep]; drop "attrs" []; drop "opts" []]); (* opts argument currently not used *) + ("wattr_off", unknown [drop "win" [r_deep; w_deep]; drop "attrs" []; drop "opts" []]); (* opts argument currently not used *) ("wrefresh", unknown [drop "win" [r_deep; w_deep]]); ("mvprintw", unknown (drop "win" [r_deep; w_deep] :: drop "y" [] :: drop "x" [] :: drop "fmt" [r] :: VarArgs (drop' [r]))); ("initscr", unknown []); @@ -813,10 +957,19 @@ let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("start_color", unknown []); ("use_default_colors", unknown []); ("wclear", unknown [drop "win" [r_deep; w_deep]]); + ("wclrtoeol", unknown [drop "win" [r_deep; w_deep]]); ("can_change_color", unknown []); ("init_color", unknown [drop "color" []; drop "red" []; drop "green" []; drop "blue" []]); ("init_pair", unknown [drop "pair" []; drop "f" [r]; drop "b" [r]]); ("wbkgd", unknown [drop "win" [r_deep; w_deep]; drop "ch" []]); + ("keyname", unknown [drop "c" []]); + ("newterm", unknown [drop "type" [r]; drop "outfd" [r_deep; w_deep]; drop "infd" [r_deep; w_deep]]); + ("cbreak", unknown []); + ("nonl", unknown []); + ("keypad", unknown [drop "win" [r_deep; w_deep]; drop "bf" []]); + ("set_escdelay", unknown [drop "size" []]); + ("printw", unknown (drop "fmt" [r] :: VarArgs (drop' [r]))); + ("werase", unknown [drop "win" [r_deep; w_deep]]); ] let pcre_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ @@ -868,46 +1021,6 @@ let activated_library_descs: (string, LibraryDesc.t) Hashtbl.t ResettableLazy.t let reset_lazy () = ResettableLazy.reset activated_library_descs -type categories = [ - | `Malloc of exp - | `Calloc of exp * exp - | `Realloc of exp * exp - | `Lock of bool * bool * bool (* try? * write? * return on success *) - | `Unlock - | `ThreadCreate of exp * exp * exp (* id * f * x *) - | `ThreadJoin of exp * exp (* id * ret_var *) - | `Unknown of string ] - - -let classify fn exps: categories = - let strange_arguments () = - M.warn ~category:Program "%s arguments are strange!" fn; - `Unknown fn - in - match fn with - | "pthread_join" -> - begin match exps with - | [id; ret_var] -> `ThreadJoin (id, ret_var) - | _ -> strange_arguments () - end - | "kmalloc" | "__kmalloc" | "usb_alloc_urb" | "__builtin_alloca" -> - begin match exps with - | size::_ -> `Malloc size - | _ -> strange_arguments () - end - | "kzalloc" -> - begin match exps with - | size::_ -> `Calloc (Cil.one, size) - | _ -> strange_arguments () - end - | "calloc" -> - begin match exps with - | n::size::_ -> `Calloc (n, size) - | _ -> strange_arguments () - end - | x -> `Unknown x - - module Invalidate = struct [@@@warning "-unused-value-declaration"] (* some functions are not used below *) @@ -1004,8 +1117,6 @@ open Invalidate * We assume that no known functions that are reachable are executed/spawned. For that we use ThreadCreate above. *) (* WTF: why are argument numbers 1-indexed (in partition)? *) let invalidate_actions = [ - "atoi", readsAll; (*safe*) - "connect", readsAll; (*safe*) "__printf_chk", readsAll;(*safe*) "printk", readsAll;(*safe*) "__mutex_init", readsAll;(*safe*) @@ -1017,102 +1128,55 @@ let invalidate_actions = [ "__ctype_b_loc", readsAll;(*safe*) "__errno", readsAll;(*safe*) "__errno_location", readsAll;(*safe*) - "sigfillset", writesAll; (*unsafe*) - "sigprocmask", writesAll; (*unsafe*) - "uname", writesAll;(*unsafe*) - "getopt_long", writesAllButFirst 2 readsAll;(*drop 2*) "__strdup", readsAll;(*safe*) "strtoul__extinline", readsAll;(*safe*) - "geteuid", readsAll;(*safe*) "readdir_r", writesAll;(*unsafe*) "atoi__extinline", readsAll;(*safe*) - "getpid", readsAll;(*safe*) "_IO_getc", writesAll;(*unsafe*) "pipe", writesAll;(*unsafe*) - "close", writesAll;(*unsafe*) - "setsid", readsAll;(*safe*) "strerror_r", writesAll;(*unsafe*) - "sigemptyset", writesAll;(*unsafe*) - "sigaddset", writesAll;(*unsafe*) "raise", writesAll;(*unsafe*) "_strlen", readsAll;(*safe*) - "__builtin_alloca", readsAll;(*safe*) - "dlopen", readsAll;(*safe*) - "dlsym", readsAll;(*safe*) - "dlclose", readsAll;(*safe*) "stat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) - "__builtin_strchr", readsAll;(*safe*) - "getpgrp", readsAll;(*safe*) - "umount2", readsAll;(*safe*) - "memchr", readsAll;(*safe*) "waitpid", readsAll;(*safe*) - "statfs", writes [1;3;4];(*keep [1;3;4]*) - "mount", readsAll;(*safe*) "__open_alias", readsAll;(*safe*) "__open_2", readsAll;(*safe*) "ioctl", writesAll;(*unsafe*) "fstat__extinline", writesAll;(*unsafe*) - "umount", readsAll;(*safe*) - "strrchr", readsAll;(*safe*) "scandir", writes [1;3;4];(*keep [1;3;4]*) - "unlink", readsAll;(*safe*) - "sched_yield", readsAll;(*safe*) - "nanosleep", writesAllButFirst 1 readsAll;(*drop 1*) - "sigdelset", readsAll;(*safe*) "sigwait", writesAllButFirst 1 readsAll;(*drop 1*) - "setlocale", readsAll;(*safe*) "bindtextdomain", readsAll;(*safe*) "textdomain", readsAll;(*safe*) "dcgettext", readsAll;(*safe*) "putw", readsAll;(*safe*) "__getdelim", writes [3];(*keep [3]*) - "gethostbyname_r", readsAll;(*safe*) "__h_errno_location", readsAll;(*safe*) "__fxstat", readsAll;(*safe*) - "getuid", readsAll;(*safe*) "openlog", readsAll;(*safe*) - "getdtablesize", readsAll;(*safe*) "umask", readsAll;(*safe*) - "socket", readsAll;(*safe*) "clntudp_create", writesAllButFirst 3 readsAll;(*drop 3*) "svctcp_create", readsAll;(*safe*) "clntudp_bufcreate", writesAll;(*unsafe*) "authunix_create_default", readsAll;(*safe*) - "writev", readsAll;(*safe*) "clnt_broadcast", writesAll;(*unsafe*) "clnt_sperrno", readsAll;(*safe*) "pmap_unset", writesAll;(*unsafe*) - "bind", readsAll;(*safe*) "svcudp_create", readsAll;(*safe*) "svc_register", writesAll;(*unsafe*) - "sleep", readsAll;(*safe*) - "usleep", readsAll; "svc_run", writesAll;(*unsafe*) "dup", readsAll; (*safe*) "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*) "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*) - "strcasecmp", readsAll; (*safe*) - "strchr", readsAll; (*safe*) "__error", readsAll; (*safe*) "__maskrune", writesAll; (*unsafe*) - "inet_addr", readsAll; (*safe*) - "setsockopt", readsAll; (*safe*) - "listen", readsAll; (*safe*) - "getsockname", writes [1;3]; (*keep [1;3]*) - "execl", readsAll; (*safe*) - "select", writes [1;5]; (*keep [1;5]*) - "accept", writesAll; (*keep [1]*) - "getpeername", writes [1]; (*keep [1]*) "times", writesAll; (*unsafe*) "timespec_get", writes [1]; "__tolower", readsAll; (*safe*) "signal", writesAll; (*unsafe*) - "popen", readsAll; (*safe*) "BF_cfb64_encrypt", writes [1;3;4;5]; (*keep [1;3;4,5]*) "BZ2_bzBuffToBuffDecompress", writes [3;4]; (*keep [3;4]*) "uncompress", writes [3;4]; (*keep [3;4]*) - "stat", writes [2]; (*keep [1]*) "__xstat", writes [3]; (*keep [1]*) "__lxstat", writes [3]; (*keep [1]*) "remove", readsAll; @@ -1120,26 +1184,10 @@ let invalidate_actions = [ "compress2", writes [3]; (*keep [3]*) "__toupper", readsAll; (*safe*) "BF_set_key", writes [3]; (*keep [3]*) - "memcmp", readsAll; (*safe*) - "sendto", writes [2;4]; (*keep [2;4]*) - "recvfrom", writes [4;5]; (*keep [4;5]*) - "srand", readsAll; (*safe*) - "gethostname", writesAll; (*unsafe*) - "fork", readsAll; (*safe*) - "setrlimit", readsAll; (*safe*) - "getrlimit", writes [2]; (*keep [2]*) - "sem_init", readsAll; (*safe*) - "sem_destroy", readsAll; (*safe*) - "sem_wait", readsAll; (*safe*) - "sem_post", readsAll; (*safe*) "PL_NewHashTable", readsAll; (*safe*) "assert_failed", readsAll; (*safe*) - "htonl", readsAll; (*safe*) - "htons", readsAll; (*safe*) - "ntohl", readsAll; (*safe*) "munmap", readsAll;(*safe*) "mmap", readsAll;(*safe*) - "clock", readsAll; "__builtin_va_arg_pack_len", readsAll; "__open_too_many_args", readsAll; "usb_submit_urb", readsAll; (* first argument is written to but according to specification must not be read from anymore *) @@ -1148,11 +1196,6 @@ let invalidate_actions = [ "kmem_cache_create", readsAll; "idr_pre_get", readsAll; "zil_replay", writes [1;2;3;5]; - "__VERIFIER_nondet_int", readsAll; (* no args, declare invalidate actions to prevent invalidating globals when extern in regression tests *) - (* no args, declare invalidate actions to prevent invalidating globals *) - "isatty", readsAll; - "setpriority", readsAll; - "getpriority", readsAll; (* ddverify *) "sema_init", readsAll; "__goblint_assume_join", readsAll; @@ -1197,7 +1240,7 @@ let is_safe_uncalled fn_name = List.exists (fun r -> Str.string_match r fn_name 0) kernel_safe_uncalled_regex -let unknown_desc ~f name = (* TODO: remove name argument, unknown function shouldn't have classify *) +let unknown_desc f = let old_accesses (kind: AccessKind.t) args = match kind with | Write when GobConfig.get_bool "sem.unknown_function.invalidate.args" -> args | Write -> [] @@ -1215,16 +1258,12 @@ let unknown_desc ~f name = (* TODO: remove name argument, unknown function shoul else [] in - let classify_name args = - match classify name args with - | `Unknown _ as category -> - (* TODO: remove hack when all classify are migrated *) - if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then - M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname; - category - | category -> category - in - LibraryDesc.of_old ~attrs old_accesses classify_name + (* TODO: remove hack when all classify are migrated *) + if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then ( + M.msg_final Error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing"; + M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname + ); + LibraryDesc.of_old ~attrs old_accesses let find f = let name = f.vname in @@ -1233,9 +1272,9 @@ let find f = | None -> match get_invalidate_action name with | Some old_accesses -> - LibraryDesc.of_old old_accesses (classify name) + LibraryDesc.of_old old_accesses | None -> - unknown_desc ~f name + unknown_desc f let is_special fv = diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml index 1b6a7e5a1d..9eb21b77ef 100644 --- a/src/analyses/mCP.ml +++ b/src/analyses/mCP.ml @@ -144,7 +144,9 @@ struct let spawn_one v d = List.iter (fun (lval, args) -> ctx.spawn lval v args) d in - if not (get_bool "exp.single-threaded") then + if get_bool "exp.single-threaded" then + M.msg_final Error ~category:Unsound "Thread not spawned" + else iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs let do_sideg ctx (xs:(V.t * (WideningTokens.TS.t * G.t)) list) = diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml index 2c2b99a075..3a501fc72f 100644 --- a/src/analyses/mallocFresh.ml +++ b/src/analyses/mallocFresh.ml @@ -43,7 +43,7 @@ struct | Malloc _ | Calloc _ | Realloc _ -> - begin match ctx.ask HeapVar with + begin match ctx.ask (AllocVar {on_stack = false}) with | `Lifted var -> D.add var ctx.local | _ -> ctx.local end diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 1bff7611a4..8576096dfe 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -44,7 +44,7 @@ struct | Realloc _ -> (* Warn about multi-threaded programs as soon as we encounter a dynamic memory allocation function *) warn_for_multi_threaded ctx; - begin match ctx.ask Queries.HeapVar with + begin match ctx.ask (Queries.AllocVar {on_stack = false}) with | `Lifted var -> D.add var state | _ -> state end @@ -53,7 +53,7 @@ struct | ad when not (Queries.AD.is_top ad) && Queries.AD.cardinal ad = 1 -> (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *) begin match Queries.AD.choose ad with - | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> D.remove v state (* Unique pointed to heap vars *) + | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> D.remove v state (* Unique pointed to heap vars *) | _ -> state end | _ -> state diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml new file mode 100644 index 0000000000..7015e6f143 --- /dev/null +++ b/src/analyses/memOutOfBounds.ml @@ -0,0 +1,416 @@ +(** An analysis for the detection of out-of-bounds memory accesses ([memOutOfBounds]).*) + +open GoblintCil +open Analyses +open MessageCategory + +module AS = AnalysisState +module VDQ = ValueDomainQueries +module ID = IntDomain.IntDomTuple + +(* + Note: + * This functionality is implemented as an analysis solely for the sake of maintaining + separation of concerns, as well as for having the ablility to conveniently turn it on or off + * It doesn't track any internal state +*) +module Spec = +struct + include Analyses.IdentitySpec + + module D = Lattice.Unit + module C = D + + let context _ _ = () + + let name () = "memOutOfBounds" + + (* HELPER FUNCTIONS *) + + let intdom_of_int x = + ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x) + + let size_of_type_in_bytes typ = + let typ_size_in_bytes = (bitsSizeOf typ) / 8 in + intdom_of_int typ_size_in_bytes + + let rec exp_contains_a_ptr (exp:exp) = + match exp with + | Const _ + | SizeOf _ + | SizeOfStr _ + | AlignOf _ + | AddrOfLabel _ -> false + | Real e + | Imag e + | SizeOfE e + | AlignOfE e + | UnOp (_, e, _) + | CastE (_, e) -> exp_contains_a_ptr e + | BinOp (_, e1, e2, _) -> + exp_contains_a_ptr e1 || exp_contains_a_ptr e2 + | Question (e1, e2, e3, _) -> + exp_contains_a_ptr e1 || exp_contains_a_ptr e2 || exp_contains_a_ptr e3 + | Lval lval + | AddrOf lval + | StartOf lval -> lval_contains_a_ptr lval + + and lval_contains_a_ptr (lval:lval) = + let (host, offset) = lval in + let host_contains_a_ptr = function + | Var v -> isPointerType v.vtype + | Mem e -> exp_contains_a_ptr e + in + let rec offset_contains_a_ptr = function + | NoOffset -> false + | Index (e, o) -> exp_contains_a_ptr e || offset_contains_a_ptr o + | Field (f, o) -> isPointerType f.ftype || offset_contains_a_ptr o + in + host_contains_a_ptr host || offset_contains_a_ptr offset + + let points_to_heap_only ctx ptr = + match ctx.ask (Queries.MayPointTo ptr) with + | a when not (Queries.AD.is_top a)-> + Queries.AD.for_all (function + | Addr (v, o) -> ctx.ask (Queries.IsHeapVar v) + | _ -> false + ) a + | _ -> false + + let get_size_of_ptr_target ctx ptr = + if points_to_heap_only ctx ptr then + (* Ask for BlobSize from the base address (the second component being set to true) in order to avoid BlobSize giving us bot *) + ctx.ask (Queries.BlobSize {exp = ptr; base_address = true}) + else + match ctx.ask (Queries.MayPointTo ptr) with + | a when not (Queries.AD.is_top a) -> + let pts_list = Queries.AD.elements a in + let pts_elems_to_sizes (addr: Queries.AD.elt) = + begin match addr with + | Addr (v, _) -> + begin match v.vtype with + | TArray (item_typ, _, _) -> + let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in + begin match ctx.ask (Queries.EvalLength ptr) with + | `Lifted arr_len -> + let arr_len_casted = ID.cast_to (Cilfacade.ptrdiff_ikind ()) arr_len in + begin + try `Lifted (ID.mul item_typ_size_in_bytes arr_len_casted) + with IntDomain.ArithmeticOnIntegerBot _ -> `Bot + end + | `Bot -> `Bot + | `Top -> `Top + end + | _ -> + let type_size_in_bytes = size_of_type_in_bytes v.vtype in + `Lifted type_size_in_bytes + end + | _ -> `Top + end + in + (* Map each points-to-set element to its size *) + let pts_sizes = List.map pts_elems_to_sizes pts_list in + (* Take the smallest of all sizes that ptr's contents may have *) + begin match pts_sizes with + | [] -> `Bot + | [x] -> x + | x::xs -> List.fold_left VDQ.ID.join x xs + end + | _ -> + M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; + `Top + + let get_ptr_deref_type ptr_typ = + match ptr_typ with + | TPtr (t, _) -> Some t + | _ -> None + + let eval_ptr_offset_in_binop ctx exp ptr_contents_typ = + let eval_offset = ctx.ask (Queries.EvalInt exp) in + let ptr_contents_typ_size_in_bytes = size_of_type_in_bytes ptr_contents_typ in + match eval_offset with + | `Lifted eo -> + let casted_eo = ID.cast_to (Cilfacade.ptrdiff_ikind ()) eo in + begin + try `Lifted (ID.mul casted_eo ptr_contents_typ_size_in_bytes) + with IntDomain.ArithmeticOnIntegerBot _ -> `Bot + end + | `Top -> `Top + | `Bot -> `Bot + + let rec offs_to_idx typ offs = + match offs with + | `NoOffset -> intdom_of_int 0 + | `Field (field, o) -> + let field_as_offset = Field (field, NoOffset) in + let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset in + let bytes_offset = intdom_of_int (bits_offset / 8) in + let remaining_offset = offs_to_idx field.ftype o in + begin + try ID.add bytes_offset remaining_offset + with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () + end + | `Index (x, o) -> + begin try + let typ_size_in_bytes = size_of_type_in_bytes typ in + let bytes_offset = ID.mul typ_size_in_bytes x in + let remaining_offset = offs_to_idx typ o in + ID.add bytes_offset remaining_offset + with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () + end + + let rec get_addr_offs ctx ptr = + match ctx.ask (Queries.MayPointTo ptr) with + | a when not (VDQ.AD.is_top a) -> + let ptr_deref_type = get_ptr_deref_type @@ typeOf ptr in + begin match ptr_deref_type with + | Some t -> + begin match VDQ.AD.is_empty a with + | true -> + M.warn "Pointer %a has an empty points-to-set" d_exp ptr; + ID.top_of @@ Cilfacade.ptrdiff_ikind () + | false -> + if VDQ.AD.exists (function + | Addr (_, o) -> ID.is_bot @@ offs_to_idx t o + | _ -> false + ) a then ( + (* TODO: Uncomment once staging-memsafety branch changes are applied *) + (* set_mem_safety_flag InvalidDeref; *) + M.warn "Pointer %a has a bot address offset. An invalid memory access may occur" d_exp ptr + ) else if VDQ.AD.exists (function + | Addr (_, o) -> ID.is_bot @@ offs_to_idx t o + | _ -> false + ) a then ( + (* TODO: Uncomment once staging-memsafety branch changes are applied *) + (* set_mem_safety_flag InvalidDeref; *) + M.warn "Pointer %a has a top address offset. An invalid memory access may occur" d_exp ptr + ); + (* Offset should be the same for all elements in the points-to set *) + (* Hence, we can just pick one element and obtain its offset *) + begin match VDQ.AD.choose a with + | Addr (_, o) -> offs_to_idx t o + | _ -> ID.top_of @@ Cilfacade.ptrdiff_ikind () + end + end + | None -> + M.error "Expression %a doesn't have pointer type" d_exp ptr; + ID.top_of @@ Cilfacade.ptrdiff_ikind () + end + | _ -> + M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; + ID.top_of @@ Cilfacade.ptrdiff_ikind () + + and check_lval_for_oob_access ctx ?(is_implicitly_derefed = false) lval = + if not @@ lval_contains_a_ptr lval then () + else + (* If the lval doesn't indicate an explicit dereference, we still need to check for an implicit dereference *) + (* An implicit dereference is, e.g., printf("%p", ptr), where ptr is a pointer *) + match lval, is_implicitly_derefed with + | (Var _, _), false -> () + | (Var v, _), true -> check_no_binop_deref ctx (Lval lval) + | (Mem e, _), _ -> + begin match e with + | Lval (Var v, _) as lval_exp -> check_no_binop_deref ctx lval_exp + | BinOp (binop, e1, e2, t) when binop = PlusPI || binop = MinusPI || binop = IndexPI -> + check_binop_exp ctx binop e1 e2 t; + check_exp_for_oob_access ctx ~is_implicitly_derefed e1; + check_exp_for_oob_access ctx ~is_implicitly_derefed e2 + | _ -> check_exp_for_oob_access ctx ~is_implicitly_derefed e + end + + and check_no_binop_deref ctx lval_exp = + let behavior = Undefined MemoryOutOfBoundsAccess in + let cwe_number = 823 in + let ptr_size = get_size_of_ptr_target ctx lval_exp in + let addr_offs = get_addr_offs ctx lval_exp in + let ptr_type = typeOf lval_exp in + let ptr_contents_type = get_ptr_deref_type ptr_type in + match ptr_contents_type with + | Some t -> + begin match ptr_size, addr_offs with + | `Top, _ -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp + | `Bot, _ -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp + | `Lifted ps, ao -> + let casted_ps = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ps in + let casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ao in + let ptr_size_lt_offs = ID.lt casted_ps casted_ao in + begin match ID.to_bool ptr_size_lt_offs with + | Some true -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer is %a (in bytes). It is offset by %a (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur" ID.pretty casted_ps ID.pretty casted_ao + | Some false -> () + | None -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of pointer (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_ps ID.pretty casted_ao + end + end + | _ -> M.error "Expression %a is not a pointer" d_exp lval_exp + + and check_exp_for_oob_access ctx ?(is_implicitly_derefed = false) exp = + match exp with + | Const _ + | SizeOf _ + | SizeOfStr _ + | AlignOf _ + | AddrOfLabel _ -> () + | Real e + | Imag e + | SizeOfE e + | AlignOfE e + | UnOp (_, e, _) + | CastE (_, e) -> check_exp_for_oob_access ctx ~is_implicitly_derefed e + | BinOp (bop, e1, e2, t) -> + check_exp_for_oob_access ctx ~is_implicitly_derefed e1; + check_exp_for_oob_access ctx ~is_implicitly_derefed e2 + | Question (e1, e2, e3, _) -> + check_exp_for_oob_access ctx ~is_implicitly_derefed e1; + check_exp_for_oob_access ctx ~is_implicitly_derefed e2; + check_exp_for_oob_access ctx ~is_implicitly_derefed e3 + | Lval lval + | StartOf lval + | AddrOf lval -> check_lval_for_oob_access ctx ~is_implicitly_derefed lval + + and check_binop_exp ctx binop e1 e2 t = + let binopexp = BinOp (binop, e1, e2, t) in + let behavior = Undefined MemoryOutOfBoundsAccess in + let cwe_number = 823 in + match binop with + | PlusPI + | IndexPI + | MinusPI -> + let ptr_size = get_size_of_ptr_target ctx e1 in + let addr_offs = get_addr_offs ctx e1 in + let ptr_type = typeOf e1 in + let ptr_contents_type = get_ptr_deref_type ptr_type in + begin match ptr_contents_type with + | Some t -> + let offset_size = eval_ptr_offset_in_binop ctx e2 t in + (* Make sure to add the address offset to the binop offset *) + let offset_size_with_addr_size = match offset_size with + | `Lifted os -> + let casted_os = ID.cast_to (Cilfacade.ptrdiff_ikind ()) os in + let casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) addr_offs in + begin + try `Lifted (ID.add casted_os casted_ao) + with IntDomain.ArithmeticOnIntegerBot _ -> `Bot + end + | `Top -> `Top + | `Bot -> `Bot + in + begin match ptr_size, offset_size_with_addr_size with + | `Top, _ -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is top. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp + | _, `Top -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is top. Memory out-of-bounds access might occur" d_exp binopexp + | `Bot, _ -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is bottom. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp + | _, `Bot -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is bottom. Memory out-of-bounds access might occur" d_exp binopexp + | `Lifted ps, `Lifted o -> + let casted_ps = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ps in + let casted_o = ID.cast_to (Cilfacade.ptrdiff_ikind ()) o in + let ptr_size_lt_offs = ID.lt casted_ps casted_o in + begin match ID.to_bool ptr_size_lt_offs with + | Some true -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp ID.pretty casted_ps ID.pretty casted_o + | Some false -> () + | None -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare pointer size (%a) with offset (%a). Memory out-of-bounds access may occur" ID.pretty casted_ps ID.pretty casted_o + end + end + | _ -> M.error "Binary expression %a doesn't have a pointer" d_exp binopexp + end + | _ -> () + + (* For memset() and memcpy() *) + let check_count ctx fun_name dest n = + let (behavior:MessageCategory.behavior) = Undefined MemoryOutOfBoundsAccess in + let cwe_number = 823 in + let dest_size = get_size_of_ptr_target ctx dest in + let eval_n = ctx.ask (Queries.EvalInt n) in + let addr_offs = get_addr_offs ctx dest in + match dest_size, eval_n with + | `Top, _ -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp dest fun_name + | _, `Top -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name + | `Bot, _ -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp dest fun_name + | _, `Bot -> + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is bottom" fun_name + | `Lifted ds, `Lifted en -> + let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in + let casted_en = ID.cast_to (Cilfacade.ptrdiff_ikind ()) en in + let casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) addr_offs in + let dest_size_lt_count = ID.lt casted_ds (ID.add casted_en casted_ao) in + begin match ID.to_bool dest_size_lt_count with + | Some true -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en + | Some false -> () + | None -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of dest (%a) with address offset (%a) count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en fun_name + end + + + (* TRANSFER FUNCTIONS *) + + let assign ctx (lval:lval) (rval:exp) : D.t = + check_lval_for_oob_access ctx lval; + check_exp_for_oob_access ctx rval; + ctx.local + + let branch ctx (exp:exp) (tv:bool) : D.t = + check_exp_for_oob_access ctx exp; + ctx.local + + let return ctx (exp:exp option) (f:fundec) : D.t = + Option.iter (fun x -> check_exp_for_oob_access ctx x) exp; + ctx.local + + let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = + let desc = LibraryFunctions.find f in + let is_arg_implicitly_derefed arg = + let read_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = false } arglist in + let read_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = true } arglist in + let write_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } arglist in + let write_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } arglist in + List.mem arg read_shallow_args || List.mem arg read_deep_args || List.mem arg write_shallow_args || List.mem arg write_deep_args + in + Option.iter (fun x -> check_lval_for_oob_access ctx x) lval; + List.iter (fun arg -> check_exp_for_oob_access ctx ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) arg) arglist; + (* Check calls to memset and memcpy for out-of-bounds-accesses *) + match desc.special arglist with + | Memset { dest; ch; count; } -> check_count ctx f.vname dest count; + | Memcpy { dest; src; n = count; } -> check_count ctx f.vname dest count; + | _ -> (); + ctx.local + + let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = + List.iter (fun arg -> check_exp_for_oob_access ctx arg) args; + [ctx.local, ctx.local] + + let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t = + Option.iter (fun x -> check_lval_for_oob_access ctx x) lval; + ctx.local + + let startstate v = () + let exitstate v = () +end + +let _ = + MCP.register_analysis (module Spec : MCPSpec) \ No newline at end of file diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml index 0375bd3f74..5dae8748cb 100644 --- a/src/analyses/modifiedSinceLongjmp.ml +++ b/src/analyses/modifiedSinceLongjmp.ml @@ -23,29 +23,23 @@ struct (* Only checks for v.vglob on purpose, acessing espaced locals after longjmp is UB like for any local *) not v.vglob (* *) && not (BaseUtil.is_volatile v) && v.vstorage <> Static - let relevants_from_ls ls = - if Queries.LS.is_top ls then - VS.top () - else - Queries.LS.fold (fun (v, _) acc -> if is_relevant v then VS.add v acc else acc) ls (VS.empty ()) - - let relevants_from_ad ad = + let relevants_from_ad ls = (* TODO: what about AD with both known and unknown pointers? *) - if Queries.AD.is_top ad then + if Queries.AD.is_top ls then VS.top () else - Queries.AD.fold (fun addr vs -> + Queries.AD.fold (fun addr acc -> match addr with - | Queries.AD.Addr.Addr (v,_) -> if is_relevant v then VS.add v vs else vs - | _ -> vs - ) ad (VS.empty ()) + | Queries.AD.Addr.Addr (v, _) when is_relevant v -> VS.add v acc + | _ -> acc + ) ls (VS.empty ()) (* transfer functions *) let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = [ctx.local, D.bot ()] (* enter with bot as opposed to IdentitySpec *) let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) = - let taintedcallee = relevants_from_ls (f_ask.f Queries.MayBeTainted) in + let taintedcallee = relevants_from_ad (f_ask.f Queries.MayBeTainted) in add_to_all_defined taintedcallee ctx.local let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask) : D.t = diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 7d8298a0a4..5a61976ef5 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -233,21 +233,15 @@ struct Mutexes.leq mutex_lockset protecting | Queries.MustLockset -> let held_locks = Lockset.export_locks (Lockset.filter snd ls) in - let ls = Mutexes.fold (fun addr ls -> - match Addr.to_mval addr with - | Some (var, offs) -> Queries.LS.add (var, Addr.Offs.to_exp offs) ls - | None -> ls - ) held_locks (Queries.LS.empty ()) - in - ls + Mutexes.fold (fun addr ls -> Queries.AD.add addr ls) held_locks (Queries.AD.empty ()) | Queries.MustBeAtomic -> let held_locks = Lockset.export_locks (Lockset.filter snd ls) in Mutexes.mem (LockDomain.Addr.of_var LF.verifier_atomic_var) held_locks | Queries.MustProtectedVars {mutex = m; write} -> let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected m))) in VarSet.fold (fun v acc -> - Queries.LS.add (v, `NoOffset) acc - ) protected (Queries.LS.empty ()) + Queries.VS.add v acc + ) protected (Queries.VS.empty ()) | Queries.IterSysVars (Global g, f) -> f (Obj.repr (V.protecting g)) (* TODO: something about V.protected? *) | WarnGlobal g -> diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml index 1bd4b6d544..acd687835e 100644 --- a/src/analyses/poisonVariables.ml +++ b/src/analyses/poisonVariables.ml @@ -15,12 +15,16 @@ struct let context _ _ = () - let check_mval tainted ((v, offset): Queries.LS.elt) = - if not v.vglob && VS.mem v tainted then - M.warn ~category:(Behavior (Undefined Other)) "Reading poisonous variable %a" CilType.Varinfo.pretty v + let check_mval tainted (addr: Queries.AD.elt) = + match addr with + | Queries.AD.Addr.Addr (v,_) -> + if not v.vglob && VS.mem v tainted then + M.warn ~category:(Behavior (Undefined Other)) "Reading poisonous variable %a" CilType.Varinfo.pretty v + | _ -> () - let rem_mval tainted ((v, offset): Queries.LS.elt) = match offset with - | `NoOffset -> VS.remove v tainted + let rem_mval tainted (addr: Queries.AD.elt) = + match addr with + | Queries.AD.Addr.Addr (v,`NoOffset) -> VS.remove v tainted | _ -> tainted (* If there is an offset, it is a bit harder to remove, as we don't know where the indeterminate value is *) @@ -88,11 +92,8 @@ struct | ad when Queries.AD.is_top ad && not (VS.is_empty octx.local) -> M.warn ~category:(Behavior (Undefined Other)) "reading unknown memory location, may be tainted!" | ad -> - Queries.AD.iter (function - (* Use original access state instead of current with removed written vars. *) - | Queries.AD.Addr.Addr (v,o) -> check_mval octx.local (v, ValueDomain.Offs.to_exp o) - | _ -> () - ) ad + (* Use original access state instead of current with removed written vars. *) + Queries.AD.iter (check_mval octx.local) ad end; ctx.local | Access {ad; kind = Write; _} -> @@ -102,9 +103,7 @@ struct ctx.local | ad -> Queries.AD.fold (fun addr vs -> - match addr with - | Queries.AD.Addr.Addr (v,o) -> rem_mval vs (v, ValueDomain.Offs.to_exp o) (* TODO: use unconverted addrs in domain? *) - | _ -> vs + rem_mval vs addr ) ad ctx.local end | _ -> ctx.local diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml index d053cd103b..feb9599977 100644 --- a/src/analyses/taintPartialContexts.ml +++ b/src/analyses/taintPartialContexts.ml @@ -6,31 +6,19 @@ open GoblintCil open Analyses -module D = SetDomain.ToppedSet (Mval.Exp) (struct let topname = "All" end) - -let to_mvals ad = - (* TODO: should one handle ad with unknown pointers separately like in (all) other analyses? *) - Queries.AD.fold (fun addr mvals -> - match addr with - | Queries.AD.Addr.Addr (v,o) -> D.add (v, ValueDomain.Offs.to_exp o) mvals (* TODO: use unconverted addrs in domain? *) - | _ -> mvals - ) ad (D.empty ()) +module AD = ValueDomain.AD module Spec = struct include Analyses.IdentitySpec let name () = "taintPartialContexts" - module D = D + module D = AD module C = Lattice.Unit (* Add Lval or any Lval which it may point to to the set *) let taint_lval ctx (lval:lval) : D.t = - let d = ctx.local in - (match lval with - | (Var v, offs) -> D.add (v, Offset.Exp.of_cil offs) d - | (Mem e, _) -> D.union (to_mvals (ctx.ask (Queries.MayPointTo e))) d - ) + D.union (ctx.ask (Queries.MayPointTo (AddrOf lval))) ctx.local (* this analysis is context insensitive*) let context _ _ = () @@ -45,14 +33,12 @@ struct let d_return = if D.is_top d then d - else ( + else let locals = f.sformals @ f.slocals in - D.filter (fun (v, _) -> - not (List.exists (fun local -> - CilType.Varinfo.equal v local && not (ctx.ask (Queries.IsMultiple local)) - ) locals) + D.filter (function + | AD.Addr.Addr (v,_) -> not (List.exists (fun local -> CilType.Varinfo.equal v local && not (ctx.ask (Queries.IsMultiple local))) locals) + | _ -> false ) d - ) in if M.tracing then M.trace "taintPC" "returning from %s: tainted vars: %a\n without locals: %a\n" f.svar.vname D.pretty d D.pretty d_return; d_return @@ -94,9 +80,10 @@ struct else deep_addrs in - let d = List.fold_left (fun accD addr -> D.union accD (to_mvals (ctx.ask (Queries.MayPointTo addr)))) d shallow_addrs + (* TODO: should one handle ad with unknown pointers separately like in (all) other analyses? *) + let d = List.fold_left (fun accD addr -> D.union accD (ctx.ask (Queries.MayPointTo addr))) d shallow_addrs in - let d = List.fold_left (fun accD addr -> D.union accD (to_mvals (ctx.ask (Queries.ReachableFrom addr)))) d deep_addrs + let d = List.fold_left (fun accD addr -> D.union accD (ctx.ask (Queries.ReachableFrom addr))) d deep_addrs in d @@ -111,7 +98,7 @@ struct let query ctx (type a) (q: a Queries.t) : a Queries.result = match q with - | MayBeTainted -> (ctx.local : Queries.LS.t) + | MayBeTainted -> (ctx.local : Queries.AD.t) | _ -> Queries.Result.top q end @@ -122,5 +109,8 @@ let _ = module VS = SetDomain.ToppedSet(Basetype.Variables) (struct let topname = "All" end) (* Convert Lval set to (less precise) Varinfo set. *) -let conv_varset (lval_set : Spec.D.t) : VS.t = - if Spec.D.is_top lval_set then VS.top () else VS.of_list (List.map (fun (v, _) -> v) (Spec.D.elements lval_set)) +let conv_varset (addr_set : Spec.D.t) : VS.t = + if Spec.D.is_top addr_set then + VS.top () + else + VS.of_list (Spec.D.to_var_may addr_set) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 0aafbd1ad4..02231336c0 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -4,8 +4,13 @@ open GoblintCil open Analyses open MessageCategory -module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end) -module ThreadIdSet = SetDomain.Make(ThreadIdDomain.ThreadLifted) +module AllocaVars = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All alloca() Variables" end) +module HeapVars = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end) + +(* Heap vars created by alloca() and deallocated at function exit * Heap vars deallocated by free() *) +module StackAndHeapVars = Lattice.Prod(AllocaVars)(HeapVars) + +module ThreadIdToJoinedThreadsMap = MapDomain.MapBot(ThreadIdDomain.ThreadLifted)(ConcDomain.MustThreadSet) module Spec : Analyses.MCPSpec = struct @@ -13,9 +18,9 @@ struct let name () = "useAfterFree" - module D = ToppedVarInfoSet + module D = StackAndHeapVars module C = Lattice.Unit - module G = ThreadIdSet + module G = ThreadIdToJoinedThreadsMap module V = VarinfoV (** TODO: Try out later in benchmarks to see how we perform with and without context-sensititivty *) @@ -24,83 +29,110 @@ struct (* HELPER FUNCTIONS *) + let set_global_svcomp_var is_double_free = + if is_double_free then + AnalysisState.svcomp_may_invalid_free := true + else + AnalysisState.svcomp_may_invalid_deref := true + let get_current_threadid ctx = ctx.ask Queries.CurrentThreadId - let warn_for_multi_threaded_access ctx (heap_var:varinfo) behavior cwe_number = + let get_joined_threads ctx = + ctx.ask Queries.MustJoinedThreads + + let warn_for_multi_threaded_access ctx ?(is_double_free = false) (heap_var:varinfo) behavior cwe_number = let freeing_threads = ctx.global heap_var in (* If we're single-threaded or there are no threads freeing the memory, we have nothing to WARN about *) - if ctx.ask (Queries.MustBeSingleThreaded { since_start = true }) || ThreadIdSet.is_empty freeing_threads then () + if ctx.ask (Queries.MustBeSingleThreaded { since_start = true }) || G.is_empty freeing_threads then () else begin - let possibly_started current = function + let possibly_started current tid joined_threads = + match tid with | `Lifted tid -> - let threads = ctx.ask Queries.CreatedThreads in - let not_started = MHP.definitely_not_started (current, threads) tid in + let created_threads = ctx.ask Queries.CreatedThreads in + let not_started = MHP.definitely_not_started (current, created_threads) tid in let possibly_started = not not_started in - possibly_started + (* If [current] is possibly running together with [tid], but is also joined before the free() in [tid], then no need to WARN *) + let current_joined_before_free = ConcDomain.MustThreadSet.mem current joined_threads in + possibly_started && not current_joined_before_free | `Top -> true | `Bot -> false in - let equal_current current = function + let equal_current current tid joined_threads = + match tid with | `Lifted tid -> ThreadId.Thread.equal current tid | `Top -> true | `Bot -> false in + let bug_name = if is_double_free then "Double Free" else "Use After Free" in match get_current_threadid ctx with | `Lifted current -> - let possibly_started = ThreadIdSet.exists (possibly_started current) freeing_threads in - if possibly_started then - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "There's a thread that's been started in parallel with the memory-freeing threads for heap variable %a. Use-After-Free might occur" CilType.Varinfo.pretty heap_var + let possibly_started = G.exists (possibly_started current) freeing_threads in + if possibly_started then begin + set_global_svcomp_var is_double_free; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "There's a thread that's been started in parallel with the memory-freeing threads for heap variable %a. %s might occur" CilType.Varinfo.pretty heap_var bug_name + end else begin let current_is_unique = ThreadId.Thread.is_unique current in - let any_equal_current threads = ThreadIdSet.exists (equal_current current) threads in - if not current_is_unique && any_equal_current freeing_threads then - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Current thread is not unique and a Use-After-Free might occur for heap variable %a" CilType.Varinfo.pretty heap_var - else if D.mem heap_var ctx.local then - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Use-After-Free might occur in current unique thread %a for heap variable %a" ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var + let any_equal_current threads = G.exists (equal_current current) threads in + if not current_is_unique && any_equal_current freeing_threads then begin + set_global_svcomp_var is_double_free; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Current thread is not unique and a %s might occur for heap variable %a" bug_name CilType.Varinfo.pretty heap_var + end + else if HeapVars.mem heap_var (snd ctx.local) then begin + set_global_svcomp_var is_double_free; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "%s might occur in current unique thread %a for heap variable %a" bug_name ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var + end end | `Top -> - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "CurrentThreadId is top. A Use-After-Free might occur for heap variable %a" CilType.Varinfo.pretty heap_var + set_global_svcomp_var is_double_free; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "CurrentThreadId is top. %s might occur for heap variable %a" bug_name CilType.Varinfo.pretty heap_var | `Bot -> M.warn ~category:MessageCategory.Analyzer "CurrentThreadId is bottom" end - let rec warn_lval_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (lval:lval) = - let state = ctx.local in - let undefined_behavior = if is_double_free then Undefined DoubleFree else Undefined UseAfterFree in - let cwe_number = if is_double_free then 415 else 416 in - let rec offset_might_contain_freed offset = - match offset with - | NoOffset -> () - | Field (f, o) -> offset_might_contain_freed o - | Index (e, o) -> warn_exp_might_contain_freed transfer_fn_name ctx e; offset_might_contain_freed o - in - let (lval_host, o) = lval in offset_might_contain_freed o; (* Check the lval's offset *) - let lval_to_query = - match lval_host with - | Var _ -> Lval lval - | Mem _ -> mkAddrOf lval (* Take the lval's address if its lhost is of the form *p, where p is a ptr *) - in - match ctx.ask (Queries.MayPointTo lval_to_query) with - | ad when not (Queries.AD.is_top ad) -> - let warn_for_heap_var v = - if D.mem v state then - M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name + let rec warn_lval_might_contain_freed ?(is_implicitly_derefed = false) ?(is_double_free = false) (transfer_fn_name:string) ctx (lval:lval) = + match is_implicitly_derefed, is_double_free, lval with + (* If we're not checking for a double-free and there's no deref happening, then there's no need to check for an invalid deref or an invalid free *) + | false, false, (Var _, NoOffset) -> () + | _ -> + let state = ctx.local in + let undefined_behavior = if is_double_free then Undefined DoubleFree else Undefined UseAfterFree in + let cwe_number = if is_double_free then 415 else 416 in + let rec offset_might_contain_freed offset = + match offset with + | NoOffset -> () + | Field (f, o) -> offset_might_contain_freed o + | Index (e, o) -> warn_exp_might_contain_freed transfer_fn_name ctx e; offset_might_contain_freed o in - let pointed_to_heap_vars = - Queries.AD.fold (fun addr vars -> - match addr with - | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsHeapVar v) -> v :: vars - | _ -> vars - ) ad [] + let (lval_host, o) = lval in offset_might_contain_freed o; (* Check the lval's offset *) + let lval_to_query = + match lval_host with + | Var _ -> Lval lval + | Mem _ -> mkAddrOf lval (* Take the lval's address if its lhost is of the form *p, where p is a ptr *) in - List.iter warn_for_heap_var pointed_to_heap_vars; (* Warn for all heap vars that the lval possibly points to *) - (* Warn for a potential multi-threaded UAF for all heap vars that the lval possibly points to *) - List.iter (fun heap_var -> warn_for_multi_threaded_access ctx heap_var undefined_behavior cwe_number) pointed_to_heap_vars - | _ -> () + begin match ctx.ask (Queries.MayPointTo lval_to_query) with + | ad when not (Queries.AD.is_top ad) -> + let warn_for_heap_var v = + if HeapVars.mem v (snd state) then + M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name + in + let pointed_to_heap_vars = + Queries.AD.fold (fun addr vars -> + match addr with + | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) -> v :: vars + | _ -> vars + ) ad [] + in + (* Warn for all heap vars that the lval possibly points to *) + List.iter warn_for_heap_var pointed_to_heap_vars; + (* Warn for a potential multi-threaded UAF for all heap vars that the lval possibly points to *) + List.iter (fun heap_var -> warn_for_multi_threaded_access ctx ~is_double_free heap_var undefined_behavior cwe_number) pointed_to_heap_vars + | _ -> () + end - and warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (exp:exp) = + and warn_exp_might_contain_freed ?(is_implicitly_derefed = false) ?(is_double_free = false) (transfer_fn_name:string) ctx (exp:exp) = match exp with (* Base recursion cases *) | Const _ @@ -114,22 +146,26 @@ struct | SizeOfE e | AlignOfE e | UnOp (_, e, _) - | CastE (_, e) -> warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e + | CastE (_, e) -> warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e | BinOp (_, e1, e2, _) -> - warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e1; - warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e2 + warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e1; + warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e2 | Question (e1, e2, e3, _) -> - warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e1; - warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e2; - warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e3 + warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e1; + warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e2; + warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e3 (* Lval cases (need [warn_lval_might_contain_freed] for them) *) | Lval lval | StartOf lval - | AddrOf lval -> warn_lval_might_contain_freed ~is_double_free transfer_fn_name ctx lval + | AddrOf lval -> warn_lval_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx lval - let side_effect_mem_free ctx freed_heap_vars threadid = - let threadid = G.singleton threadid in - D.iter (fun var -> ctx.sideg var threadid) freed_heap_vars + let side_effect_mem_free ctx freed_heap_vars threadid joined_threads = + let side_effect_globals_to_heap_var heap_var = + let current_globals = ctx.global heap_var in + let globals_to_side_effect = G.add threadid joined_threads current_globals in + ctx.sideg heap_var globals_to_side_effect + in + HeapVars.iter side_effect_globals_to_heap_var freed_heap_vars (* TRANSFER FUNCTIONS *) @@ -153,7 +189,7 @@ struct let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = let caller_state = ctx.local in List.iter (fun arg -> warn_exp_might_contain_freed "enter" ctx arg) args; - if D.is_empty caller_state then + if AllocaVars.is_empty (fst caller_state) && HeapVars.is_empty (snd caller_state) then [caller_state, caller_state] else ( let reachable_from_args = List.fold_left (fun ad arg -> Queries.AD.join ad (ctx.ask (ReachableFrom arg))) (Queries.AD.empty ()) args in @@ -161,13 +197,18 @@ struct [caller_state, caller_state] else let reachable_vars = Queries.AD.to_var_may reachable_from_args in - let callee_state = D.filter (fun var -> List.mem var reachable_vars) caller_state in (* TODO: use AD.mem directly *) + let callee_state = (AllocaVars.empty (), HeapVars.filter (fun var -> List.mem var reachable_vars) (snd caller_state)) in (* TODO: use AD.mem directly *) [caller_state, callee_state] ) let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t = - let caller_state = ctx.local in - D.join caller_state callee_local + let (caller_stack_state, caller_heap_state) = ctx.local in + let callee_stack_state = fst callee_local in + let callee_heap_state = snd callee_local in + (* Put all alloca()-vars together with all freed() vars in the caller's second component *) + (* Don't change caller's first component => caller hasn't exited yet *) + let callee_combined_state = HeapVars.join callee_stack_state callee_heap_state in + (caller_stack_state, HeapVars.join caller_heap_state callee_combined_state) let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t = Option.iter (fun x -> warn_lval_might_contain_freed "enter" ctx x) lval; @@ -175,9 +216,16 @@ struct let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = let state = ctx.local in - Option.iter (fun x -> warn_lval_might_contain_freed ("special: " ^ f.vname) ctx x) lval; - List.iter (fun arg -> warn_exp_might_contain_freed ~is_double_free:(f.vname = "free") ("special: " ^ f.vname) ctx arg) arglist; let desc = LibraryFunctions.find f in + let is_arg_implicitly_derefed arg = + let read_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = false } arglist in + let read_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = true } arglist in + let write_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } arglist in + let write_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } arglist in + List.mem arg read_shallow_args || List.mem arg read_deep_args || List.mem arg write_shallow_args || List.mem arg write_deep_args + in + Option.iter (fun x -> warn_lval_might_contain_freed ("special: " ^ f.vname) ctx x) lval; + List.iter (fun arg -> warn_exp_might_contain_freed ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) ~is_double_free:(match desc.special arglist with Free _ -> true | _ -> false) ("special: " ^ f.vname) ctx arg) arglist; match desc.special arglist with | Free ptr -> begin match ctx.ask (Queries.MayPointTo ptr) with @@ -185,13 +233,20 @@ struct let pointed_to_heap_vars = Queries.AD.fold (fun addr state -> match addr with - | Queries.AD.Addr.Addr (var,_) when ctx.ask (Queries.IsHeapVar var) -> D.add var state + | Queries.AD.Addr.Addr (var,_) when ctx.ask (Queries.IsAllocVar var) && ctx.ask (Queries.IsHeapVar var) -> HeapVars.add var state | _ -> state - ) ad (D.empty ()) + ) ad (HeapVars.empty ()) in (* Side-effect the tid that's freeing all the heap vars collected here *) - side_effect_mem_free ctx pointed_to_heap_vars (get_current_threadid ctx); - D.join state (pointed_to_heap_vars) (* Add all heap vars, which ptr points to, to the state *) + side_effect_mem_free ctx pointed_to_heap_vars (get_current_threadid ctx) (get_joined_threads ctx); + (* Add all heap vars, which ptr points to, to the state *) + (fst state, HeapVars.join (snd state) pointed_to_heap_vars) + | _ -> state + end + | Alloca _ -> + (* Create fresh heap var for the alloca() call *) + begin match ctx.ask (Queries.AllocVar {on_stack = true}) with + | `Lifted v -> (AllocaVars.add v (fst state), snd state) | _ -> state end | _ -> state diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 634a684c7c..dcd49c9f02 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -437,10 +437,14 @@ struct let d_local = (* if we are multithreaded, we run the risk, that some mutex protected variables got unlocked, so in this case caller state goes to top TODO: !!Unsound, this analysis does not handle this case -> regtest 63 08!! *) - if Queries.LS.is_top tainted || not (ctx.ask (Queries.MustBeSingleThreaded {since_start = true})) then + if Queries.AD.is_top tainted || not (ctx.ask (Queries.MustBeSingleThreaded {since_start = true})) then D.top () else - let taint_exp = Queries.ES.of_list (List.map Mval.Exp.to_cil_exp (Queries.LS.elements tainted)) in + let taint_exp = + Queries.AD.to_mval tainted + |> List.map Addr.Mval.to_cil_exp + |> Queries.ES.of_list + in D.filter (fun exp -> not (Queries.ES.mem exp taint_exp)) ctx.local in let d = D.meet au d_local in diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml index d9bbdb6197..5c0176df48 100644 --- a/src/analyses/wrapperFunctionAnalysis.ml +++ b/src/analyses/wrapperFunctionAnalysis.ml @@ -133,7 +133,7 @@ module MallocWrapper : MCPSpec = struct let query (ctx: (D.t, G.t, C.t, V.t) ctx) (type a) (q: a Q.t): a Q.result = let wrapper_node, counter = ctx.local in match q with - | Q.HeapVar -> + | Q.AllocVar {on_stack = on_stack} -> let node = match wrapper_node with | `Lifted wrapper_node -> wrapper_node | _ -> node_for_ctx ctx @@ -141,8 +141,11 @@ module MallocWrapper : MCPSpec = struct let count = UniqueCallCounter.find (`Lifted node) counter in let var = NodeVarinfoMap.to_varinfo (ctx.ask Q.CurrentThreadId, node, count) in var.vdecl <- UpdateCil.getLoc node; (* TODO: does this do anything bad for incremental? *) + if on_stack then var.vattr <- addAttribute (Attr ("stack_alloca", [])) var.vattr; (* If the call was for stack allocation, add an attr to mark the heap var *) `Lifted var | Q.IsHeapVar v -> + NodeVarinfoMap.mem_varinfo v && not @@ hasAttribute "stack_alloca" v.vattr + | Q.IsAllocVar v -> NodeVarinfoMap.mem_varinfo v | Q.IsMultiple v -> begin match NodeVarinfoMap.from_varinfo v with diff --git a/src/autoTune.ml b/src/autoTune.ml index a267c3bf9b..d532081799 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -219,6 +219,13 @@ let focusOnSpecification () = | NoOverflow -> (*We focus on integer analysis*) set_bool "ana.int.def_exc" true; set_bool "ana.int.interval" true + | ValidFree -> (* Enable the useAfterFree analysis *) + let uafAna = ["useAfterFree"] in + print_endline @@ "Specification: ValidFree -> enabling useAfterFree analysis \"" ^ (String.concat ", " uafAna) ^ "\""; + enableAnalyses uafAna + (* TODO: Finish these two below later *) + | ValidDeref + | ValidMemtrack -> () (*Detect enumerations and enable the "ana.int.enums" option*) exception EnumFound diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml index 0de5afc32c..4bc97b34ab 100644 --- a/src/cdomains/lockDomain.ml +++ b/src/cdomains/lockDomain.ml @@ -7,7 +7,7 @@ module IdxDom = ValueDomain.IndexDomain open GoblintCil -module Mutexes = SetDomain.ToppedSet (Addr) (struct let topname = "All mutexes" end) (* TODO HoareDomain? *) +module Mutexes = SetDomain.ToppedSet (Addr) (struct let topname = "All mutexes" end) (* TODO: AD? *) module Simple = Lattice.Reverse (Mutexes) module Priorities = IntDomain.Lifted diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index aa52770475..b6fbfaf7dc 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -865,6 +865,8 @@ struct (* Funny, this does not compile without the final type annotation! *) let rec eval_offset (ask: VDQ.t) f (x: t) (offs:offs) (exp:exp option) (v:lval option) (t:typ): t = let rec do_eval_offset (ask:VDQ.t) f (x:t) (offs:offs) (exp:exp option) (l:lval option) (o:offset option) (v:lval option) (t:typ): t = + if M.tracing then M.traceli "eval_offset" "do_eval_offset %a %a (%a)\n" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp; + let r = match x, offs with | Blob((va, _, orig) as c), `Index (_, ox) -> begin @@ -927,6 +929,9 @@ struct | Top -> M.info ~category:Imprecise "Trying to read an index, but the array is unknown"; top () | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read an index, but was not given an array (%a)" pretty x; top () end + in + if M.tracing then M.traceu "eval_offset" "do_eval_offset -> %a\n" pretty r; + r in let l, o = match exp with | Some(Lval (x,o)) -> Some ((x, NoOffset)), Some(o) diff --git a/src/domains/access.ml b/src/domains/access.ml index fa6446df16..8907ccbc32 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -10,28 +10,105 @@ module M = Messages (* Some helper functions to avoid flagging race warnings on atomic types, and * other irrelevant stuff, such as mutexes and functions. *) -let is_ignorable_type (t: typ): bool = - match t with - | TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "pthread_rwlock_t" | "pthread_spinlock_t" | "spinlock_t" | "pthread_cond_t"; _ }, _) -> true - | TComp ({ cname = "__pthread_mutex_s" | "__pthread_rwlock_arch_t" | "__jmp_buf_tag" | "_pthread_cleanup_buffer" | "__pthread_cleanup_frame" | "__cancel_jmp_buf_tag"; _}, _) -> true - | TComp ({ cname; _}, _) when String.starts_with_stdlib ~prefix:"__anon" cname -> +let is_ignorable_comp_name = function + | "__pthread_mutex_s" | "__pthread_rwlock_arch_t" | "__jmp_buf_tag" | "_pthread_cleanup_buffer" | "__pthread_cleanup_frame" | "__cancel_jmp_buf_tag" | "_IO_FILE" -> true + | cname when String.starts_with_stdlib ~prefix:"__anon" cname -> begin match Cilfacade.split_anoncomp_name cname with | (true, Some ("__once_flag" | "__pthread_unwind_buf_t" | "__cancel_jmp_buf"), _) -> true (* anonstruct *) | (false, Some ("pthread_mutexattr_t" | "pthread_condattr_t" | "pthread_barrierattr_t"), _) -> true (* anonunion *) | _ -> false end - | TComp ({ cname = "lock_class_key"; _ }, _) -> true - | TInt (IInt, attr) when hasAttribute "mutex" attr -> true - | t when hasAttribute "atomic" (typeAttrs t) -> true (* C11 _Atomic *) + | "lock_class_key" -> true (* kernel? *) | _ -> false -let is_ignorable = function - | None -> false - | Some (v,os) when hasAttribute "thread" v.vattr && not (v.vaddrof) -> true (* Thread-Local Storage *) - | Some (v,os) when BaseUtil.is_volatile v && not (get_bool "ana.race.volatile") -> true (* volatile & races on volatiles should not be reported *) - | Some (v,os) -> - try isFunctionType v.vtype || is_ignorable_type v.vtype - with Not_found -> false +let is_ignorable_attrs attrs = + let is_ignorable_attr = function + | Attr ("volatile", _) when not (get_bool "ana.race.volatile") -> true (* volatile & races on volatiles should not be reported *) + | Attr ("atomic", _) -> true (* C11 _Atomic *) + | _ -> false + in + List.exists is_ignorable_attr attrs + +let rec is_ignorable_type (t: typ): bool = + (* efficient pattern matching first *) + match t with + | TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "pthread_rwlock_t" | "pthread_spinlock_t" | "spinlock_t" | "pthread_cond_t" | "atomic_flag" | "FILE" | "__FILE"; _ }, _) -> true + | TComp ({ cname; _}, _) when is_ignorable_comp_name cname -> true + | TInt (IInt, attr) when hasAttribute "mutex" attr -> true (* kernel? *) + | TFun _ -> true + | _ -> + if is_ignorable_attrs (typeAttrsOuter t) then (* only outer because we unroll TNamed ourselves *) + true + else ( + (* unroll TNamed once *) + (* can't use unrollType because we want to check TNamed-s at all intermediate typedefs as well *) + match t with + | TNamed ({ttype; _}, attrs) -> is_ignorable_type (typeAddAttributes attrs ttype) + | _ -> false + ) + +let rec is_ignorable_type_offset (t: typ) (o: _ Offset.t): bool = + (* similar to Cilfacade.typeOffset but we want to check types at all intermediate offsets as well *) + if is_ignorable_type t then + true (* type at offset so far ignorable, no need to recurse *) + else ( + match o with + | `NoOffset -> false (* already checked t *) + | `Index (_, o') -> + begin match unrollType t with + | TArray (et, _, attrs) -> + let t' = Cilfacade.typeBlendAttributes attrs et in + is_ignorable_type_offset t' o' + | _ -> false (* index on non-array *) + end + | `Field (f, o') -> + begin match unrollType t with + | TComp (_, attrs) -> + let t' = Cilfacade.typeBlendAttributes attrs f.ftype in + is_ignorable_type_offset t' o' + | _ -> false (* field on non-compound *) + end + ) + +(** {!is_ignorable_type} for {!typsig}. *) +let is_ignorable_typsig (ts: typsig): bool = + (* efficient pattern matching first *) + match ts with + | TSComp (_, cname, _) when is_ignorable_comp_name cname -> true + | TSFun _ -> true + | TSBase t -> is_ignorable_type t + | _ -> is_ignorable_attrs (typeSigAttrs ts) + +(** {!is_ignorable_type_offset} for {!typsig}. *) +let rec is_ignorable_typsig_offset (ts: typsig) (o: _ Offset.t): bool = + if is_ignorable_typsig ts then + true (* type at offset so far ignorable, no need to recurse *) + else ( + match o with + | `NoOffset -> false (* already checked t *) + | `Index (_, o') -> + begin match ts with + | TSArray (ets, _, attrs) -> + let ts' = Cilfacade.typeSigBlendAttributes attrs ets in + is_ignorable_typsig_offset ts' o' + | _ -> false (* index on non-array *) + end + | `Field (f, o') -> + begin match ts with + | TSComp (_, _, attrs) -> + let t' = Cilfacade.typeBlendAttributes attrs f.ftype in + is_ignorable_type_offset t' o' (* switch to type because it is more precise with TNamed *) + | _ -> false (* field on non-compound *) + end + ) + +let is_ignorable_mval = function + | ({vaddrof = false; vattr; _}, _) when hasAttribute "thread" vattr -> true (* Thread-Local Storage *) + | (v, o) -> is_ignorable_type_offset v.vtype o (* can't use Cilfacade.typeOffset because we want to check types at all intermediate offsets as well *) + +let is_ignorable_memo = function + | (`Type ts, o) -> is_ignorable_typsig_offset ts o + | (`Var v, o) -> is_ignorable_mval (v, o) module TSH = Hashtbl.Make (CilType.Typsig) @@ -195,8 +272,7 @@ let get_val_type e: acc_typ = (** Add access to {!Memo} after distributing. *) let add_one ~side memo: unit = - let mv = Memo.to_mval memo in - let ignorable = is_ignorable mv in + let ignorable = is_ignorable_memo memo in if M.tracing then M.trace "access" "add_one %a (ignorable = %B)\n" Memo.pretty memo ignorable; if not ignorable then side memo diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 0388ce2995..c706339bf2 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -80,26 +80,31 @@ type _ t = | MayBePublic: maybepublic -> MayBool.t t (* old behavior with write=false *) | MayBePublicWithout: maybepublicwithout -> MayBool.t t | MustBeProtectedBy: mustbeprotectedby -> MustBool.t t - | MustLockset: LS.t t + | MustLockset: AD.t t | MustBeAtomic: MustBool.t t | MustBeSingleThreaded: {since_start: bool} -> MustBool.t t | MustBeUniqueThread: MustBool.t t | CurrentThreadId: ThreadIdDomain.ThreadLifted.t t | ThreadCreateIndexedNode: ThreadNodeLattice.t t | MayBeThreadReturn: MayBool.t t - | EvalFunvar: exp -> LS.t t + | EvalFunvar: exp -> AD.t t | EvalInt: exp -> ID.t t | EvalStr: exp -> SD.t t | EvalLength: exp -> ID.t t (* length of an array or string *) | EvalValue: exp -> VD.t t - | BlobSize: exp -> ID.t t (* size of a dynamically allocated `Blob pointed to by exp *) + | BlobSize: {exp: Cil.exp; base_address: bool} -> ID.t t + (* Size of a dynamically allocated `Blob pointed to by exp. *) + (* If the record's second field is set to true, then address offsets are discarded and the size of the `Blob is asked for the base address. *) | CondVars: exp -> ES.t t | PartAccess: access -> Obj.t t (** Only queried by access and deadlock analysis. [Obj.t] represents [MCPAccess.A.t], needed to break dependency cycle. *) | IterPrevVars: iterprevvar -> Unit.t t | IterVars: itervar -> Unit.t t | PathQuery: int * 'a t -> 'a t (** Query only one path under witness lifter. *) | DYojson: FlatYojson.t t (** Get local state Yojson of one path under [PathQuery]. *) - | HeapVar: VI.t t + | AllocVar: {on_stack: bool} -> VI.t t + (* Create a variable representing a dynamic allocation-site *) + (* If on_stack is [true], then the dynamic allocation is on the stack (i.e., alloca() or a similar function was called). Otherwise, allocation is on the heap *) + | IsAllocVar: varinfo -> MayBool.t t (* [true] if variable represents dynamically allocated memory *) | IsHeapVar: varinfo -> MayBool.t t (* TODO: is may or must? *) | IsMultiple: varinfo -> MustBool.t t (* For locals: Is another copy of this local variable reachable via pointers? *) @@ -114,13 +119,13 @@ type _ t = | CreatedThreads: ConcDomain.ThreadSet.t t | MustJoinedThreads: ConcDomain.MustThreadSet.t t | ThreadsJoinedCleanly: MustBool.t t - | MustProtectedVars: mustprotectedvars -> LS.t t + | MustProtectedVars: mustprotectedvars -> VS.t t | Invariant: invariant_context -> Invariant.t t | InvariantGlobal: Obj.t -> Invariant.t t (** Argument must be of corresponding [Spec.V.t]. *) | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *) | IterSysVars: VarQuery.t * Obj.t VarQuery.f -> Unit.t t (** [iter_vars] for [Constraints.FromSpec]. [Obj.t] represents [Spec.V.t]. *) | MayAccessed: AccessDomain.EventSet.t t - | MayBeTainted: LS.t t + | MayBeTainted: AD.t t | MayBeModifiedSinceSetjmp: JmpBufDomain.BufferEntry.t -> VS.t t | TmpSpecial: Mval.Exp.t -> ML.t t @@ -144,14 +149,15 @@ struct | MayPointTo _ -> (module AD) | ReachableFrom _ -> (module AD) | Regions _ -> (module LS) - | MustLockset -> (module LS) - | EvalFunvar _ -> (module LS) + | MustLockset -> (module AD) + | EvalFunvar _ -> (module AD) | ReachableUkTypes _ -> (module TS) | MayEscape _ -> (module MayBool) | MayBePublic _ -> (module MayBool) | MayBePublicWithout _ -> (module MayBool) | MayBeThreadReturn -> (module MayBool) | IsHeapVar _ -> (module MayBool) + | IsAllocVar _ -> (module MayBool) | MustBeProtectedBy _ -> (module MustBool) | MustBeAtomic -> (module MustBool) | MustBeSingleThreaded _ -> (module MustBool) @@ -163,7 +169,7 @@ struct | BlobSize _ -> (module ID) | CurrentThreadId -> (module ThreadIdDomain.ThreadLifted) | ThreadCreateIndexedNode -> (module ThreadNodeLattice) - | HeapVar -> (module VI) + | AllocVar _ -> (module VI) | EvalStr _ -> (module SD) | IterPrevVars _ -> (module Unit) | IterVars _ -> (module Unit) @@ -179,13 +185,13 @@ struct | CreatedThreads -> (module ConcDomain.ThreadSet) | MustJoinedThreads -> (module ConcDomain.MustThreadSet) | ThreadsJoinedCleanly -> (module MustBool) - | MustProtectedVars _ -> (module LS) + | MustProtectedVars _ -> (module VS) | Invariant _ -> (module Invariant) | InvariantGlobal _ -> (module Invariant) | WarnGlobal _ -> (module Unit) | IterSysVars _ -> (module Unit) | MayAccessed -> (module AccessDomain.EventSet) - | MayBeTainted -> (module LS) + | MayBeTainted -> (module AD) | MayBeModifiedSinceSetjmp _ -> (module VS) | TmpSpecial _ -> (module ML) @@ -208,14 +214,15 @@ struct | MayPointTo _ -> AD.top () | ReachableFrom _ -> AD.top () | Regions _ -> LS.top () - | MustLockset -> LS.top () - | EvalFunvar _ -> LS.top () + | MustLockset -> AD.top () + | EvalFunvar _ -> AD.top () | ReachableUkTypes _ -> TS.top () | MayEscape _ -> MayBool.top () | MayBePublic _ -> MayBool.top () | MayBePublicWithout _ -> MayBool.top () | MayBeThreadReturn -> MayBool.top () | IsHeapVar _ -> MayBool.top () + | IsAllocVar _ -> MayBool.top () | MutexType _ -> MutexAttrDomain.top () | MustBeProtectedBy _ -> MustBool.top () | MustBeAtomic -> MustBool.top () @@ -228,7 +235,7 @@ struct | BlobSize _ -> ID.top () | CurrentThreadId -> ThreadIdDomain.ThreadLifted.top () | ThreadCreateIndexedNode -> ThreadNodeLattice.top () - | HeapVar -> VI.top () + | AllocVar _ -> VI.top () | EvalStr _ -> SD.top () | IterPrevVars _ -> Unit.top () | IterVars _ -> Unit.top () @@ -243,13 +250,13 @@ struct | CreatedThreads -> ConcDomain.ThreadSet.top () | MustJoinedThreads -> ConcDomain.MustThreadSet.top () | ThreadsJoinedCleanly -> MustBool.top () - | MustProtectedVars _ -> LS.top () + | MustProtectedVars _ -> VS.top () | Invariant _ -> Invariant.top () | InvariantGlobal _ -> Invariant.top () | WarnGlobal _ -> Unit.top () | IterSysVars _ -> Unit.top () | MayAccessed -> AccessDomain.EventSet.top () - | MayBeTainted -> LS.top () + | MayBeTainted -> AD.top () | MayBeModifiedSinceSetjmp _ -> VS.top () | TmpSpecial _ -> ML.top () end @@ -288,7 +295,7 @@ struct | Any (PartAccess _) -> 23 | Any (IterPrevVars _) -> 24 | Any (IterVars _) -> 25 - | Any HeapVar -> 29 + | Any (AllocVar _) -> 29 | Any (IsHeapVar _) -> 30 | Any (IsMultiple _) -> 31 | Any (EvalThread _) -> 32 @@ -313,6 +320,7 @@ struct | Any ThreadCreateIndexedNode -> 51 | Any ThreadsJoinedCleanly -> 52 | Any (TmpSpecial _) -> 53 + | Any (IsAllocVar _) -> 54 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -335,7 +343,12 @@ struct | Any (EvalLength e1), Any (EvalLength e2) -> CilType.Exp.compare e1 e2 | Any (EvalMutexAttr e1), Any (EvalMutexAttr e2) -> CilType.Exp.compare e1 e2 | Any (EvalValue e1), Any (EvalValue e2) -> CilType.Exp.compare e1 e2 - | Any (BlobSize e1), Any (BlobSize e2) -> CilType.Exp.compare e1 e2 + | Any (BlobSize {exp = e1; base_address = b1}), Any (BlobSize {exp = e2; base_address = b2}) -> + let r = CilType.Exp.compare e1 e2 in + if r <> 0 then + r + else + Stdlib.compare b1 b2 | Any (CondVars e1), Any (CondVars e2) -> CilType.Exp.compare e1 e2 | Any (PartAccess p1), Any (PartAccess p2) -> compare_access p1 p2 | Any (IterPrevVars ip1), Any (IterPrevVars ip2) -> compare_iterprevvar ip1 ip2 @@ -347,6 +360,7 @@ struct else compare (Any q1) (Any q2) | Any (IsHeapVar v1), Any (IsHeapVar v2) -> CilType.Varinfo.compare v1 v2 + | Any (IsAllocVar v1), Any (IsAllocVar v2) -> CilType.Varinfo.compare v1 v2 | Any (IsMultiple v1), Any (IsMultiple v2) -> CilType.Varinfo.compare v1 v2 | Any (EvalThread e1), Any (EvalThread e2) -> CilType.Exp.compare e1 e2 | Any (EvalJumpBuf e1), Any (EvalJumpBuf e2) -> CilType.Exp.compare e1 e2 @@ -380,13 +394,14 @@ struct | Any (EvalLength e) -> CilType.Exp.hash e | Any (EvalMutexAttr e) -> CilType.Exp.hash e | Any (EvalValue e) -> CilType.Exp.hash e - | Any (BlobSize e) -> CilType.Exp.hash e + | Any (BlobSize {exp = e; base_address = b}) -> CilType.Exp.hash e + Hashtbl.hash b | Any (CondVars e) -> CilType.Exp.hash e | Any (PartAccess p) -> hash_access p | Any (IterPrevVars i) -> 0 | Any (IterVars i) -> 0 | Any (PathQuery (i, q)) -> 31 * i + hash (Any q) | Any (IsHeapVar v) -> CilType.Varinfo.hash v + | Any (IsAllocVar v) -> CilType.Varinfo.hash v | Any (IsMultiple v) -> CilType.Varinfo.hash v | Any (EvalThread e) -> CilType.Exp.hash e | Any (EvalJumpBuf e) -> CilType.Exp.hash e @@ -428,14 +443,15 @@ struct | Any (EvalStr e) -> Pretty.dprintf "EvalStr %a" CilType.Exp.pretty e | Any (EvalLength e) -> Pretty.dprintf "EvalLength %a" CilType.Exp.pretty e | Any (EvalValue e) -> Pretty.dprintf "EvalValue %a" CilType.Exp.pretty e - | Any (BlobSize e) -> Pretty.dprintf "BlobSize %a" CilType.Exp.pretty e + | Any (BlobSize {exp = e; base_address = b}) -> Pretty.dprintf "BlobSize %a (base_address: %b)" CilType.Exp.pretty e b | Any (CondVars e) -> Pretty.dprintf "CondVars %a" CilType.Exp.pretty e | Any (PartAccess p) -> Pretty.dprintf "PartAccess _" | Any (IterPrevVars i) -> Pretty.dprintf "IterPrevVars _" | Any (IterVars i) -> Pretty.dprintf "IterVars _" | Any (PathQuery (i, q)) -> Pretty.dprintf "PathQuery (%d, %a)" i pretty (Any q) - | Any HeapVar -> Pretty.dprintf "HeapVar" + | Any (AllocVar {on_stack = on_stack}) -> Pretty.dprintf "AllocVar %b" on_stack | Any (IsHeapVar v) -> Pretty.dprintf "IsHeapVar %a" CilType.Varinfo.pretty v + | Any (IsAllocVar v) -> Pretty.dprintf "IsAllocVar %a" CilType.Varinfo.pretty v | Any (IsMultiple v) -> Pretty.dprintf "IsMultiple %a" CilType.Varinfo.pretty v | Any (EvalThread e) -> Pretty.dprintf "EvalThread %a" CilType.Exp.pretty e | Any (EvalJumpBuf e) -> Pretty.dprintf "EvalJumpBuf %a" CilType.Exp.pretty e diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index df3346af93..bb2170509d 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -643,7 +643,8 @@ struct let vdecl ctx _ = ctx.local let asm x = - ignore (M.info ~category:Unsound "ASM statement ignored."); + M.msg_final Info ~category:Unsound "ASM ignored"; + M.info ~category:Unsound "ASM statement ignored."; x.local (* Just ignore. *) let skip x = x.local (* Just ignore. *) diff --git a/src/framework/analysisState.ml b/src/framework/analysisState.ml index 0f3a9f55bc..ca619d4dfb 100644 --- a/src/framework/analysisState.ml +++ b/src/framework/analysisState.ml @@ -7,6 +7,15 @@ let should_warn = ref false (** Whether signed overflow or underflow happened *) let svcomp_may_overflow = ref false +(** Whether an invalid free happened *) +let svcomp_may_invalid_free = ref false + +(** Whether an invalid pointer dereference happened *) +let svcomp_may_invalid_deref = ref false + +(** Whether an invalid memtrack happened *) +let svcomp_may_invalid_memtrack = ref false + (** A hack to see if we are currently doing global inits *) let global_initialization = ref false diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 740d1f85a9..21f3958a81 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -302,7 +302,7 @@ struct | Queries.EvalFunvar e -> let (d,l) = ctx.local in if leq0 l then - Queries.LS.empty () + Queries.AD.empty () else query' ctx (Queries.EvalFunvar e) | q -> query' ctx q @@ -754,8 +754,8 @@ struct [v] | _ -> (* Depends on base for query. *) - let ls = ctx.ask (Queries.EvalFunvar e) in - Queries.LS.fold (fun ((x,_)) xs -> x::xs) ls [] + let ad = ctx.ask (Queries.EvalFunvar e) in + Queries.AD.to_var_may ad (* TODO: don't convert, handle UnknownPtr below *) in let one_function f = match f.vtype with @@ -776,16 +776,17 @@ struct end else begin let geq = if var_arg then ">=" else "" in - M.warn ~tags:[CWE 685] "Potential call to function %a with wrong number of arguments (expected: %s%d, actual: %d). This call will be ignored." CilType.Varinfo.pretty f geq p_length arg_length; + M.warn ~category:Unsound ~tags:[Category Call; CWE 685] "Potential call to function %a with wrong number of arguments (expected: %s%d, actual: %d). This call will be ignored." CilType.Varinfo.pretty f geq p_length arg_length; None end | _ -> - M.warn ~category:Call "Something that is not a function (%a) is called." CilType.Varinfo.pretty f; + M.warn ~category:Call "Something that is not a function (%a) is called." CilType.Varinfo.pretty f; None in let funs = List.filter_map one_function functions in if [] = funs then begin - M.warn ~category:Unsound "No suitable function to be called at call site. Continuing with state before call."; + M.msg_final Warning ~category:Unsound ~tags:[Category Call] "No suitable function to call"; + M.warn ~category:Unsound ~tags:[Category Call] "No suitable function to be called at call site. Continuing with state before call."; d (* because LevelSliceLifter *) end else common_joins ctx funs !r !spawns @@ -1390,6 +1391,7 @@ struct let cilinserted = if loc.synthetic then "(possibly inserted by CIL) " else "" in M.warn ~loc:(Node g) ~tags:[CWE (if tv then 571 else 570)] ~category:Deadcode "condition '%a' %sis always %B" d_exp exp cilinserted tv | `Bot when not (CilType.Exp.equal exp one) -> (* all branches dead *) + M.msg_final Error ~category:Analyzer ~tags:[Category Unsound] "Both branches dead"; M.error ~loc:(Node g) ~category:Analyzer ~tags:[Category Unsound] "both branches over condition '%a' are dead" d_exp exp | `Bot (* all branches dead, fine at our inserted Neg(1)-s because no Pos(1) *) | `Top -> (* may be both true and false *) diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index 625e81f18b..6e700485dd 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -85,6 +85,7 @@ module MallocFresh = MallocFresh module Malloc_null = Malloc_null module MemLeak = MemLeak module UseAfterFree = UseAfterFree +module MemOutOfBounds = MemOutOfBounds (** {2 Concurrency} diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 155faa0e76..7808cbcd3f 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -410,6 +410,10 @@ let preprocess_files () = ); preprocessed +(** Regex for special "paths" in cpp output: + , , but also translations! *) +let special_path_regexp = Str.regexp "<.+>" + (** Parse preprocessed files *) let parse_preprocessed preprocessed = (* get the AST *) @@ -417,7 +421,8 @@ let parse_preprocessed preprocessed = let goblint_cwd = GobFpath.cwd () in let get_ast_and_record_deps (preprocessed_file, task_opt) = - let transform_file (path_str, system_header) = if Str.string_match (Str.regexp "<.+>") path_str 0 then + let transform_file (path_str, system_header) = + if Str.string_match special_path_regexp path_str 0 then (path_str, system_header) (* ignore special "paths" *) else let path = Fpath.v path_str in diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml index 346ce312b1..f96ca832a1 100644 --- a/src/solvers/postSolver.ml +++ b/src/solvers/postSolver.ml @@ -82,10 +82,13 @@ module Verify: F = let complain_constraint x ~lhs ~rhs = AnalysisState.verified := Some false; + M.msg_final Error ~category:Unsound "Fixpoint not reached"; ignore (Pretty.printf "Fixpoint not reached at %a\n @[Solver computed:\n%a\nRight-Hand-Side:\n%a\nDifference: %a\n@]" S.Var.pretty_trace x S.Dom.pretty lhs S.Dom.pretty rhs S.Dom.pretty_diff (rhs, lhs)) let complain_side x y ~lhs ~rhs = AnalysisState.verified := Some false; + + M.msg_final Error ~category:Unsound "Fixpoint not reached"; ignore (Pretty.printf "Fixpoint not reached at %a\nOrigin: %a\n @[Solver computed:\n%a\nSide-effect:\n%a\nDifference: %a\n@]" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty lhs S.Dom.pretty rhs S.Dom.pretty_diff (rhs, lhs)) let one_side ~vh ~x ~y ~d = diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 29ad301292..07edc632c7 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -327,7 +327,7 @@ module Base = else box old eqd in - if tracing then trace "sol" "Var: %a (wp: %b)\nOld value: %a\nNew value: %a\n" S.Var.pretty_trace x wp S.Dom.pretty old S.Dom.pretty wpd; + if tracing then trace "sol" "Var: %a (wp: %b)\nOld value: %a\nEqd: %a\nNew value: %a\n" S.Var.pretty_trace x wp S.Dom.pretty old S.Dom.pretty eqd S.Dom.pretty wpd; if cache then ( if tracing then trace "cache" "cache size %d for %a\n" (HM.length l) S.Var.pretty_trace x; cache_sizes := HM.length l :: !cache_sizes; diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml index eb7330aa19..7f6116f604 100644 --- a/src/util/cilfacade.ml +++ b/src/util/cilfacade.ml @@ -51,7 +51,8 @@ let init () = (* lineDirectiveStyle := None; *) RmUnused.keepUnused := true; print_CIL_Input := true; - Cabs2cil.allowDuplication := false + Cabs2cil.allowDuplication := false; + Cabs2cil.silenceLongDoubleWarning := true let current_file = ref dummyFile @@ -322,6 +323,15 @@ and typeOffset basetyp = | t -> raise (TypeOfError (Field_NonCompound (fi, t))) +let typeBlendAttributes baseAttrs = (* copied from Cilfacade.typeOffset *) + let (_, _, contageous) = partitionAttributes ~default:AttrName baseAttrs in + typeAddAttributes contageous + +let typeSigBlendAttributes baseAttrs = + let (_, _, contageous) = partitionAttributes ~default:AttrName baseAttrs in + typeSigAddAttrs contageous + + (** {!Cil.mkCast} using our {!typeOf}. *) let mkCast ~(e: exp) ~(newt: typ) = let oldt = diff --git a/src/util/messageCategory.ml b/src/util/messageCategory.ml index d1c8f0db3c..1bb31d6d5b 100644 --- a/src/util/messageCategory.ml +++ b/src/util/messageCategory.ml @@ -11,6 +11,7 @@ type undefined_behavior = | ArrayOutOfBounds of array_oob | NullPointerDereference | UseAfterFree + | MemoryOutOfBoundsAccess | DoubleFree | InvalidMemoryDeallocation | MemoryLeak @@ -66,6 +67,7 @@ struct let array_out_of_bounds e: category = create @@ ArrayOutOfBounds e let nullpointer_dereference: category = create @@ NullPointerDereference let use_after_free: category = create @@ UseAfterFree + let memory_out_of_bounds_access: category = create @@ MemoryOutOfBoundsAccess let double_free: category = create @@ DoubleFree let invalid_memory_deallocation: category = create @@ InvalidMemoryDeallocation let memory_leak: category = create @@ MemoryLeak @@ -105,6 +107,7 @@ struct | "array_out_of_bounds" -> ArrayOutOfBounds.from_string_list t | "nullpointer_dereference" -> nullpointer_dereference | "use_after_free" -> use_after_free + | "memory_out_of_bounds_access" -> memory_out_of_bounds_access | "double_free" -> double_free | "invalid_memory_deallocation" -> invalid_memory_deallocation | "uninitialized" -> uninitialized @@ -117,6 +120,7 @@ struct | ArrayOutOfBounds e -> "ArrayOutOfBounds" :: ArrayOutOfBounds.path_show e | NullPointerDereference -> ["NullPointerDereference"] | UseAfterFree -> ["UseAfterFree"] + | MemoryOutOfBoundsAccess -> ["MemoryOutOfBoundsAccess"] | DoubleFree -> ["DoubleFree"] | InvalidMemoryDeallocation -> ["InvalidMemoryDeallocation"] | MemoryLeak -> ["MemoryLeak"] @@ -229,6 +233,7 @@ let behaviorName = function |Undefined u -> match u with |NullPointerDereference -> "NullPointerDereference" |UseAfterFree -> "UseAfterFree" + |MemoryOutOfBoundsAccess -> "MemoryOutOfBoundsAccess" |DoubleFree -> "DoubleFree" |InvalidMemoryDeallocation -> "InvalidMemoryDeallocation" |MemoryLeak -> "MemoryLeak" diff --git a/src/util/messages.ml b/src/util/messages.ml index a06a183eee..42a3118978 100644 --- a/src/util/messages.ml +++ b/src/util/messages.ml @@ -248,12 +248,24 @@ let add m = Table.add m ) +let final_table: unit Table.MH.t = Table.MH.create 13 + +let add_final m = + Table.MH.replace final_table m () + let finalize () = if get_bool "warn.deterministic" then ( !Table.messages_list |> List.sort Message.compare |> List.iter print - ) + ); + Table.MH.to_seq_keys final_table + |> List.of_seq + |> List.sort Message.compare + |> List.iter (fun m -> + print m; + Table.add m + ) let current_context: ControlSpecC.t option ref = ref None @@ -282,7 +294,7 @@ let msg_noloc severity ?(tags=[]) ?(category=Category.Unknown) fmt = if !AnalysisState.should_warn && Severity.should_warn severity && (Category.should_warn category || Tags.should_warn tags) then ( let finish doc = let text = GobPretty.show doc in - add {tags = Category category :: tags; severity; multipiece = Single {loc = None; text; context = msg_context ()}} + add {tags = Category category :: tags; severity; multipiece = Single {loc = None; text; context = None}} in Pretty.gprintf finish fmt ) @@ -316,4 +328,15 @@ let debug_noloc ?tags = msg_noloc Debug ?tags let success ?loc = msg Success ?loc let success_noloc ?tags = msg_noloc Success ?tags +let msg_final severity ?(tags=[]) ?(category=Category.Unknown) fmt = + if !AnalysisState.should_warn then ( + let finish doc = + let text = GobPretty.show doc in + add_final {tags = Category category :: tags; severity; multipiece = Single {loc = None; text; context = None}} + in + Pretty.gprintf finish fmt + ) + else + GobPretty.igprintf () fmt + include Tracing diff --git a/src/util/server.ml b/src/util/server.ml index e133fb96c3..22f5a03350 100644 --- a/src/util/server.ml +++ b/src/util/server.ml @@ -264,6 +264,7 @@ let node_locator: Locator.t ResettableLazy.t = let analyze ?(reset=false) (s: t) = Messages.Table.(MH.clear messages_table); + Messages.(Table.MH.clear final_table); Messages.Table.messages_list := []; let file, reparsed = reparse s in if reset then ( diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index a5a572d1c2..f1ee18ed72 100644 --- a/src/witness/svcomp.ml +++ b/src/witness/svcomp.ml @@ -52,6 +52,9 @@ struct | UnreachCall _ -> "unreach-call" | NoOverflow -> "no-overflow" | NoDataRace -> "no-data-race" (* not yet in SV-COMP/Benchexec *) + | ValidFree -> "valid-free" + | ValidDeref -> "valid-deref" + | ValidMemtrack -> "valid-memtrack" in "false(" ^ result_spec ^ ")" | Unknown -> "unknown" diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml index 464c170251..8dafb8873c 100644 --- a/src/witness/svcompSpec.ml +++ b/src/witness/svcompSpec.ml @@ -6,11 +6,15 @@ type t = | UnreachCall of string | NoDataRace | NoOverflow + | ValidFree + | ValidDeref + | ValidMemtrack let of_string s = let s = String.strip s in - let regexp = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in - if Str.string_match regexp s 0 then + let regexp = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )" in + let regexp_negated = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in + if Str.string_match regexp_negated s 0 then let global_not = Str.matched_group 1 s in if global_not = "data-race" then NoDataRace @@ -23,6 +27,16 @@ let of_string s = UnreachCall f else failwith "Svcomp.Specification.of_string: unknown global not expression" + else if Str.string_match regexp s 0 then + let global = Str.matched_group 1 s in + if global = "valid-free" then + ValidFree + else if global = "valid-deref" then + ValidDeref + else if global = "valid-memtrack" then + ValidMemtrack + else + failwith "Svcomp.Specification.of_string: unknown global expression" else failwith "Svcomp.Specification.of_string: unknown expression" @@ -38,9 +52,18 @@ let of_option () = of_string s let to_string spec = - let global_not = match spec with - | UnreachCall f -> "call(" ^ f ^ "())" - | NoDataRace -> "data-race" - | NoOverflow -> "overflow" + let print_output spec_str is_neg = + if is_neg then + Printf.sprintf "CHECK( init(main()), LTL(G ! %s) )" spec_str + else + Printf.sprintf "CHECK( init(main()), LTL(G %s) )" spec_str + in + let spec_str, is_neg = match spec with + | UnreachCall f -> "call(" ^ f ^ "())", true + | NoDataRace -> "data-race", true + | NoOverflow -> "overflow", true + | ValidFree -> "valid-free", false + | ValidDeref -> "valid-deref", false + | ValidMemtrack -> "valid-memtrack", false in - "CHECK( init(main()), LTL(G ! " ^ global_not ^ ") )" + print_output spec_str is_neg diff --git a/src/witness/witness.ml b/src/witness/witness.ml index baa465a1b3..0e237716fd 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -505,6 +505,96 @@ struct in (module TaskResult:WitnessTaskResult) ) + | ValidFree -> + let module TrivialArg = + struct + include Arg + let next _ = [] + end + in + if not !AnalysisState.svcomp_may_invalid_free then + let module TaskResult = + struct + module Arg = Arg + let result = Result.True + let invariant _ = Invariant.none + let is_violation _ = false + let is_sink _ = false + end + in + (module TaskResult:WitnessTaskResult) + else ( + let module TaskResult = + struct + module Arg = TrivialArg + let result = Result.Unknown + let invariant _ = Invariant.none + let is_violation _ = false + let is_sink _ = false + end + in + (module TaskResult:WitnessTaskResult) + ) + | ValidDeref -> + let module TrivialArg = + struct + include Arg + let next _ = [] + end + in + if not !AnalysisState.svcomp_may_invalid_deref then + let module TaskResult = + struct + module Arg = Arg + let result = Result.True + let invariant _ = Invariant.none + let is_violation _ = false + let is_sink _ = false + end + in + (module TaskResult:WitnessTaskResult) + else ( + let module TaskResult = + struct + module Arg = TrivialArg + let result = Result.Unknown + let invariant _ = Invariant.none + let is_violation _ = false + let is_sink _ = false + end + in + (module TaskResult:WitnessTaskResult) + ) + | ValidMemtrack -> + let module TrivialArg = + struct + include Arg + let next _ = [] + end + in + if not !AnalysisState.svcomp_may_invalid_memtrack then + let module TaskResult = + struct + module Arg = Arg + let result = Result.True + let invariant _ = Invariant.none + let is_violation _ = false + let is_sink _ = false + end + in + (module TaskResult:WitnessTaskResult) + else ( + let module TaskResult = + struct + module Arg = TrivialArg + let result = Result.Unknown + let invariant _ = Invariant.none + let is_violation _ = false + let is_sink _ = false + end + in + (module TaskResult:WitnessTaskResult) + ) let write entrystates = diff --git a/tests/regression/00-sanity/37-long-double.c b/tests/regression/00-sanity/37-long-double.c new file mode 100644 index 0000000000..01c9b8bb9b --- /dev/null +++ b/tests/regression/00-sanity/37-long-double.c @@ -0,0 +1,4 @@ +int main() { + long double l = 0.0L; + return (int)l; +} diff --git a/tests/regression/00-sanity/37-long-double.t b/tests/regression/00-sanity/37-long-double.t new file mode 100644 index 0000000000..567db89e5a --- /dev/null +++ b/tests/regression/00-sanity/37-long-double.t @@ -0,0 +1,6 @@ +Testing that there isn't a warning about treating long double as double constant. + $ goblint 37-long-double.c + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 3 + dead: 0 + total lines: 3 diff --git a/tests/regression/01-cpa/33-asserts.c b/tests/regression/01-cpa/33-asserts.c index f8bf6c3132..26efad44fc 100644 --- a/tests/regression/01-cpa/33-asserts.c +++ b/tests/regression/01-cpa/33-asserts.c @@ -26,14 +26,14 @@ int main(){ check(j==6); // assert UNKNOWN unknown(&k); - assume(k==4); // TODO? assert SUCCESS + assume(k==4); check(k==4); // assert SUCCESS unknown(&k); - assume(k+1==n); // TODO? FAIL + assume(k+1==n); - assume(n==5); // TODO? NOWARN - assert(0); // NOWARN + assume(n==5); // contradiction + assert(0); // NOWARN (unreachable) return 0; } \ No newline at end of file diff --git a/tests/regression/03-practical/31-zstd-cctxpool-blobs.c b/tests/regression/03-practical/31-zstd-cctxpool-blobs.c new file mode 100644 index 0000000000..40e448eb22 --- /dev/null +++ b/tests/regression/03-practical/31-zstd-cctxpool-blobs.c @@ -0,0 +1,29 @@ +#include +#include + +struct ZSTD_CCtx_s { + int bmi2; +}; + +typedef struct ZSTD_CCtx_s ZSTD_CCtx; + +typedef struct { + ZSTD_CCtx* cctx[1]; +} ZSTDMT_CCtxPool; + +void *t_fun(void *arg) { + return NULL; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); // enter multithreaded + + ZSTDMT_CCtxPool* const cctxPool = calloc(1, sizeof(ZSTDMT_CCtxPool)); + cctxPool->cctx[0] = malloc(sizeof(ZSTD_CCtx)); + if (!cctxPool->cctx[0]) // TODO NOWARN + __goblint_check(1); // TODO reachable + else + __goblint_check(1); // TODO reachable + return 0; +} diff --git a/tests/regression/04-mutex/49-type-invariants.t b/tests/regression/04-mutex/49-type-invariants.t index 3ddd8f237d..4c105d1559 100644 --- a/tests/regression/04-mutex/49-type-invariants.t +++ b/tests/regression/04-mutex/49-type-invariants.t @@ -21,6 +21,7 @@ [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:21:3-21:21) [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:21:3-21:21) [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:21:3-21:21) + [Error][Imprecise][Unsound] Function definition missing $ goblint --enable warn.deterministic --disable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21) @@ -45,3 +46,4 @@ [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:21:3-21:21) [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:21:3-21:21) [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:21:3-21:21) + [Error][Imprecise][Unsound] Function definition missing diff --git a/tests/regression/04-mutex/58-pthread-lock-return.c b/tests/regression/04-mutex/58-pthread-lock-return.c new file mode 100644 index 0000000000..3e2a05c94e --- /dev/null +++ b/tests/regression/04-mutex/58-pthread-lock-return.c @@ -0,0 +1,118 @@ +// PARAM: --disable sem.lock.fail +#include + +int g_mutex = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; + +int g_rwlock = 0; +pthread_rwlock_t rwlock = PTHREAD_RWLOCK_INITIALIZER; + +// OS X has no spinlock +#ifndef __APPLE__ +int g_spin = 0; +pthread_spinlock_t spin; +#endif + +void *t_fun(void *arg) { + if (!pthread_mutex_lock(&mutex)) { + __goblint_check(1); // reachable + g_mutex++; // NORACE + pthread_mutex_unlock(&mutex); + } + else { + __goblint_check(0); // NOWARN (unreachable) + } + + if (!pthread_mutex_trylock(&mutex)) { + __goblint_check(1); // reachable + g_mutex++; // NORACE + pthread_mutex_unlock(&mutex); + } + else { + __goblint_check(1); // reachable + } + + if (!pthread_rwlock_wrlock(&mutex)) { + __goblint_check(1); // reachable + g_rwlock++; // NORACE + pthread_rwlock_unlock(&mutex); + } + else { + __goblint_check(0); // NOWARN (unreachable) + } + + if (!pthread_rwlock_trywrlock(&mutex)) { + __goblint_check(1); // reachable + g_rwlock++; // NORACE + pthread_rwlock_unlock(&mutex); + } + else { + __goblint_check(1); // reachable + } + + if (!pthread_rwlock_rdlock(&mutex)) { + __goblint_check(1); // reachable + g_rwlock++; // NORACE + pthread_rwlock_unlock(&mutex); + } + else { + __goblint_check(0); // NOWARN (unreachable) + } + + if (!pthread_rwlock_tryrdlock(&mutex)) { + __goblint_check(1); // reachable + g_rwlock++; // NORACE + pthread_rwlock_unlock(&mutex); + } + else { + __goblint_check(1); // reachable + } + +#ifndef __APPLE__ + if (!pthread_spin_lock(&spin)) { + __goblint_check(1); // TODO reachable (TODO for OSX) + g_spin++; // NORACE + pthread_spin_unlock(&spin); + } + else { + __goblint_check(0); // NOWARN (unreachable) + } + + if (!pthread_spin_trylock(&spin)) { + __goblint_check(1); // TODO reachable (TODO for OSX) + g_spin++; // NORACE + pthread_spin_unlock(&spin); + } + else { + __goblint_check(1); // TODO reachable (TODO for OSX) + } +#endif + + return NULL; +} + +int main() { +#ifndef __APPLE__ + pthread_spin_init(&spin, PTHREAD_PROCESS_PRIVATE); +#endif + + pthread_t id; + pthread_create(&id, NULL, &t_fun, NULL); + + pthread_mutex_lock(&mutex); + g_mutex++; // NORACE + pthread_mutex_unlock(&mutex); + + pthread_rwlock_wrlock(&mutex); + g_rwlock++; // NORACE + pthread_rwlock_unlock(&mutex); + +#ifndef __APPLE__ + pthread_spin_lock(&spin); + g_spin++; // NORACE + pthread_spin_unlock(&spin); +#endif + + pthread_join(id, NULL); + return 0; +} diff --git a/tests/regression/04-mutex/62-simple_atomic_nr.c b/tests/regression/04-mutex/62-simple_atomic_nr.c index d63f303251..fdef44bdd6 100644 --- a/tests/regression/04-mutex/62-simple_atomic_nr.c +++ b/tests/regression/04-mutex/62-simple_atomic_nr.c @@ -1,24 +1,83 @@ #include -#include #include -atomic_int myglobal; -pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; -pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; +atomic_int g1; +_Atomic int g2; +_Atomic(int) g3; + +atomic_int a1[1]; +_Atomic int a2[1]; +_Atomic(int) a3[1]; + +struct s { + int f0; + atomic_int f1; + _Atomic int f2; + _Atomic(int) f3; +}; + +struct s s1; +_Atomic struct s s2; +_Atomic(struct s) s3; + +typedef atomic_int t_int1; +typedef _Atomic int t_int2; +typedef _Atomic(int) t_int3; + +t_int1 t1; +t_int2 t2; +t_int3 t3; + +typedef int t_int0; + +_Atomic t_int0 t0; +_Atomic(t_int0) t00; + +atomic_int *p0 = &g1; +int x; +// int * _Atomic p1 = &x; // TODO: https://github.com/goblint/cil/issues/64 +// _Atomic(int*) p2 = &x; // TODO: https://github.com/goblint/cil/issues/64 +// atomic_int * _Atomic p3 = &g1; // TODO: https://github.com/goblint/cil/issues/64 + +atomic_flag flag = ATOMIC_FLAG_INIT; void *t_fun(void *arg) { - pthread_mutex_lock(&mutex1); - myglobal=myglobal+1; // NORACE - pthread_mutex_unlock(&mutex1); + g1++; // NORACE + g2++; // NORACE + g3++; // NORACE + a1[0]++; // NORACE + a2[0]++; // NORACE + a3[0]++; // NORACE + s1.f1++; // NORACE + s1.f2++; // NORACE + s1.f3++; // NORACE + s2.f0++; // NORACE + s3.f0++; // NORACE + t1++; // NORACE + t2++; // NORACE + t3++; // NORACE + t0++; // NORACE + t00++; // NORACE + (*p0)++; // NORACE + // p1++; // TODO NORACE: https://github.com/goblint/cil/issues/64 + // p2++; // TODO NORACE: https://github.com/goblint/cil/issues/64 + // p3++; // TODO NORACE: https://github.com/goblint/cil/issues/64 + // (*p3)++; // TODO NORACE: https://github.com/goblint/cil/issues/64 + + struct s ss = {0}; + s2 = ss; // NORACE + s3 = ss; // NORACE + + atomic_flag_clear(&flag); // NORACE + atomic_flag_test_and_set(&flag); // NORACE return NULL; } int main(void) { - pthread_t id; + pthread_t id, id2; pthread_create(&id, NULL, t_fun, NULL); - pthread_mutex_lock(&mutex2); - myglobal=myglobal+1; // NORACE - pthread_mutex_unlock(&mutex2); - pthread_join (id, NULL); + pthread_create(&id2, NULL, t_fun, NULL); + pthread_join(id, NULL); + pthread_join(id2, NULL); return 0; } diff --git a/tests/regression/04-mutex/77-type-nested-fields.t b/tests/regression/04-mutex/77-type-nested-fields.t index 738784f5d5..bb935cb0ed 100644 --- a/tests/regression/04-mutex/77-type-nested-fields.t +++ b/tests/regression/04-mutex/77-type-nested-fields.t @@ -27,3 +27,4 @@ [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:38:3-38:22) [Error][Imprecise][Unsound] Function definition missing for getS (77-type-nested-fields.c:31:3-31:20) [Error][Imprecise][Unsound] Function definition missing for getT (77-type-nested-fields.c:38:3-38:22) + [Error][Imprecise][Unsound] Function definition missing diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.t b/tests/regression/04-mutex/79-type-nested-fields-deep1.t index 2e15f83c39..ba1399d225 100644 --- a/tests/regression/04-mutex/79-type-nested-fields-deep1.t +++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.t @@ -27,3 +27,4 @@ [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:43:3-43:24) [Error][Imprecise][Unsound] Function definition missing for getS (79-type-nested-fields-deep1.c:36:3-36:20) [Error][Imprecise][Unsound] Function definition missing for getU (79-type-nested-fields-deep1.c:43:3-43:24) + [Error][Imprecise][Unsound] Function definition missing diff --git a/tests/regression/04-mutex/80-type-nested-fields-deep2.t b/tests/regression/04-mutex/80-type-nested-fields-deep2.t index 48e726f623..71bdcfb2e2 100644 --- a/tests/regression/04-mutex/80-type-nested-fields-deep2.t +++ b/tests/regression/04-mutex/80-type-nested-fields-deep2.t @@ -27,3 +27,4 @@ [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:43:3-43:24) [Error][Imprecise][Unsound] Function definition missing for getT (80-type-nested-fields-deep2.c:36:3-36:22) [Error][Imprecise][Unsound] Function definition missing for getU (80-type-nested-fields-deep2.c:43:3-43:24) + [Error][Imprecise][Unsound] Function definition missing diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.t b/tests/regression/04-mutex/90-distribute-fields-type-1.t index ba3e3da0ed..46435045b9 100644 --- a/tests/regression/04-mutex/90-distribute-fields-type-1.t +++ b/tests/regression/04-mutex/90-distribute-fields-type-1.t @@ -29,3 +29,4 @@ [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:39:3-39:17) [Error][Imprecise][Unsound] Function definition missing for getS (90-distribute-fields-type-1.c:31:3-31:20) [Error][Imprecise][Unsound] Function definition missing for getT (90-distribute-fields-type-1.c:39:3-39:17) + [Error][Imprecise][Unsound] Function definition missing diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.t b/tests/regression/04-mutex/91-distribute-fields-type-2.t index fd544b0b0b..c7e66c0527 100644 --- a/tests/regression/04-mutex/91-distribute-fields-type-2.t +++ b/tests/regression/04-mutex/91-distribute-fields-type-2.t @@ -29,3 +29,4 @@ [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:40:3-40:17) [Error][Imprecise][Unsound] Function definition missing for getS (91-distribute-fields-type-2.c:32:3-32:17) [Error][Imprecise][Unsound] Function definition missing for getT (91-distribute-fields-type-2.c:40:3-40:17) + [Error][Imprecise][Unsound] Function definition missing diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.t b/tests/regression/04-mutex/92-distribute-fields-type-deep.t index aefc1520d1..4fc1c7e101 100644 --- a/tests/regression/04-mutex/92-distribute-fields-type-deep.t +++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.t @@ -29,3 +29,4 @@ [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:44:3-44:17) [Error][Imprecise][Unsound] Function definition missing for getS (92-distribute-fields-type-deep.c:36:3-36:20) [Error][Imprecise][Unsound] Function definition missing for getU (92-distribute-fields-type-deep.c:44:3-44:17) + [Error][Imprecise][Unsound] Function definition missing diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.t b/tests/regression/04-mutex/93-distribute-fields-type-global.t index 2199c689b1..bf34d99936 100644 --- a/tests/regression/04-mutex/93-distribute-fields-type-global.t +++ b/tests/regression/04-mutex/93-distribute-fields-type-global.t @@ -23,3 +23,4 @@ [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (93-distribute-fields-type-global.c:13:3-13:29) [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (93-distribute-fields-type-global.c:13:3-13:29) [Error][Imprecise][Unsound] Function definition missing for getS (93-distribute-fields-type-global.c:13:3-13:29) + [Error][Imprecise][Unsound] Function definition missing diff --git a/tests/regression/04-mutex/99-volatile.c b/tests/regression/04-mutex/99-volatile.c index aaf81f13a1..7c2a255902 100644 --- a/tests/regression/04-mutex/99-volatile.c +++ b/tests/regression/04-mutex/99-volatile.c @@ -1,18 +1,53 @@ // PARAM: --disable ana.race.volatile #include -#include -volatile int myglobal; +volatile int g1; + +volatile int a1[1]; + +struct s { + int f0; + volatile int f1; +}; + +struct s s1; +volatile struct s s2; + +typedef volatile int t_int1; + +t_int1 t1; + +typedef int t_int0; + +volatile t_int0 t0; + +volatile int *p0 = &g1; +int x; +int * volatile p1 = &x; +volatile int * volatile p2 = &g1; void *t_fun(void *arg) { - myglobal= 8; //NORACE + g1++; // NORACE + a1[0]++; // NORACE + s1.f1++; // NORACE + s2.f0++; // NORACE + t1++; // NORACE + t0++; // NORACE + (*p0)++; // NORACE + p1++; // NORACE + p2++; // NORACE + (*p2)++; // NORACE + + struct s ss = {0}; + s2 = ss; // NORACE return NULL; } int main(void) { - pthread_t id; - pthread_create(&id, NULL, t_fun, (void*) &myglobal); - myglobal = 42; //NORACE - pthread_join (id, NULL); + pthread_t id, id2; + pthread_create(&id, NULL, t_fun, NULL); + pthread_create(&id2, NULL, t_fun, NULL); + pthread_join(id, NULL); + pthread_join(id2, NULL); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/05-lval_ls/20-race-null-void.c b/tests/regression/05-lval_ls/20-race-null-void.c new file mode 100644 index 0000000000..1950ada73e --- /dev/null +++ b/tests/regression/05-lval_ls/20-race-null-void.c @@ -0,0 +1,54 @@ +#include +#include + +void *t_fun(void *arg) { + void **top; + free(top); // RACE + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + int r; // rand + int zero = 0; // IntDomain zero + void *null; + __goblint_assume(null == NULL); // AddressDomain NULL + int one = 1; // IntDomain one + void *unknown; + __goblint_assume(unknown != NULL); // AddressDomain unknown + void *top; + switch (r) { + case 0: + pthread_join(id, NULL); // NORACE + break; + case 1: + pthread_join(id, 0); // NORACE + break; + case 2: + pthread_join(id, zero); // NORACE + break; + case 3: + pthread_join(id, 1); // RACE + break; + case 4: + pthread_join(id, one); // RACE + break; + case 5: + pthread_join(id, r); // RACE + break; + case 6: + pthread_join(id, null); // NORACE + break; + case 7: + pthread_join(id, unknown); // RACE + break; + case 8: + pthread_join(id, top); // RACE + break; + default: + break; + } + return 0; +} diff --git a/tests/regression/05-lval_ls/21-race-null-type.c b/tests/regression/05-lval_ls/21-race-null-type.c new file mode 100644 index 0000000000..6b5e6e42fd --- /dev/null +++ b/tests/regression/05-lval_ls/21-race-null-type.c @@ -0,0 +1,55 @@ +// PARAM: --enable ana.race.direct-arithmetic +#include +#include + +void *t_fun(void *arg) { + void *top; + time(top); // RACE + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + int r; // rand + int zero = 0; // IntDomain zero + void *null; + __goblint_assume(null == NULL); // AddressDomain NULL + int one = 1; // IntDomain one + void *unknown; + __goblint_assume(unknown != NULL); // AddressDomain unknown + void *top; + switch (r) { + case 0: + time(NULL); // NORACE + break; + case 1: + time(0); // NORACE + break; + case 2: + time(zero); // NORACE + break; + case 3: + time(1); // RACE + break; + case 4: + time(one); // RACE + break; + case 5: + time(r); // RACE + break; + case 6: + time(null); // NORACE + break; + case 7: + time(unknown); // RACE + break; + case 8: + time(top); // RACE + break; + default: + break; + } + return 0; +} diff --git a/tests/regression/05-lval_ls/22-race-null-void-deep.c b/tests/regression/05-lval_ls/22-race-null-void-deep.c new file mode 100644 index 0000000000..7e99f286b6 --- /dev/null +++ b/tests/regression/05-lval_ls/22-race-null-void-deep.c @@ -0,0 +1,56 @@ +#include +#include + +pthread_key_t key; + +void *t_fun(void *arg) { + void *top; + pthread_setspecific(key, top); // RACE + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + int r; // rand + int zero = 0; // IntDomain zero + void *null; + __goblint_assume(null == NULL); // AddressDomain NULL + int one = 1; // IntDomain one + void *unknown; + __goblint_assume(unknown != NULL); // AddressDomain unknown + void *top; + switch (r) { + case 0: + pthread_setspecific(key, NULL); // NORACE + break; + case 1: + pthread_setspecific(key, 0); // NORACE + break; + case 2: + pthread_setspecific(key, zero); // NORACE + break; + case 3: + pthread_setspecific(key, 1); // RACE + break; + case 4: + pthread_setspecific(key, one); // RACE + break; + case 5: + pthread_setspecific(key, r); // RACE + break; + case 6: + pthread_setspecific(key, null); // NORACE + break; + case 7: + pthread_setspecific(key, unknown); // RACE + break; + case 8: + pthread_setspecific(key, top); // RACE + break; + default: + break; + } + return 0; +} diff --git a/tests/regression/05-lval_ls/23-race-null-type-deep.c b/tests/regression/05-lval_ls/23-race-null-type-deep.c new file mode 100644 index 0000000000..f7de758d8f --- /dev/null +++ b/tests/regression/05-lval_ls/23-race-null-type-deep.c @@ -0,0 +1,60 @@ +// PARAM: --disable sem.unknown_function.invalidate.globals --disable sem.unknown_function.spawn +#include + +struct s { + int f; +}; + +extern void magic(struct s *p); + +void *t_fun(void *arg) { + void *top; + magic(top); // RACE + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + int r; // rand + int zero = 0; // IntDomain zero + void *null; + __goblint_assume(null == NULL); // AddressDomain NULL + int one = 1; // IntDomain one + void *unknown; + __goblint_assume(unknown != NULL); // AddressDomain unknown + void *top; + switch (r) { + case 0: + magic(NULL); // NORACE + break; + case 1: + magic(0); // NORACE + break; + case 2: + magic(zero); // NORACE + break; + case 3: + magic(1); // RACE + break; + case 4: + magic(one); // RACE + break; + case 5: + magic(r); // RACE + break; + case 6: + magic(null); // NORACE + break; + case 7: + magic(unknown); // RACE + break; + case 8: + magic(top); // RACE + break; + default: + break; + } + return 0; +} diff --git a/tests/regression/06-symbeq/16-type_rc.t b/tests/regression/06-symbeq/16-type_rc.t index 06a3b314a4..b63471a45e 100644 --- a/tests/regression/06-symbeq/16-type_rc.t +++ b/tests/regression/06-symbeq/16-type_rc.t @@ -10,6 +10,7 @@ Disable info messages because race summary contains (safe) memory location count write with [mhp:{tid=[main]; created={[main, t_fun@16-type_rc.c:35:3-35:37#top]}}, thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:36:3-36:9) [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24) [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14) + [Error][Imprecise][Unsound] Function definition missing $ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable allglobs 16-type_rc.c [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:21:3-21:15) @@ -20,3 +21,4 @@ Disable info messages because race summary contains (safe) memory location count write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#top]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#top]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24) [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14) + [Error][Imprecise][Unsound] Function definition missing diff --git a/tests/regression/06-symbeq/21-mult_accs_rc.t b/tests/regression/06-symbeq/21-mult_accs_rc.t index 9b02dcde76..227c66058e 100644 --- a/tests/regression/06-symbeq/21-mult_accs_rc.t +++ b/tests/regression/06-symbeq/21-mult_accs_rc.t @@ -15,6 +15,7 @@ Disable info messages because race summary contains (safe) memory location count [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:13:3-13:14) [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:15:3-15:14) [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:27:3-27:14) + [Error][Imprecise][Unsound] Function definition missing $ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable allglobs 21-mult_accs_rc.c [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:14:3-14:32) @@ -30,3 +31,4 @@ Disable info messages because race summary contains (safe) memory location count [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:13:3-13:14) [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:15:3-15:14) [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:27:3-27:14) + [Error][Imprecise][Unsound] Function definition missing diff --git a/tests/regression/09-regions/40-zstd-thread-pool-region.c b/tests/regression/09-regions/40-zstd-thread-pool-region.c new file mode 100644 index 0000000000..13baf5ec3f --- /dev/null +++ b/tests/regression/09-regions/40-zstd-thread-pool-region.c @@ -0,0 +1,34 @@ +// SKIP PARAM: --set ana.activated[+] region +// FIXPOINT +#include +#include +#include + +typedef struct POOL_job_s { + void *opaque; +} POOL_job; + +typedef struct POOL_ctx_s { + POOL_job *queue; +} POOL_ctx; + +POOL_ctx* ctx_global; + +POOL_ctx* POOL_create(size_t numThreads, size_t queueSize) +{ + POOL_ctx* ctx_create; + ctx_create = (POOL_ctx*)malloc(sizeof(POOL_ctx)); + ctx_create->queue = (POOL_job*)malloc(queueSize * sizeof(POOL_job)); + + int r; // rand + if (r) + ctx_global = ctx_create; // pretend escape + return ctx_create; +} + +int main() { + while (1) { + POOL_ctx *ctx_main; + ctx_main = POOL_create(20, 10); + } +} diff --git a/tests/regression/28-race_reach/01-simple_racing.c b/tests/regression/28-race_reach/01-simple_racing.c index 16a0fb28c9..f444228690 100644 --- a/tests/regression/28-race_reach/01-simple_racing.c +++ b/tests/regression/28-race_reach/01-simple_racing.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -19,4 +20,4 @@ int main(void) { pthread_mutex_unlock(&mutex2); join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/02-simple_racefree.c b/tests/regression/28-race_reach/02-simple_racefree.c index 4713ccd48d..0e35f8da67 100644 --- a/tests/regression/28-race_reach/02-simple_racefree.c +++ b/tests/regression/28-race_reach/02-simple_racefree.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -19,4 +20,4 @@ int main(void) { pthread_mutex_unlock(&mutex1); join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/03-munge_racing.c b/tests/regression/28-race_reach/03-munge_racing.c index 3c279d597a..9b8536e540 100644 --- a/tests/regression/28-race_reach/03-munge_racing.c +++ b/tests/regression/28-race_reach/03-munge_racing.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -26,4 +27,4 @@ int main(void) { create_threads(t1); create_threads(t2); join_threads(t1); join_threads(t2); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/04-munge_racefree.c b/tests/regression/28-race_reach/04-munge_racefree.c index 799477e6ae..86637da91f 100644 --- a/tests/regression/28-race_reach/04-munge_racefree.c +++ b/tests/regression/28-race_reach/04-munge_racefree.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -26,4 +27,4 @@ int main(void) { create_threads(t1); create_threads(t2); join_threads(t1); join_threads(t2); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/05-lockfuns_racefree.c b/tests/regression/28-race_reach/05-lockfuns_racefree.c index 0faecd0217..0a904005f8 100644 --- a/tests/regression/28-race_reach/05-lockfuns_racefree.c +++ b/tests/regression/28-race_reach/05-lockfuns_racefree.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -26,4 +27,4 @@ int main(void) { unlock(); join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/06-cond_racing1.c b/tests/regression/28-race_reach/06-cond_racing1.c index c3e87507d5..931b68f81f 100644 --- a/tests/regression/28-race_reach/06-cond_racing1.c +++ b/tests/regression/28-race_reach/06-cond_racing1.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include @@ -31,7 +32,3 @@ int main() { join_threads(t); return 0; } - - - - diff --git a/tests/regression/28-race_reach/07-cond_racing2.c b/tests/regression/28-race_reach/07-cond_racing2.c index b13b52dd1c..5e0d3f77f5 100644 --- a/tests/regression/28-race_reach/07-cond_racing2.c +++ b/tests/regression/28-race_reach/07-cond_racing2.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/08-cond_racefree.c b/tests/regression/28-race_reach/08-cond_racefree.c index ce18620121..8d86e89cf5 100644 --- a/tests/regression/28-race_reach/08-cond_racefree.c +++ b/tests/regression/28-race_reach/08-cond_racefree.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/09-ptrmunge_racing.c b/tests/regression/28-race_reach/09-ptrmunge_racing.c index 3191ca3ead..eb6a098800 100644 --- a/tests/regression/28-race_reach/09-ptrmunge_racing.c +++ b/tests/regression/28-race_reach/09-ptrmunge_racing.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -27,4 +28,4 @@ int main(void) { create_threads(t1); create_threads(t2); join_threads(t1); join_threads(t2); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/10-ptrmunge_racefree.c b/tests/regression/28-race_reach/10-ptrmunge_racefree.c index d4e2144971..b21a1e9480 100644 --- a/tests/regression/28-race_reach/10-ptrmunge_racefree.c +++ b/tests/regression/28-race_reach/10-ptrmunge_racefree.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -27,4 +28,4 @@ int main(void) { create_threads(t1); create_threads(t2); join_threads(t1); join_threads(t2); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/11-ptr_racing.c b/tests/regression/28-race_reach/11-ptr_racing.c index dc3f3c1a21..d6851afa82 100644 --- a/tests/regression/28-race_reach/11-ptr_racing.c +++ b/tests/regression/28-race_reach/11-ptr_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -20,4 +21,4 @@ int main(void) { pthread_mutex_unlock(&mutex2); join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/12-ptr_racefree.c b/tests/regression/28-race_reach/12-ptr_racefree.c index bb7bcffa3d..b22a942eda 100644 --- a/tests/regression/28-race_reach/12-ptr_racefree.c +++ b/tests/regression/28-race_reach/12-ptr_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -16,8 +17,8 @@ void *t_fun(void *arg) { int main(void) { create_threads(t); pthread_mutex_lock(&mutex1); - assert_racefree(global); + assert_racefree(global); pthread_mutex_unlock(&mutex1); join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/19-callback_racing.c b/tests/regression/28-race_reach/19-callback_racing.c index 798d1e2783..04eaaeef4f 100644 --- a/tests/regression/28-race_reach/19-callback_racing.c +++ b/tests/regression/28-race_reach/19-callback_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp extern int __VERIFIER_nondet_int(); #include diff --git a/tests/regression/28-race_reach/20-callback_racefree.c b/tests/regression/28-race_reach/20-callback_racefree.c index 6f30ef492d..e41896f31a 100644 --- a/tests/regression/28-race_reach/20-callback_racefree.c +++ b/tests/regression/28-race_reach/20-callback_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp extern int __VERIFIER_nondet_int(); #include diff --git a/tests/regression/28-race_reach/21-deref_read_racing.c b/tests/regression/28-race_reach/21-deref_read_racing.c index 93166f8125..880a8a4d38 100644 --- a/tests/regression/28-race_reach/21-deref_read_racing.c +++ b/tests/regression/28-race_reach/21-deref_read_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/22-deref_read_racefree.c b/tests/regression/28-race_reach/22-deref_read_racefree.c index 3386277083..9ed4fb03cf 100644 --- a/tests/regression/28-race_reach/22-deref_read_racefree.c +++ b/tests/regression/28-race_reach/22-deref_read_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -17,7 +18,7 @@ int main() { create_threads(t); q = p; pthread_mutex_lock(&mutex); - assert_racefree(*q); // TODO + assert_racefree(*q); pthread_mutex_unlock(&mutex); return 0; } diff --git a/tests/regression/28-race_reach/23-sound_unlock_racing.c b/tests/regression/28-race_reach/23-sound_unlock_racing.c index da8db888db..c3ed280fbd 100644 --- a/tests/regression/28-race_reach/23-sound_unlock_racing.c +++ b/tests/regression/28-race_reach/23-sound_unlock_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/24-sound_lock_racing.c b/tests/regression/28-race_reach/24-sound_lock_racing.c index 89ed5103dc..597bea716c 100644 --- a/tests/regression/28-race_reach/24-sound_lock_racing.c +++ b/tests/regression/28-race_reach/24-sound_lock_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/27-funptr_racing.c b/tests/regression/28-race_reach/27-funptr_racing.c index 2c970deaf3..7210d0d56c 100644 --- a/tests/regression/28-race_reach/27-funptr_racing.c +++ b/tests/regression/28-race_reach/27-funptr_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include #include "racemacros.h" @@ -5,11 +6,11 @@ int global; pthread_mutex_t gm = PTHREAD_MUTEX_INITIALIZER; -void bad() { +void bad() { access(global); } -void good() { +void good() { pthread_mutex_lock(&gm); access(global); pthread_mutex_unlock(&gm); @@ -42,4 +43,4 @@ int main() { join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/28-funptr_racefree.c b/tests/regression/28-race_reach/28-funptr_racefree.c index 4e39156ecf..f36168aaaa 100644 --- a/tests/regression/28-race_reach/28-funptr_racefree.c +++ b/tests/regression/28-race_reach/28-funptr_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include #include "racemacros.h" @@ -5,10 +6,10 @@ int global = 0; pthread_mutex_t gm = PTHREAD_MUTEX_INITIALIZER; -void bad() { +void bad() { access(global); -} -void good() { +} +void good() { pthread_mutex_lock(&gm); access(global); pthread_mutex_unlock(&gm); @@ -41,4 +42,4 @@ int main() { join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/36-indirect_racefree.c b/tests/regression/28-race_reach/36-indirect_racefree.c index 97dd10fc85..a2733f9df3 100644 --- a/tests/regression/28-race_reach/36-indirect_racefree.c +++ b/tests/regression/28-race_reach/36-indirect_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/37-indirect_racing.c b/tests/regression/28-race_reach/37-indirect_racing.c index e769a24836..6bf5757991 100644 --- a/tests/regression/28-race_reach/37-indirect_racing.c +++ b/tests/regression/28-race_reach/37-indirect_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/40-trylock_racing.c b/tests/regression/28-race_reach/40-trylock_racing.c index 4d9c4acb98..94694bc1eb 100644 --- a/tests/regression/28-race_reach/40-trylock_racing.c +++ b/tests/regression/28-race_reach/40-trylock_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -25,4 +26,4 @@ int main(void) { pthread_mutex_unlock(&mutex); // no UB because ERRORCHECK join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/41-trylock_racefree.c b/tests/regression/28-race_reach/41-trylock_racefree.c index 0e521474c5..ce68d3abe2 100644 --- a/tests/regression/28-race_reach/41-trylock_racefree.c +++ b/tests/regression/28-race_reach/41-trylock_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -22,4 +23,4 @@ int main(void) { pthread_mutex_unlock(&mutex); join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/42-trylock2_racefree.c b/tests/regression/28-race_reach/42-trylock2_racefree.c index 5f50097355..8b73328281 100644 --- a/tests/regression/28-race_reach/42-trylock2_racefree.c +++ b/tests/regression/28-race_reach/42-trylock2_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -35,4 +36,4 @@ int main(void) { join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/45-escape_racing.c b/tests/regression/28-race_reach/45-escape_racing.c index a27db9a9df..31cb5fcacc 100644 --- a/tests/regression/28-race_reach/45-escape_racing.c +++ b/tests/regression/28-race_reach/45-escape_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/46-escape_racefree.c b/tests/regression/28-race_reach/46-escape_racefree.c index af4874534e..731a61483e 100644 --- a/tests/regression/28-race_reach/46-escape_racefree.c +++ b/tests/regression/28-race_reach/46-escape_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/51-mutexptr_racefree.c b/tests/regression/28-race_reach/51-mutexptr_racefree.c index 972cd6e667..c57b58eb61 100644 --- a/tests/regression/28-race_reach/51-mutexptr_racefree.c +++ b/tests/regression/28-race_reach/51-mutexptr_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/60-invariant_racefree.c b/tests/regression/28-race_reach/60-invariant_racefree.c index d396e349bc..b8b86a86ca 100644 --- a/tests/regression/28-race_reach/60-invariant_racefree.c +++ b/tests/regression/28-race_reach/60-invariant_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/61-invariant_racing.c b/tests/regression/28-race_reach/61-invariant_racing.c index 3facd56d32..b61f34ba25 100644 --- a/tests/regression/28-race_reach/61-invariant_racing.c +++ b/tests/regression/28-race_reach/61-invariant_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -6,9 +7,12 @@ pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; void *t_fun(void *arg) { pthread_mutex_lock(&mutex); - if (x == 0) { + pthread_mutex_lock(&__global_lock); + if (x == 0) { // NORACE + pthread_mutex_unlock(&__global_lock); pthread_mutex_unlock(&mutex); } else { + pthread_mutex_unlock(&__global_lock); pthread_mutex_unlock(&mutex); access(x); } diff --git a/tests/regression/28-race_reach/70-funloop_racefree.c b/tests/regression/28-race_reach/70-funloop_racefree.c index 11f44100cd..2ff0cdf9e5 100644 --- a/tests/regression/28-race_reach/70-funloop_racefree.c +++ b/tests/regression/28-race_reach/70-funloop_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/71-funloop_racing.c b/tests/regression/28-race_reach/71-funloop_racing.c index d34be23175..ac20711401 100644 --- a/tests/regression/28-race_reach/71-funloop_racing.c +++ b/tests/regression/28-race_reach/71-funloop_racing.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/72-funloop_hard_racing.c b/tests/regression/28-race_reach/72-funloop_hard_racing.c index d913bb16a6..78e24279f9 100644 --- a/tests/regression/28-race_reach/72-funloop_hard_racing.c +++ b/tests/regression/28-race_reach/72-funloop_hard_racing.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/73-funloop_hard_racefree.c b/tests/regression/28-race_reach/73-funloop_hard_racefree.c index 33571b8c4d..cc48865d24 100644 --- a/tests/regression/28-race_reach/73-funloop_hard_racefree.c +++ b/tests/regression/28-race_reach/73-funloop_hard_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/74-tricky_address1_racefree.c b/tests/regression/28-race_reach/74-tricky_address1_racefree.c index 0fdacd23c2..f9ce5d8b4d 100644 --- a/tests/regression/28-race_reach/74-tricky_address1_racefree.c +++ b/tests/regression/28-race_reach/74-tricky_address1_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/75-tricky_address2_racefree.c b/tests/regression/28-race_reach/75-tricky_address2_racefree.c index 76b3b3752a..162eb8d13a 100644 --- a/tests/regression/28-race_reach/75-tricky_address2_racefree.c +++ b/tests/regression/28-race_reach/75-tricky_address2_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/76-tricky_address3_racefree.c b/tests/regression/28-race_reach/76-tricky_address3_racefree.c index 1a782b670e..70c3d033b2 100644 --- a/tests/regression/28-race_reach/76-tricky_address3_racefree.c +++ b/tests/regression/28-race_reach/76-tricky_address3_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/77-tricky_address4_racing.c b/tests/regression/28-race_reach/77-tricky_address4_racing.c index 5b189aa221..5fea171553 100644 --- a/tests/regression/28-race_reach/77-tricky_address4_racing.c +++ b/tests/regression/28-race_reach/77-tricky_address4_racing.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/78-equ_racing.c b/tests/regression/28-race_reach/78-equ_racing.c index 32e10d5a02..b21d76b889 100644 --- a/tests/regression/28-race_reach/78-equ_racing.c +++ b/tests/regression/28-race_reach/78-equ_racing.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/79-equ_racefree.c b/tests/regression/28-race_reach/79-equ_racefree.c index ba9affb71f..5b8744c322 100644 --- a/tests/regression/28-race_reach/79-equ_racefree.c +++ b/tests/regression/28-race_reach/79-equ_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/81-list_racing.c b/tests/regression/28-race_reach/81-list_racing.c index c131e5c2a1..8b231f843c 100644 --- a/tests/regression/28-race_reach/81-list_racing.c +++ b/tests/regression/28-race_reach/81-list_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" +// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/82-list_racefree.c b/tests/regression/28-race_reach/82-list_racefree.c index 67470cf8e0..5bab3c5c31 100644 --- a/tests/regression/28-race_reach/82-list_racefree.c +++ b/tests/regression/28-race_reach/82-list_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" +// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/83-list2_racing1.c b/tests/regression/28-race_reach/83-list2_racing1.c index 6002bc73d4..f0d9f9744b 100644 --- a/tests/regression/28-race_reach/83-list2_racing1.c +++ b/tests/regression/28-race_reach/83-list2_racing1.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" +// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/84-list2_racing2.c b/tests/regression/28-race_reach/84-list2_racing2.c index d807e2d0ac..ce15b2ddf5 100644 --- a/tests/regression/28-race_reach/84-list2_racing2.c +++ b/tests/regression/28-race_reach/84-list2_racing2.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" +// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/85-list2_racefree.c b/tests/regression/28-race_reach/85-list2_racefree.c index b0fb1baa83..cef0e1cb08 100644 --- a/tests/regression/28-race_reach/85-list2_racefree.c +++ b/tests/regression/28-race_reach/85-list2_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" +// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/86-lists_racing.c b/tests/regression/28-race_reach/86-lists_racing.c index 0548dcab37..e90b699212 100644 --- a/tests/regression/28-race_reach/86-lists_racing.c +++ b/tests/regression/28-race_reach/86-lists_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" +// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/87-lists_racefree.c b/tests/regression/28-race_reach/87-lists_racefree.c index 0d05e5b2c2..8e51670b61 100644 --- a/tests/regression/28-race_reach/87-lists_racefree.c +++ b/tests/regression/28-race_reach/87-lists_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" +// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/90-arrayloop2_racing.c b/tests/regression/28-race_reach/90-arrayloop2_racing.c index 4859ed5a95..184d79af89 100644 --- a/tests/regression/28-race_reach/90-arrayloop2_racing.c +++ b/tests/regression/28-race_reach/90-arrayloop2_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true +// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/91-arrayloop2_racefree.c b/tests/regression/28-race_reach/91-arrayloop2_racefree.c index 30ffa83e78..4461e78459 100644 --- a/tests/regression/28-race_reach/91-arrayloop2_racefree.c +++ b/tests/regression/28-race_reach/91-arrayloop2_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true +// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/92-evilcollapse_racing.c b/tests/regression/28-race_reach/92-evilcollapse_racing.c index af5bae0830..a33eb630f5 100644 --- a/tests/regression/28-race_reach/92-evilcollapse_racing.c +++ b/tests/regression/28-race_reach/92-evilcollapse_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true +// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/93-evilcollapse_racefree.c b/tests/regression/28-race_reach/93-evilcollapse_racefree.c index e4ca831199..dee7d67659 100644 --- a/tests/regression/28-race_reach/93-evilcollapse_racefree.c +++ b/tests/regression/28-race_reach/93-evilcollapse_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true +// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/94-alloc_region_racing.c b/tests/regression/28-race_reach/94-alloc_region_racing.c index 74333bcab4..f985a9d91e 100644 --- a/tests/regression/28-race_reach/94-alloc_region_racing.c +++ b/tests/regression/28-race_reach/94-alloc_region_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" --set exp.region-offsets true +// PARAM: --set ana.activated[+] "'region'" --set exp.region-offsets true --set lib.activated[+] sv-comp #include #include #include diff --git a/tests/regression/36-apron/15-globals-st.c b/tests/regression/36-apron/15-globals-st.c index 692d66f299..4c167ad742 100644 --- a/tests/regression/36-apron/15-globals-st.c +++ b/tests/regression/36-apron/15-globals-st.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --disable ana.int.interval +// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --disable ana.int.interval --set lib.activated[+] sv-comp extern int __VERIFIER_nondet_int(); #include diff --git a/tests/regression/41-stdlib/07-atexit.c b/tests/regression/41-stdlib/07-atexit.c new file mode 100644 index 0000000000..4551400175 --- /dev/null +++ b/tests/regression/41-stdlib/07-atexit.c @@ -0,0 +1,13 @@ +#include +#include + +void bye() +{ + __goblint_check(1); // reachable +} + +int main() +{ + atexit(bye); + return 0; +} diff --git a/tests/regression/41-stdlib/08-atexit-no-spawn.c b/tests/regression/41-stdlib/08-atexit-no-spawn.c new file mode 100644 index 0000000000..7f25f42183 --- /dev/null +++ b/tests/regression/41-stdlib/08-atexit-no-spawn.c @@ -0,0 +1,14 @@ +// PARAM: --disable sem.unknown_function.spawn +#include +#include + +void bye() +{ + __goblint_check(0); // NOWARN (unreachable) +} + +int main() +{ + atexit(bye); + return 0; +} diff --git a/tests/regression/56-witness/60-tm-inv-transfer-protection.c b/tests/regression/56-witness/60-tm-inv-transfer-protection.c index 3d5bcbc871..07260adbdd 100644 --- a/tests/regression/56-witness/60-tm-inv-transfer-protection.c +++ b/tests/regression/56-witness/60-tm-inv-transfer-protection.c @@ -35,12 +35,12 @@ int main(void) { __goblint_check(g >= 40); __goblint_check(g <= 41); // UNKNOWN (lacks expressivity) pthread_mutex_unlock(&C); - pthread_mutex_unlock(&C); - + pthread_mutex_unlock(&B); + pthread_mutex_lock(&C); __goblint_check(g >= 40); __goblint_check(g <= 42); // UNKNOWN (widen) pthread_mutex_unlock(&C); - + return 0; } diff --git a/tests/regression/56-witness/61-tm-inv-transfer-mine.c b/tests/regression/56-witness/61-tm-inv-transfer-mine.c index 8f912bc2d9..cd8301fb39 100644 --- a/tests/regression/56-witness/61-tm-inv-transfer-mine.c +++ b/tests/regression/56-witness/61-tm-inv-transfer-mine.c @@ -35,12 +35,12 @@ int main(void) { __goblint_check(g >= 40); __goblint_check(g <= 41); pthread_mutex_unlock(&C); - pthread_mutex_unlock(&C); - + pthread_mutex_unlock(&B); + pthread_mutex_lock(&C); - __goblint_check(g >= 40); + __goblint_check(g >= 40); // TODO why? __goblint_check(g <= 42); pthread_mutex_unlock(&C); - + return 0; } \ No newline at end of file diff --git a/tests/regression/56-witness/62-tm-inv-transfer-protection-witness.c b/tests/regression/56-witness/62-tm-inv-transfer-protection-witness.c index 7be5bcf53e..68aada7394 100644 --- a/tests/regression/56-witness/62-tm-inv-transfer-protection-witness.c +++ b/tests/regression/56-witness/62-tm-inv-transfer-protection-witness.c @@ -35,12 +35,12 @@ int main(void) { __goblint_check(g >= 40); __goblint_check(g <= 41); // UNKNOWN (lacks expressivity) pthread_mutex_unlock(&C); - pthread_mutex_unlock(&C); - + pthread_mutex_unlock(&B); + pthread_mutex_lock(&C); __goblint_check(g >= 40); __goblint_check(g <= 42); pthread_mutex_unlock(&C); - + return 0; } \ No newline at end of file diff --git a/tests/regression/66-interval-set-one/51-widen-sides.c b/tests/regression/66-interval-set-one/51-widen-sides.c index 72eb1396b1..b086baf026 100644 --- a/tests/regression/66-interval-set-one/51-widen-sides.c +++ b/tests/regression/66-interval-set-one/51-widen-sides.c @@ -3,13 +3,13 @@ int further(int n) { // Even sides-local can not save us here :( - __goblint_check(n <= 1); //TODO + __goblint_check(n <= 2); //TODO } int fun(int n, const char* arg) { // Fails with solvers.td3.side_widen sides, needs sides-local - __goblint_check(n <= 1); + __goblint_check(n <= 2); further(n); } @@ -26,5 +26,5 @@ int main() { doIt("two"); // In the setting with solvers.td3.side_widen sides, widening happens and the bound is lost - fun(1, "org"); + fun(2, "org"); } diff --git a/tests/regression/74-use_after_free/04-function-call-uaf.c b/tests/regression/74-use_after_free/04-function-call-uaf.c index f83f9966b4..d110db9edc 100644 --- a/tests/regression/74-use_after_free/04-function-call-uaf.c +++ b/tests/regression/74-use_after_free/04-function-call-uaf.c @@ -17,7 +17,8 @@ int main() { free(ptr1); free(ptr2); - f(ptr1, ptr2, ptr3); //WARN + // No deref happening in the function call, hence nothing to warn about + f(ptr1, ptr2, ptr3); //NOWARN free(ptr3); //WARN diff --git a/tests/regression/74-use_after_free/06-uaf-struct.c b/tests/regression/74-use_after_free/06-uaf-struct.c index 02c4f3e77a..fa3ffc7b56 100644 --- a/tests/regression/74-use_after_free/06-uaf-struct.c +++ b/tests/regression/74-use_after_free/06-uaf-struct.c @@ -17,12 +17,15 @@ int main(int argc, char **argv) { char line[128]; while (1) { + // printf() is considered an implicit deref => need to warn here printf("[ auth = %p, service = %p ]\n", auth, service); //WARN if (fgets(line, sizeof(line), stdin) == NULL) break; if (strncmp(line, "auth ", 5) == 0) { - auth = malloc(sizeof(auth)); //WARN + // No deref happening in the line below => no need to warn + auth = malloc(sizeof(auth)); //NOWARN + // memset() is considered an implicit deref => need to warn memset(auth, 0, sizeof(auth)); //WARN if (strlen(line + 5) < 31) { strcpy(auth->name, line + 5); //WARN diff --git a/tests/regression/74-use_after_free/09-juliet-uaf.c b/tests/regression/74-use_after_free/09-juliet-uaf.c index 5a5bf3ee32..e1a88508a6 100644 --- a/tests/regression/74-use_after_free/09-juliet-uaf.c +++ b/tests/regression/74-use_after_free/09-juliet-uaf.c @@ -21,7 +21,8 @@ static char * helperBad(char * aString) reversedString[i] = '\0'; free(reversedString); - return reversedString; // WARN (Use After Free (CWE-416)) + // No need to warn in the line below, as there's no dereferencing happening + return reversedString; // NOWARN } else { @@ -67,8 +68,10 @@ void CWE416_Use_After_Free__return_freed_ptr_08_bad() if(staticReturnsTrue()) { { - char * reversedString = helperBad("BadSink"); // WARN (Use After Free (CWE-416)) - printf("%s\n", reversedString); // WARN (Use After Free (CWE-416)) + // No need to warn in the line below, since there's no dereferencing of the freed memory + char * reversedString = helperBad("BadSink"); // NOWARN + // printf() is considered an implicit deref => need to warn here + printf("%s\n", reversedString); // WARN } } } diff --git a/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c b/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c index 3ed540b53d..cc6539eff2 100644 --- a/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c +++ b/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c @@ -27,12 +27,14 @@ int main(int argc, char const *argv[]) { my_free2(p); *(p + 42) = 'c'; //WARN + // printf() is considered an implicit deref => need to warn printf("%s", p); //WARN - char *p2 = p; //WARN - - my_free2(p); //WARN - my_free2(p2); //WARN + // No dereferencing happening in the lines below => no need to warn for an invalid-deref + // Also no need to warn for an invalid-free, as the call to free is within these functions and they're not the "free" function itself + char *p2 = p; //NOWARN + my_free2(p); //NOWARN + my_free2(p2); //NOWARN return 0; } diff --git a/tests/regression/74-use_after_free/12-multi-threaded-uaf.c b/tests/regression/74-use_after_free/12-multi-threaded-uaf.c index 0c647eff76..f6d11ae098 100644 --- a/tests/regression/74-use_after_free/12-multi-threaded-uaf.c +++ b/tests/regression/74-use_after_free/12-multi-threaded-uaf.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.activated[+] useAfterFree +//PARAM: --set ana.activated[+] useAfterFree --set ana.activated[+] threadJoins #include #include #include diff --git a/tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c b/tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c new file mode 100644 index 0000000000..2ce291f9d1 --- /dev/null +++ b/tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c @@ -0,0 +1,33 @@ +//PARAM: --set ana.activated[+] useAfterFree --set ana.activated[+] threadJoins +#include +#include +#include + +int* gptr; + +// Mutex to ensure we don't get race warnings, but the UAF warnings we actually care about +pthread_mutex_t mtx = PTHREAD_MUTEX_INITIALIZER; + +void *t_use(void* p) { + pthread_mutex_lock(&mtx); + *gptr = 0; //NOWARN + pthread_mutex_unlock(&mtx); +} + +int main() { + gptr = malloc(sizeof(int)); + *gptr = 42; + + pthread_t using_thread; + pthread_create(&using_thread, NULL, t_use, NULL); + + // Join using_thread before freeing gptr in the main thread + pthread_join(using_thread, NULL); + + pthread_mutex_lock(&mtx); + *gptr = 43; //NOWARN + free(gptr); //NOWARN + pthread_mutex_unlock(&mtx); + + return 0; +} \ No newline at end of file diff --git a/tests/regression/74-use_after_free/14-alloca-uaf.c b/tests/regression/74-use_after_free/14-alloca-uaf.c new file mode 100644 index 0000000000..3dc494cb09 --- /dev/null +++ b/tests/regression/74-use_after_free/14-alloca-uaf.c @@ -0,0 +1,16 @@ +//PARAM: --set ana.activated[+] useAfterFree +#include +#include + +int *f() { + int *c = alloca(sizeof(int)); + return c; +} + +int main(int argc, char const *argv[]) { + int *ps = alloca(sizeof(int)); + int *c = f(); + int a = *ps; //NOWARN + int b = *c; //WARN + return 0; +} diff --git a/tests/regression/75-invalid_dealloc/09-juliet-invalid-dealloc-alloca.c b/tests/regression/75-invalid_dealloc/09-juliet-invalid-dealloc-alloca.c new file mode 100644 index 0000000000..9a84d1e49a --- /dev/null +++ b/tests/regression/75-invalid_dealloc/09-juliet-invalid-dealloc-alloca.c @@ -0,0 +1,75 @@ +#include +#include + +typedef struct twoIntsStruct { + int intOne ; + int intTwo ; +} twoIntsStruct; + +void CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54_bad(void) { + twoIntsStruct *data; + data = (twoIntsStruct *)0; + { + twoIntsStruct *dataBuffer = __builtin_alloca(800UL); + { + size_t i; + i = 0UL; + + goto ldv_3204; + ldv_3203: + ; + + (dataBuffer + i)->intOne = 1; + (dataBuffer + i)->intTwo = 1; + + i += 1UL; + ldv_3204: + ; + + if (i <= 99UL) + goto ldv_3203; + else + goto ldv_3205; + ldv_3205: + ; + } + + data = dataBuffer; + } + + CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54b_badSink(data); + return; +} + +void CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54b_badSink(twoIntsStruct *data) { + CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54c_badSink(data); + return; +} + +void CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54c_badSink(twoIntsStruct *data) { + CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54d_badSink(data); + return; +} + +void CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54d_badSink(twoIntsStruct *data) { + CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54e_badSink(data); + return; +} + +void CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54e_badSink(twoIntsStruct *data) { + free((void *)data); //WARN + return; +} + +int main(int argc, char **argv) { + int __retres; + { + CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54_bad(); + __retres = 0; + goto return_label; + } + + __retres = 0; + return_label: + return __retres; +} diff --git a/tests/regression/77-mem-oob/01-oob-heap-simple.c b/tests/regression/77-mem-oob/01-oob-heap-simple.c new file mode 100644 index 0000000000..10c7864184 --- /dev/null +++ b/tests/regression/77-mem-oob/01-oob-heap-simple.c @@ -0,0 +1,14 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include + +int main(int argc, char const *argv[]) { + char *ptr = malloc(5 * sizeof(char)); + + *ptr = 'a';//NOWARN + *(ptr + 1) = 'b';//NOWARN + *(ptr + 10) = 'c';//WARN + + free(ptr); + + return 0; +} diff --git a/tests/regression/77-mem-oob/02-oob-stack-simple.c b/tests/regression/77-mem-oob/02-oob-stack-simple.c new file mode 100644 index 0000000000..8d022feca4 --- /dev/null +++ b/tests/regression/77-mem-oob/02-oob-stack-simple.c @@ -0,0 +1,12 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include + +int main(int argc, char const *argv[]) { + int i = 42; + int *ptr = &i; + + *ptr = 5;//NOWARN + *(ptr + 10) = 55;//WARN + + return 0; +} diff --git a/tests/regression/77-mem-oob/03-oob-loop.c b/tests/regression/77-mem-oob/03-oob-loop.c new file mode 100644 index 0000000000..4f637d487e --- /dev/null +++ b/tests/regression/77-mem-oob/03-oob-loop.c @@ -0,0 +1,16 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --set exp.unrolling-factor 10 --enable ana.int.interval +#include +#include + +int main(int argc, char const *argv[]) { + char *ptr = malloc(5 * sizeof(char)); + + for (int i = 0; i < 10; i++) { + ptr++; + } + + printf("%s", *ptr); //WARN + free(ptr); //WARN + + return 0; +} diff --git a/tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c b/tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c new file mode 100644 index 0000000000..5046a00664 --- /dev/null +++ b/tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c @@ -0,0 +1,18 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include +#include + +int main(int argc, char const *argv[]) { + char *ptr = malloc(5 * sizeof(char)); + + ptr++;//NOWARN + printf("%s", *ptr);//NOWARN + ptr = ptr + 5;//NOWARN + printf("%s", *ptr);//WARN + *(ptr + 1) = 'b';//WARN + *(ptr + 10) = 'c';//WARN + + free(ptr); + + return 0; +} diff --git a/tests/regression/77-mem-oob/05-oob-implicit-deref.c b/tests/regression/77-mem-oob/05-oob-implicit-deref.c new file mode 100644 index 0000000000..8bec6a72e0 --- /dev/null +++ b/tests/regression/77-mem-oob/05-oob-implicit-deref.c @@ -0,0 +1,23 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info +/* + Note: the "--disable warn.info" above is a temporary workaround, + since the GitHub CI seems to be considering Info messages as violations of NOWARN (cf. https://github.com/goblint/analyzer/issues/1151) +*/ +#include +#include +#include + +int main(int argc, char const *argv[]) { + int *ptr = malloc(4 * sizeof(int)); + + // Both lines below are considered derefs => no need to warn, since ptr is pointing within its bounds + memset(ptr, 0, 4 * sizeof(int)); //NOWARN + printf("%p", (void *) ptr); //NOWARN + ptr = ptr + 10; // ptr no longer points within its allocated bounds + + // Each of both lines below should now receive a WARN + memset(ptr, 0, 4 * sizeof(int)); //WARN + printf("%p", (void *) ptr); //WARN + + return 0; +} diff --git a/tests/regression/77-mem-oob/06-memset-oob.c b/tests/regression/77-mem-oob/06-memset-oob.c new file mode 100644 index 0000000000..931f7eaa8c --- /dev/null +++ b/tests/regression/77-mem-oob/06-memset-oob.c @@ -0,0 +1,54 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info +// TODO: The "--disable warn.info" part is a temporary fix and needs to be removed once the MacOS CI job is fixed +#include +#include +#include + +typedef struct s { + int a; + char b; +} s; + +int main(int argc, char const *argv[]) { + int *a = malloc(10 * sizeof(int)); //Size is 40 bytes, assuming a 4-byte int + + memset(a, 0, 40); //NOWARN + memset(a, 0, 10 * sizeof(int)); //NOWARN + memset(a, 0, 41); //WARN + memset(a, 0, 40000000); //WARN + + int d; + + if (argc == 15) { + int c = 55; + a = &c; + memset(a, 0, argv[5]); //WARN + } else if (argv[2] == 2) { + a = &d; + } + + memset(a, 0, 40); //WARN + + int input; + scanf("%d", &input); + memset(a, 0, input); //WARN + + + + int *b = malloc(15 * sizeof(int)); //Size is 60 bytes, assuming a 4-byte int + memset(b, 0, 60); //NOWARN + b += 1; + memset(b, 0, 60); //WARN + + + + s *s_ptr = malloc(sizeof(s)); + memset(s_ptr, 0, sizeof(s)); //NOWARN + memset(s_ptr->a, 0, sizeof(s)); //WARN + memset(s_ptr->b, 0, sizeof(s)); //WARN + + s_ptr = s_ptr->a; + memset(s_ptr, 0, sizeof(s)); //WARN + + return 0; +} diff --git a/tests/regression/77-mem-oob/07-memcpy-oob.c b/tests/regression/77-mem-oob/07-memcpy-oob.c new file mode 100644 index 0000000000..012f92996e --- /dev/null +++ b/tests/regression/77-mem-oob/07-memcpy-oob.c @@ -0,0 +1,53 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info +// TODO: The "--disable warn.info" part is a temporary fix and needs to be removed once the MacOS CI job is fixed +#include +#include + +typedef struct s { + int a; + char b; +} s; + +int main(int argc, char const *argv[]) { + int *a = malloc(10 * sizeof(int)); //Size is 40 bytes, assuming a 4-byte int + int *b = malloc(15 * sizeof(int)); //Size is 60 bytes, assuming a 4-byte int + + memcpy(a, b, 40); //NOWARN + memcpy(a, b, 10 * sizeof(int)); //NOWARN + memcpy(a, b, 41); //WARN + memcpy(a, b, 40000000); //WARN + memcpy(a, b, 15 * sizeof(int)); //WARN + + int d; + + if (*argv == 42) { + a = &d; + } else if (*(argv + 5)) { + int random = rand(); + a = &random; + memcpy(a, b, 40); //WARN + } + + memcpy(a, b, 40); //WARN + memcpy(a, b, sizeof(a)); //WARN + + memcpy(b, a, 60); //NOWARN + b += 1; + memcpy(b, a, 60); //WARN + + + s *s_ptr = malloc(sizeof(s)); + memcpy(s_ptr, a, sizeof(s)); //NOWARN + memcpy(s_ptr->a, 0, sizeof(s)); //WARN + memcpy(s_ptr->b, 0, sizeof(s)); //WARN + + memcpy(s_ptr, a, 40); //WARN + memcpy(s_ptr, a, 60); //WARN + memcpy(s_ptr, b, 40); //WARN + memcpy(s_ptr, b, 60); //WARN + + s_ptr = s_ptr->b; + memcpy(s_ptr, a, sizeof(s)); //WARN + + return 0; +} diff --git a/tests/regression/77-mem-oob/08-memset-memcpy-array.c b/tests/regression/77-mem-oob/08-memset-memcpy-array.c new file mode 100644 index 0000000000..f231ba2dc4 --- /dev/null +++ b/tests/regression/77-mem-oob/08-memset-memcpy-array.c @@ -0,0 +1,43 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info +// TODO: The "--disable warn.info" part is a temporary fix and needs to be removed once the MacOS CI job is fixed +#include +#include + +int main(int argc, char const *argv[]) { + int arr[42]; // Size should be 168 bytes (with 4 byte ints) + int *b = arr; + + + memset(b, 0, 168); //NOWARN + memset(b, 0, sizeof(arr)); //NOWARN + memset(b, 0, 169); //WARN + memset(b, 0, sizeof(arr) + 1); //WARN + + int *c = malloc(sizeof(arr)); // Size should be 168 bytes (with 4 byte ints) + memcpy(b, c, 168); //NOWARN + memcpy(b, c, sizeof(arr)); //NOWARN + memcpy(b, c, 169); //WARN + memcpy(b, c, sizeof(arr) + 1); //WARN + + int d; + + if (*argv == 42) { + b = &d; + memset(b, 0, 168); //WARN + memcpy(b, c, 168); //WARN + } else if (*(argv + 5)) { + int random = rand(); + b = &random; + memset(b, 0, 168); //WARN + memcpy(b, c, 168); //WARN + } + + memset(b, 0, sizeof(arr)); //WARN + memcpy(b, c, sizeof(arr)); //WARN + memset(b, 0, sizeof(int)); //NOWARN + memcpy(b, c, sizeof(int)); //NOWARN + memset(b, 0, sizeof(int) + 1); //WARN + memcpy(b, c, sizeof(int) + 1); //WARN + + return 0; +} diff --git a/tests/regression/77-mem-oob/09-memset-memcpy-addr-offs.c b/tests/regression/77-mem-oob/09-memset-memcpy-addr-offs.c new file mode 100644 index 0000000000..725024946e --- /dev/null +++ b/tests/regression/77-mem-oob/09-memset-memcpy-addr-offs.c @@ -0,0 +1,20 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info +// TODO: The "--disable warn.info" part is a temporary fix and needs to be removed once the MacOS CI job is fixed +#include +#include + +int main(int argc, char const *argv[]) { + int *a = malloc(10 * sizeof(int)); //Size is 40 bytes, assuming a 4-byte int + int *b = malloc(15 * sizeof(int)); //Size is 60 bytes, assuming a 4-byte int + + memset(a, 0, 40); //NOWARN + memcpy(a, b, 40); //NOWARN + + a += 3; + + memset(a, 0, 40); //WARN + memcpy(a, b, 40); //WARN + + memset(a, 0, 37); //NOWARN + memcpy(a, b, 37); //NOWARN +} \ No newline at end of file diff --git a/tests/sv-comp/valid-memsafety.prp b/tests/sv-comp/valid-memsafety.prp new file mode 100644 index 0000000000..06a87f5a37 --- /dev/null +++ b/tests/sv-comp/valid-memsafety.prp @@ -0,0 +1,4 @@ +CHECK( init(main()), LTL(G valid-free) ) +CHECK( init(main()), LTL(G valid-deref) ) +CHECK( init(main()), LTL(G valid-memtrack) ) +