Skip to content

Commit

Permalink
Use MayBeTaintedA in base
Browse files Browse the repository at this point in the history
  • Loading branch information
@karoliineh
karoliineh committed Aug 29, 2023
1 parent 8e42121 commit 392834b
Showing 1 changed file with 38 additions and 31 deletions.
69 changes: 38 additions & 31 deletions src/analyses/base.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2386,34 +2386,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) =
Expand All @@ -2427,10 +2431,10 @@ struct
(* Remove the return value as this is dealt with separately. *)
let cpa_noreturn = CPA.remove (return_varinfo ()) fun_st.cpa in
let ask = (Analyses.ask_of_ctx ctx) in
let 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;
let tainted = f_ask.f Q.MayBeTaintedA in
if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a\n" f.svar.vname AD.pretty tainted;
if M.tracing then M.trace "taintPC" "combine base:\ncaller: %a\ncallee: %a\n" CPA.pretty st.cpa CPA.pretty fun_st.cpa;
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';
Expand All @@ -2445,7 +2449,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 }
Expand Down

0 comments on commit 392834b

Please sign in to comment.