From 8a79c04a0e07c5016e5b9942920f04a4ec1f1c72 Mon Sep 17 00:00:00 2001 From: Nathan Schmidt Date: Tue, 1 Aug 2023 15:24:20 +0200 Subject: [PATCH] Updated join and strlen effect, first draft for special in analysis --- .../apron/relationalStringAnalyses.apron.ml | 40 ++++++++---- .../apron/relationalStringDomains.apron.ml | 63 +++++++++++++------ 2 files changed, 74 insertions(+), 29 deletions(-) diff --git a/src/analyses/apron/relationalStringAnalyses.apron.ml b/src/analyses/apron/relationalStringAnalyses.apron.ml index 8b96398b2b..8506e95967 100644 --- a/src/analyses/apron/relationalStringAnalyses.apron.ml +++ b/src/analyses/apron/relationalStringAnalyses.apron.ml @@ -6,6 +6,8 @@ module PCU = RelationPrecCompareUtil.DummyUtil module RA = RelationAnalysis.SpecFunctor (Priv) (RSD) (PCU) +module BatS = BatSet.Make (Mval.Exp) + module RelationalSubstringAnalysis = struct include RelationAnalysis @@ -24,22 +26,38 @@ struct let get_spec (): (module MCPSpec) = Lazy.force spec_module - let after_config () = - let module Spec = (val get_spec ()) in - MCP.register_analysis (module Spec : MCPSpec); - GobConfig.set_string "ana.path_sens[+]" (Spec.name ()) - - let _ = - AfterConfig.register after_config + let strpcy_strcat_edge ctx (st:(RSD.t, Priv(RSD).D.t) RelationDomain.relcomponents_t) dest src n str_fun = + let ask = Analyses.ask_of_ctx ctx in + let dest' = Queries.LS.elements (ask.f (MayPointTo dest)) + |> List.map (fun (v, _) -> v) in + let src' = Queries.LS.elements (ask.f (MayPointTo src)) + |> List.map (fun (v, _) -> v) in + let prod = BatList.cartesian_product dest' src' in + let t = begin match n with + (* strcpy or strcat *) + | None -> + List.map (fun (v1, v2) -> str_fun ctx st.rel v1 v2 None) prod + |> List.fold_left RSD.join (RSD.bot ()) + (* strncpy or strncat *) + | Some n -> + let n = ask.f (EvalInt n) in + begin match Queries.ID.to_int n with + | Some n -> + List.map (fun (v1, v2) -> str_fun ctx st.rel v1 v2 (Some (Z.to_int n))) prod + |> List.fold_left RSD.join (RSD.bot ()) + | _ -> + List.map RSD.varinfo_to_var dest' + |> RSD.forget_vars st.rel + end + end in + {st with rel = t} let special ctx r f args = - let ask = Analyses.ask_of_ctx ctx in let st = ctx.local in let desc = LibraryFunctions.find f in match desc.special args, f.vname with - | Strcpy { dest; src; n }, _ -> failwith "TODO" (* TODO: how to exp -> varinfo? *) - (* RSD.string_copy ctx st dest src n *) - | Strcat { dest; src; n }, _ -> failwith "TODO" + | Strcpy { dest; src; n }, _ -> strpcy_strcat_edge ctx st dest src n RSD.string_copy + | Strcat { dest; src; n }, _ -> strpcy_strcat_edge ctx st dest src n RSD.string_concat | Strlen s, _ -> failwith "TODO" | Strstr { haystack; needle }, _ -> failwith "TODO" | Strcmp { s1; s2; n }, _ -> failwith "TODO" diff --git a/src/cdomains/apron/relationalStringDomains.apron.ml b/src/cdomains/apron/relationalStringDomains.apron.ml index c42bfddb99..d0740b6734 100644 --- a/src/cdomains/apron/relationalStringDomains.apron.ml +++ b/src/cdomains/apron/relationalStringDomains.apron.ml @@ -8,10 +8,14 @@ module ID = IntDomain.IntDomTuple module Var = SharedFunctions.PrintableVar module V = RelationDomain.V (Var) +module SetS = Set.Make(Var) + module type StringRelationDomain = sig include RelationDomain.RD + val varinfo_to_var: varinfo -> var + val string_copy: ('a, 'b, 'c, 'd) ctx -> t -> varinfo -> varinfo -> int option -> t val string_concat: ('a, 'b, 'c, 'd) ctx -> t -> varinfo -> varinfo -> int option -> t val to_string_length: ('a, 'b, 'c, 'd) ctx -> t -> varinfo -> ID.t @@ -64,12 +68,6 @@ struct add_all_relations s' in add_all_relations s - let varinfo_to_var (v:varinfo) = - if v.vglob then - V.global v - else - V.local v - let vid_to_id ik = function (* TODO: okay? *) | `Lifted i -> i | _ -> ID.top_of ik @@ -82,7 +80,7 @@ struct let leq t1 t2 = S.leq t1.r_set t2.r_set - let join t1 t2 = {r_set = transitive_closure (S.join t1.r_set t2.r_set); env = Environment.lce t1.env t2.env} + let join t1 t2 = {r_set = S.join t1.r_set t2.r_set; env = Environment.lce t1.env t2.env} let meet t1 t2 = {r_set = transitive_closure (S.meet t1.r_set t2.r_set); env = Environment.lce t1.env t2.env} let widen = join let narrow = meet @@ -127,6 +125,12 @@ struct let invariant t = [] + let varinfo_to_var (v:varinfo) = + if v.vglob then + V.global v + else + V.local v + (* string functions *) let string_copy ctx t dest src n = let dest' = varinfo_to_var dest in @@ -197,20 +201,43 @@ struct let to_string_length ctx t s = let s' = varinfo_to_var s in - S.fold (fun (x, y) acc -> - (* if s <= y and y <= s, strlen(s) = strlen(y) *) + (* collect all strings = s *) + let t_eq = S.fold (fun (x, y) acc -> if Var.equal x s' && S.mem (y, s') t.r_set then - match V.to_cil_varinfo y with - | Some y -> vid_to_id !Cil.kindOfSizeOf (ctx.ask (VarStringLength y)) - | None -> acc - (* if s <= y, strlen(s) <= strlen(y) *) - else if Var.equal x s' then - match V.to_cil_varinfo y with - | Some y -> ID.meet acc (ID.le (ID.top_of !Cil.kindOfSizeOf) (vid_to_id !Cil.kindOfSizeOf (ctx.ask (VarStringLength y)))) (* TODO: does this work? *) - | None -> acc + SetS.add y acc + else + acc) + t.r_set SetS.empty in + (* collect all strings <= s *) + let t_leq = S.fold (fun (x, y) acc -> + if Var.equal x s' then + SetS.add y acc + else + acc) + t.r_set SetS.empty in + (* collect all strings >= s *) + let t_geq = S.fold (fun (x, y) acc -> + if Var.equal y s' then + SetS.add x acc else acc) - t.r_set (vid_to_id !Cil.kindOfSizeOf (ctx.ask (VarStringLength s))) + t.r_set SetS.empty in + + (* s = s' ==> strlen(s) = strlen(s') *) + let len_eq = SetS.fold (fun x acc -> match V.to_cil_varinfo x with + | Some x -> ID.meet (vid_to_id !Cil.kindOfSizeOf (ctx.ask (VarStringLength x))) acc + | None -> acc) + t_eq (vid_to_id !Cil.kindOfSizeOf (ctx.ask (VarStringLength s))) in + (* s <= s' ==> strlen(s) <= strlen(s') *) + let len_eq_leq = SetS.fold (fun x acc -> match V.to_cil_varinfo x with + | Some x -> ID.meet (ID.le (ID.top_of !Cil.kindOfSizeOf) (vid_to_id !Cil.kindOfSizeOf (ctx.ask (VarStringLength x)))) acc + | None -> acc) + t_leq len_eq in + (* s' <= s ==> strlen(s) >= strlen(s') *) + SetS.fold (fun x acc -> match V.to_cil_varinfo x with + | Some x -> ID.meet (ID.ge (ID.top_of !Cil.kindOfSizeOf) (vid_to_id !Cil.kindOfSizeOf (ctx.ask (VarStringLength x)))) acc + | None -> acc) + t_geq len_eq_leq (* returns is_maybe_null_ptr, is_surely_offset_0 *) let substring_extraction ctx t lval haystack needle =