Gamma domain

lib/analysis/dune

@@ -14,6 +14,7 @@
   lattice_collections
   wrapped_intervals
   known_bits
+  gamma_domain
   tnum_wint_reduced_product
   known_bits
   wp_dual

lib/analysis/gamma_domain.ml

@@ -0,0 +1,155 @@
+(* The forwards overappraximating gamma domain. It is assumed that the program is in ssa form. *)
+
+include Lang
+include Common
+include Intra_analysis
+include Lattice_collections
+
+module GammaSet = struct
+  include LatticeSet (struct
+    include Var
+
+    let show = name
+    let name = "variable"
+  end)
+
+  let name = "Gamma set"
+  let pp fmt v = Format.pp_print_string fmt (show v)
+end
+
+module Domain = struct
+  include MapState (GammaSet)
+
+  let name = "Gamma domain"
+
+  let init proc =
+    Procedure.formal_in_params proc
+    |> StringMap.values
+    |> Iter.append
+         ((Procedure.specification proc).captures_globs |> Iter.of_list)
+    |> Iter.map (fun v -> (v, GammaSet.singleton v))
+    |> Iter.fold (fun m (v, d) -> update v d m) bottom
+
+  let transfer_state m stmt =
+    let open Stmt in
+    let eval_expr e =
+      Expr.BasilExpr.free_vars_iter e
+      |> Iter.fold (fun s v' -> V.join (m v') s) V.bottom
+    in
+    match stmt with
+    | Instr_Assign a ->
+        Iter.of_list a |> Iter.map (fun (v, e) -> (v, eval_expr e))
+    | Instr_Assert _ -> Iter.empty
+    | Instr_Assume _ -> Iter.empty
+    | Instr_Load { lhs; rhs; addr = Scalar } -> Iter.singleton (lhs, m rhs)
+    | Instr_Store { lhs; value; addr = Scalar } ->
+        Iter.singleton (lhs, eval_expr value)
+    | Instr_Load { lhs; rhs } -> Iter.singleton (lhs, m rhs)
+    | Instr_Store { lhs; value } ->
+        Iter.singleton (lhs, V.join (m lhs) (eval_expr value))
+    (* could use IDE summaries, but that requires access to formal in params of caller *)
+    | Instr_Call { lhs } | Instr_IntrinCall { lhs } ->
+        StringMap.values lhs |> Iter.map (fun v -> (v, GammaSet.top))
+    (* need to globally go to top which the transfer_state api doesn't support *)
+    (*| Instr_IndirectCall c -> raise (Failure "unsupported")*)
+    | Instr_IndirectCall _ -> Iter.empty
+
+  let transfer m (stmt : Program.stmt) =
+    let open Stmt in
+    match stmt with
+    (* TODO calls can be more precise with modifies information (only send outputs + modifies to top) but this requires spec info *)
+    | Instr_Call _ | Instr_IntrinCall _ | Instr_IndirectCall _ -> top
+    | s ->
+        transfer_state (fun v -> read v m) s
+        |> Iter.fold (fun m (v, s) -> update v s m) m
+end
+
+module CFGAnalysis = Forwards (Domain)
+module DFGAnalysis = Dataflow_graph.AnalysisFwd (Domain)
+open Idessi
+
+(* TODO handle memory nicely *)
+module IDEDomain : IDESSIDomain = struct
+  let direction = `Forwards
+
+  module DL = struct
+    type t = Lambda | Label of Var.t
+    [@@deriving eq, ord, show { with_path = false }]
+
+    let show = function Lambda -> "L" | Label v -> Var.name v
+  end
+
+  module Value = GammaSet
+
+  let show_state s =
+    s
+    |> Iter.to_string ~sep:", " (fun (v, s) ->
+        Var.to_string v ^ "->" ^ GammaSet.show s)
+
+  type t = BottomEdge | IdEdge | TopEdge
+  [@@deriving eq, ord, show { with_path = false }]
+
+  let pp fmt v = Format.pp_print_string fmt (show v)
+  let identity = IdEdge
+  let bottom = BottomEdge
+  let top = TopEdge
+
+  let compose a b =
+    match a with IdEdge -> b | BottomEdge -> BottomEdge | TopEdge -> TopEdge
+
+  let join a b =
+    match (a, b) with
+    | BottomEdge, e | e, BottomEdge -> e
+    | TopEdge, _ | _, TopEdge -> TopEdge
+    | IdEdge, IdEdge -> IdEdge
+
+  let eval s = function
+    | BottomEdge -> Value.bottom
+    | IdEdge -> s
+    | TopEdge -> Value.top
+
+  let init_data (proc : Program.proc) =
+    Procedure.formal_in_params proc |> StringMap.values
+
+  type state_update = (DL.t * t) Iter.t
+
+  open DL
+
+  let transfer_call call params d =
+    match d with
+    | Lambda -> Iter.singleton (d, IdEdge)
+    | Label v ->
+        StringMap.to_iter call
+        |> Iter.filter (fun (_, e) ->
+            Expr.BasilExpr.free_vars e |> VarSet.mem v)
+        |> Iter.map (fun (s, _) -> (Label (StringMap.find s params), IdEdge))
+
+  let transfer stmt d =
+    let open Stmt in
+    match d with
+    | Lambda -> (
+        match stmt with
+        | Instr_Load l -> Iter.singleton (Label l.lhs, TopEdge)
+        | _ -> Iter.empty)
+    | Label v -> (
+        match stmt with
+        | Instr_Assign a ->
+            Iter.of_list a
+            |> Iter.flat_map (fun (v', e) ->
+                if VarSet.mem v (Expr.BasilExpr.free_vars e) then
+                  Iter.singleton (Label v', IdEdge)
+                else Iter.empty)
+        | _ -> Iter.empty)
+
+  let transfer_phi lhs rhs d =
+    match d with
+    | Lambda -> Iter.empty
+    | Label v -> Iter.singleton (Label lhs, IdEdge)
+
+  let init_p2 (proc : Program.proc) =
+    Procedure.formal_in_params proc
+    |> StringMap.values
+    |> Iter.map (fun v -> (v, Value.singleton v))
+end
+
+module IDEAnalysis = IDESSI (IDEDomain)

lib/analysis/ide.ml

@@ -99,7 +99,7 @@ module type IDEDomain = sig
   val compose : t -> t -> t
   (** the composite of edge functions *)
 
-  val eval : t -> Value.t -> Value.t
+  val eval : Value.t -> t -> Value.t
   (** evaluate an edge function *)
 
   val init_data : Var.t Iter.t -> Program.proc -> Data.t Iter.t
@@ -585,7 +585,7 @@ module IDE (D : IDEDomain) = struct
       updates
     |> Iter.fold
          (fun acc ((d1, d3), e) ->
-           let base = dldlget Lambda d3 summary in
+           let base = dldlget Lambda d3 acc in
            let m = DlMap.get_or d1 acc ~default:DlMap.empty in
            match d1 with
            | Label v when D.equal base (D.join e base) ->
@@ -654,7 +654,7 @@ module IDE (D : IDEDomain) = struct
             match d3 with
             | Label v ->
                 let st = Hashtbl.get_or states target ~default:DataMap.empty in
-                let fd = D.eval e21 md in
+                let fd = D.eval md e21 in
                 let y = DataMap.get_or v st ~default:D.Value.bottom in
                 let j = D.Value.join y fd in
                 if not (D.Value.equal j y) then (
@@ -750,7 +750,7 @@ module IDE (D : IDEDomain) = struct
                 match d2 with
                 | Label v ->
                     let st = get_st l in
-                    let y = D.eval e x in
+                    let y = D.eval x e in
                     Hashtbl.replace states l (join_state_with st v y)
                 | _ -> ())));
     states

lib/analysis/ide_live.ml

@@ -70,7 +70,7 @@ module IDELiveCommon = struct
     | IdEdge, ConstEdge false -> IdEdge
     | IdEdge, IdEdge -> IdEdge
 
-  let eval f v = match f with IdEdge -> v | ConstEdge c -> c
+  let eval v f = match f with IdEdge -> v | ConstEdge v -> v
 end
 
 module IDELive = struct

lib/analysis/idessi.ml

@@ -42,7 +42,7 @@ module type IDESSIDomain = sig
   val compose : t -> t -> t
   (** the composite of edge functions *)
 
-  val eval : t -> Value.t -> Value.t
+  val eval : Value.t -> t -> Value.t
   (** evaluate an edge function *)
 
   type state_update = (DL.t * t) Iter.t
@@ -260,9 +260,9 @@ module IDESSI (D : IDESSIDomain) = struct
                | Label v ->
                    let x =
                      match d with
-                     | Lambda -> D.eval ef D.Value.bottom
+                     | Lambda -> D.eval D.Value.bottom ef
                      | Label v' ->
-                         D.eval ef (VarMap.get_or v' m ~default:D.Value.bottom)
+                         D.eval (VarMap.get_or v' m ~default:D.Value.bottom) ef
                    in
                    let j =
                      D.Value.join (VarMap.get_or v m ~default:D.Value.bottom) x

lib/analysis/linear_const.ml

@@ -156,7 +156,7 @@ module LinearDomain = struct
     | Join (a, b, c), Join (d, e, Bot) ->
         Join (Bitvec.mul a d, Bitvec.add (Bitvec.mul a e) b, c)
 
-  let eval f x =
+  let eval x f =
     match (f, x) with
     | BotEdge, _ -> Value.Bot
     | IdEdge, x -> x

lib/passes.ml

@@ -121,6 +121,13 @@ module PassManager = struct
          control flow graph and prints results";
     }
 
+  let demo_dfg_gamma =
+    {
+      name = "demo-dfg-gamma-analysis";
+      apply = DFGAnalysis (module Analysis.Gamma_domain.DFGAnalysis);
+      doc = "Runs a gamma analysis on a data flow graph and prints results";
+    }
+
   let remove_unused =
     {
       name = "remove-unused-decls";
@@ -225,6 +232,7 @@ module PassManager = struct
       demo_ival_wint_dfg;
       cfg_wrapped_int;
       cfg_tnum_wint_reduced;
+      demo_dfg_gamma;
       sparams;
       read_uninit false;
       read_uninit true;