Updated join and strlen effect, first draft for special in analysis

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"

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 =