Merge pull request #952 from FelixKrayer/taint

Taint analysis to improve the precision loss of partial contexts

Author: michael-schwarz

src/analyses/abortUnless.ml

@@ -46,7 +46,7 @@ struct
     in
     [false, candidate]
 
-  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t =
+  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
     if au && lval = None then (
       (* Assert happens after evaluation of call, so if variables in `arg` are assigned to, asserting might unsoundly yield bot *)
       (* See test 62/03 *)

src/analyses/accessAnalysis.ml

@@ -98,7 +98,7 @@ struct
   let enter ctx lv f args : (D.t * D.t) list =
     [(ctx.local,ctx.local)]
 
-  let combine ctx lv fexp f args fc al =
+  let combine ctx lv fexp f args fc al f_ask =
     access_one_top ctx Read false fexp;
     begin match lv with
       | None      -> ()

src/analyses/apron/relationAnalysis.apron.ml

@@ -350,7 +350,7 @@ struct
         st'
     end
 
-  let combine ctx r fe f args fc fun_st =
+  let combine ctx r fe f args fc fun_st (f_ask : Queries.ask) =
     let st = ctx.local in
     let reachable_from_args = List.fold (fun ls e -> Queries.LS.join ls (ctx.ask (ReachableFrom e))) (Queries.LS.empty ()) args in
     let fundec = Node.find_fundec ctx.node in
@@ -378,10 +378,14 @@ struct
     let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in
     if M.tracing then M.tracel "combine" "relation remove vars: %a\n" (docList (fun v -> Pretty.text (RD.Var.to_string v))) arg_vars;
     RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *)
+    let tainted = f_ask.f Queries.MayBeTainted in
+    let tainted_vars = TaintPartialContexts.conv_varset tainted in
     let new_rel = RD.keep_filter st.rel (fun var ->
         match RV.find_metadata var with
         | Some (Local _) when not (pass_to_callee fundec any_local_reachable var) -> true (* keep caller locals, provided they were not passed to the function *)
         | Some (Arg _) -> true (* keep caller args *)
+        | Some ((Local _ | Global _)) when not (RD.mem_var new_fun_rel var) -> false (* remove locals and globals, for which no record exists in the new_fun_apr *)
+        | Some ((Local v | Global v)) when not (TaintPartialContexts.VS.mem v tainted_vars) -> true (* keep locals and globals, which have not been touched by the call *)
         | _ -> false (* remove everything else (globals, global privs, reachable things from the caller) *)
       )
     in

src/analyses/assert.ml

@@ -27,7 +27,7 @@ struct
   let enter ctx (lval: lval option) (fd:fundec) (args:exp list) : (D.t * D.t) list =
     [ctx.local, ctx.local]
 
-  let combine ctx (lval:lval option) fexp (fd:fundec) (args:exp list) fc (au:D.t) : D.t =
+  let combine ctx (lval:lval option) fexp (fd:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
     au
 
   let assert_fn ctx e check refine =

src/analyses/base.ml

@@ -2247,7 +2247,36 @@ struct
     in
     if get_bool "sem.noreturn.dead_code" && Cil.hasAttribute "noreturn" f.vattr then raise Deadcode else st
 
-  let combine ctx (lval: lval option) fexp (f: fundec) (args: exp list) fc (after: D.t) : D.t =
+  let combine_st ctx (local_st : store) (fun_st : store) (tainted_lvs : Q.LS.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 = Lval.CilLval.to_lval (v,o) in
+        let address = eval_lv ask ctx.global st lval in
+        let lval_type = (AD.get_type address) in
+        if M.tracing then M.trace "taintPC" "updating %a; type: %a\n" Lval.CilLval.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
+
+  let combine ctx (lval: lval option) fexp (f: fundec) (args: exp list) fc (after: D.t) (f_ask: Q.ask) : D.t =
     let combine_one (st: D.t) (fun_st: D.t) =
       if M.tracing then M.tracel "combine" "%a\n%a\n" CPA.pretty st.cpa CPA.pretty fun_st.cpa;
       (* This function does miscellaneous things, but the main task was to give the
@@ -2258,9 +2287,27 @@ struct
       let add_globals (st: store) (fun_st: store) =
         (* Remove the return value as this is dealt with separately. *)
         let cpa_noreturn = CPA.remove (return_varinfo ()) fun_st.cpa in
-        let cpa_local = CPA.filter (fun x _ -> not (is_global (Analyses.ask_of_ctx ctx) x)) st.cpa in
-        let cpa' = CPA.fold CPA.add cpa_noreturn cpa_local in (* add cpa_noreturn to cpa_local *)
-        { fun_st with cpa = cpa' }
+        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 base:\ncaller: %a\ncallee: %a\n" CPA.pretty st.cpa CPA.pretty fun_st.cpa;
+        begin if (Q.LS.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';
+          { fun_st with cpa = cpa' }
+        else
+          (* remove variables from caller cpa, that are global and not in the callee cpa *)
+          let cpa_caller = CPA.filter (fun x _ -> (not (is_global ask x)) || CPA.mem x fun_st.cpa) st.cpa in
+          (* add variables from callee that are not in caller yet *)
+          let cpa_new = CPA.filter (fun x _ -> not (CPA.mem x cpa_caller)) cpa_noreturn in
+          let cpa_caller' = CPA.fold CPA.add cpa_new cpa_caller in
+          (* 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 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 }
+        end
       in
       let return_var = return_var () in
       let return_val =
@@ -2271,7 +2318,7 @@ struct
       let nst = add_globals st fun_st in
 
       (* Projection to Precision of the Caller *)
-      let p = PrecisionUtil.int_precision_from_node ()in (* Since f is the fundec of the Callee we have to get the fundec of the current Node instead *)
+      let p = PrecisionUtil.int_precision_from_node () in (* Since f is the fundec of the Callee we have to get the fundec of the current Node instead *)
       let callerFundec = match !MyCFG.current_node with
         | Some n -> Node.find_fundec n
         | None -> failwith "callerfundec not found"

src/analyses/condVars.ml

@@ -36,6 +36,9 @@ module Domain = struct
   let only_locals d =
     let p v = not v.vglob in
     filter_vars p d
+  let only_untainted d tainted =
+    let p v = (not v.vglob) || not (TaintPartialContexts.VS.mem v tainted) in
+    filter_vars p d
   let only_global_exprs s = V.for_all (var_in_expr (fun v -> v.vglob)) s
   let rec get k d =
     if mem k d && V.cardinal (find k d) = 1 then
@@ -104,7 +107,7 @@ struct
     let save_expr lval expr =
       match mustPointTo ctx (AddrOf lval) with
       | Some clval ->
-        if M.tracing then M.tracel "condvars" "CondVars: saving %a = %a" Lval.CilLval.pretty clval d_exp expr;
+        if M.tracing then M.tracel "condvars" "CondVars: saving %a = %a\n" Lval.CilLval.pretty clval d_exp expr;
         D.add clval (D.V.singleton expr) d (* if lval must point to clval, add expr *)
       | None -> d
     in
@@ -136,13 +139,15 @@ struct
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     [ctx.local, D.bot ()]
 
-  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t =
+  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
     (* combine caller's state with globals from callee *)
     (* TODO (precision): globals with only global vars are kept, the rest is lost -> collect which globals are assigned to *)
     (* D.merge (fun k s1 s2 -> match s2 with Some ss2 when (fst k).vglob && D.only_global_exprs ss2 -> s2 | _ when (fst k).vglob -> None | _ -> s1) ctx.local au *)
-    D.only_locals ctx.local (* globals might have changed... *)
+    let tainted = TaintPartialContexts.conv_varset (f_ask.f Queries.MayBeTainted) in
+    D.only_untainted ctx.local tainted (* tainted globals might have changed... *)
 
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    (* TODO: shouldn't there be some kind of invalidadte, depending on the effect of the special function? *)
     ctx.local
 
   let startstate v = D.bot ()

src/analyses/expRelation.ml

@@ -99,7 +99,7 @@ struct
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     [ctx.local, ctx.local]
 
-  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t =
+  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
     au
 
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =

src/analyses/expsplit.ml

@@ -46,7 +46,7 @@ struct
   let return ctx (exp:exp option) (f:fundec) =
     emit_splits_ctx ctx
 
-  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc au =
+  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc au (f_ask: Queries.ask) =
     let d = D.join ctx.local au in
     emit_splits ctx d
 

src/analyses/extractPthread.ml

@@ -1057,14 +1057,7 @@ module Spec : Analyses.MCPSpec = struct
     [ (d_caller, d_callee) ]
 
 
-  let combine
-      ctx
-      (lval : lval option)
-      fexp
-      (f : fundec)
-      (args : exp list)
-      fc
-      (au : D.t) : D.t =
+  let combine ctx (lval : lval option) fexp (f : fundec) (args : exp list) fc (au : D.t) (f_ask: Queries.ask) : D.t =
     if D.any_is_bot ctx.local || D.any_is_bot au
     then ctx.local
     else

src/analyses/fileUse.ml

@@ -163,7 +163,7 @@ struct
       D.extend_value unclosed_var (mustOpen, mayOpen) m
     ) else m
 
-  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t =
+  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
     let m = ctx.local in
     (* pop the last location off the stack *)
     let m = D.edit_callstack List.tl m in (* TODO could it be problematic to keep this in the caller instead of callee domain? if we only add the stack for the callee in enter, then there would be no need to pop a location anymore... *)