Skip to content

Commit

Permalink
Support for threadenter for unknown function
Browse files Browse the repository at this point in the history
  • Loading branch information
michael-schwarz committed Dec 17, 2024
1 parent 406ad22 commit 563a5b1
Showing 1 changed file with 38 additions and 34 deletions.
72 changes: 38 additions & 34 deletions src/analyses/apron/relationAnalysis.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -512,6 +512,36 @@ struct
if RD.is_bot_env res then raise Deadcode;
{st with rel = res}


let special_unknown_invalidate ctx f args =
(* No warning here, base already prodcues the appropriate warnings *)
let desc = LibraryFunctions.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
let deep_addrs =
if List.mem LibraryDesc.InvalidateGlobals desc.attrs then (
foldGlobals !Cilfacade.current_file (fun acc global ->
match global with
| GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
mkAddrOf (Var vi, NoOffset) :: acc
(* TODO: what about GVarDecl? *)
| _ -> acc
) deep_addrs
)
else
deep_addrs
in
let lvallist e =
match ctx.ask (Queries.MayPointTo e) with
| ad when Queries.AD.is_top ad -> []
| ad ->
Queries.AD.to_mval ad
|> List.map ValueDomain.Addr.Mval.to_cil
in
let st' = forget_reachable ctx ctx.local deep_addrs in
let shallow_lvals = List.concat_map lvallist shallow_addrs in
List.fold_left (invalidate_one (Analyses.ask_of_ctx ctx) ctx) st' shallow_lvals

let special ctx r f args =
let ask = Analyses.ask_of_ctx ctx in
let st = ctx.local in
Expand Down Expand Up @@ -547,31 +577,7 @@ struct
assert_fn {ctx with local = st} (BinOp (Ge, Lval lv, zero, intType)) true
| None -> st)
| _, _ ->
let lvallist e =
match ask.f (Queries.MayPointTo e) with
| ad when Queries.AD.is_top ad -> []
| ad ->
Queries.AD.to_mval ad
|> List.map ValueDomain.Addr.Mval.to_cil
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
let deep_addrs =
if List.mem LibraryDesc.InvalidateGlobals desc.attrs then (
foldGlobals !Cilfacade.current_file (fun acc global ->
match global with
| GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
mkAddrOf (Var vi, NoOffset) :: acc
(* TODO: what about GVarDecl? *)
| _ -> acc
) deep_addrs
)
else
deep_addrs
in
let st' = forget_reachable ctx st deep_addrs in
let shallow_lvals = List.concat_map lvallist shallow_addrs in
let st' = List.fold_left (invalidate_one ask ctx) st' shallow_lvals in
let st' = special_unknown_invalidate ctx f args in
(* invalidate lval if present *)
match r with
| Some lv -> invalidate_one ask ctx st' lv
Expand Down Expand Up @@ -673,21 +679,19 @@ struct

let threadenter ctx ~multiple lval f args =
let st = ctx.local in
(* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread.
Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published...
sync `Thread doesn't help us here, it's not specific to entering multithreaded mode.
EnterMultithreaded events only execute after threadenter and threadspawn. *)
if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st);
match Cilfacade.find_varinfo_fundec f with
| fd ->
(* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread.
Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published...
sync `Thread doesn't help us here, it's not specific to entering multithreaded mode.
EnterMultithreaded events only execute after threadenter and threadspawn. *)
if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st);
let st' = Priv.threadenter (Analyses.ask_of_ctx ctx) ctx.global st in
let new_rel = make_callee_rel ~thread:true ctx fd args in
[{st' with rel = new_rel}]
| exception Not_found ->
(* Unknown functions *)
(* TODO: do something like base? *)
failwith "relation.threadenter: unknown function"
[special_unknown_invalidate ctx f args]

let threadspawn ctx ~multiple lval f args fctx =
ctx.local
Expand Down

0 comments on commit 563a5b1

Please sign in to comment.