Expr/stmt eval that provides types

.github/workflows/test.yml

@@ -3,8 +3,10 @@ name: build and test
 on:
   pull_request:
   merge_group:
-  push:
   workflow_dispatch:
+  push:
+    branches:
+      - main
 
 permissions: read-all
 

.ocamlformat-ignore

@@ -1 +1 @@
-lib/fe/**
+lib/fe/**

lib/analysis/dataflow_graph.ml

@@ -309,7 +309,7 @@ end
 
 (** Simple way to get started with forwards analysis on def-use graph *)
 module EasyForwardAnalysisPack (V : sig
-  include Lattice_types.ValueAbstraction with module E = Expr.BasilExpr
+  include Lattice_types.TypedValueAbstraction with module E = Expr.BasilExpr
 
   val top : t
 end) =

lib/analysis/defuse_bool.ml

@@ -115,12 +115,24 @@ module IsZeroValueAbstraction = struct
         else Top
 end
 
-module IsZeroValueAbstractionBasil = struct
+module IsZeroValueAbstractionUntyped = struct
   include IsZeroValueAbstraction
+  module E = Lang.Expr.BasilExpr
 
-  let top = IsZeroLattice.Top
+  (*let eval_const op (rt : ty) = eval_const op
+  let eval_unop op arg rt = eval_unop op (fst arg)
+  let eval_binop op arg1 arg2 rt = eval_binop op (fst arg1) (fst arg2)
+  let eval_intrin op args rt = eval_intrin op (List.map fst args)
+  *)
+end
+
+module IsZeroValueAbstractionBasil = struct
+  include
+    Intra_analysis.ValueAbstractionIgnoringTypes (IsZeroValueAbstractionUntyped)
 
   module E = Lang.Expr.BasilExpr
+
+  let top = IsZeroLattice.Top
 end
 
 include Dataflow_graph.EasyForwardAnalysisPack (IsZeroValueAbstractionBasil)

lib/analysis/intra_analysis.ml

@@ -5,61 +5,78 @@ open Common
 open Containers
 open Lattice_types
 
-module EvalExprLog (V : ValueAbstraction) = struct
+module EvalExpr (V : ValueAbstraction) = struct
   type t
 
-  let eval show_const show_unop show_binop show_intrin read expr =
+  let alg read e =
     let open Expr.AbstractExpr in
-    let eval_alg e =
-      let e_eval = Expr.AbstractExpr.map fst e in
-      let e_pretty = Expr.AbstractExpr.map snd e in
-      let evaled =
-        match e_eval with
-        | RVar v -> read v
-        | Constant c -> V.eval_const c
-        | UnaryExpr (op, e) -> V.eval_unop op e
-        | BinaryExpr (op, a, b) -> V.eval_binop op a b
-        | ApplyIntrin (op, es) -> V.eval_intrin op es
-        | _ -> failwith "unsupported"
-      in
-      let pretty =
-        let open Containers_pp in
-        let eval_e = textpf "%s = " (V.show evaled) in
-        let print op lst =
-          bracket " ("
-            (eval_e
-            ^ bracket "(" (text op ^ nest 2 (fill (text ";" ^ newline) lst)) ")"
-            )
-            ")"
-        in
-        match e_pretty with
-        | RVar v -> eval_e ^ text @@ V.E.Var.show v
-        | Constant c -> eval_e ^ text @@ show_const c
-        | UnaryExpr (op, e) -> print (show_unop op) [ e ]
-        | BinaryExpr (op, a, b) -> print (show_binop op) [ a; b ]
-        | ApplyIntrin (op, es) -> print (show_intrin op) es
-        | _ -> failwith "unsupported"
-      in
-      (evaled, pretty)
-    in
-    V.E.cata eval_alg expr
+    match e with
+    | RVar v -> read v
+    | Constant c -> V.eval_const c
+    | UnaryExpr (op, e) -> V.eval_unop op e
+    | BinaryExpr (op, a, b) -> V.eval_binop op a b
+    | ApplyIntrin (op, es) -> V.eval_intrin op es
+    | _ -> failwith "unsupported"
+
+  let eval read expr = V.E.cata (alg read) expr
 end
 
-module EvalExpr (V : ValueAbstraction) = struct
+module EvalExprWithType (V : TypedValueAbstraction) = struct
   type t
 
-  let eval read expr =
+  let alg read e =
     let open Expr.AbstractExpr in
-    let eval_alg e =
+    let tt = V.E.type_alg (Expr.AbstractExpr.map snd e) in
+    let r =
       match e with
       | RVar v -> read v
-      | Constant c -> V.eval_const c
-      | UnaryExpr (op, e) -> V.eval_unop op e
-      | BinaryExpr (op, a, b) -> V.eval_binop op a b
-      | ApplyIntrin (op, es) -> V.eval_intrin op es
+      | Constant c -> V.eval_const c tt
+      | UnaryExpr (op, e) -> V.eval_unop op e tt
+      | BinaryExpr (op, a, b) -> V.eval_binop op a b tt
+      | ApplyIntrin (op, es) -> V.eval_intrin op es tt
       | _ -> failwith "unsupported"
     in
-    V.E.cata eval_alg expr
+    (r, tt)
+
+  let eval read expr =
+    let open Expr.AbstractExpr in
+    fst (V.E.cata (alg read) expr)
+end
+
+module EvalExprLog (V : TypedValueAbstraction) = struct
+  type t
+
+  module Eval = EvalExprWithType (V)
+
+  let pretty_alg show_const show_unop show_binop show_intrin read e =
+    let e_pretty = Expr.AbstractExpr.map fst e in
+    let evaled = Eval.alg read (Expr.AbstractExpr.map snd e) in
+    let pretty =
+      let open Containers_pp in
+      let eval_e = textpf "%s = " (V.show @@ fst evaled) in
+      let print op lst =
+        bracket " ("
+          (eval_e
+          ^ bracket "(" (text op ^ nest 2 (fill (text ";" ^ newline) lst)) ")")
+          ")"
+      in
+      match e_pretty with
+      | RVar v -> eval_e ^ text @@ V.E.Var.show v
+      | Constant c -> eval_e ^ text @@ show_const c
+      | UnaryExpr (op, e) -> print (show_unop op) [ e ]
+      | BinaryExpr (op, a, b) -> print (show_binop op) [ a; b ]
+      | ApplyIntrin (op, es) -> print (show_intrin op) es
+      | _ -> failwith "unsupported"
+    in
+    (pretty, evaled)
+
+  let eval show_const show_unop show_binop show_intrin read expr =
+    let p, (v, _) =
+      V.E.cata
+        (pretty_alg show_const show_unop show_binop show_intrin read)
+        expr
+    in
+    (v, p)
 end
 
 module EvalValueAbstraction
@@ -72,13 +89,22 @@ struct
   let eval read expr = Eval.eval read expr
 end
 
+module ValueAbstractionIgnoringTypes (V : ValueAbstraction) = struct
+  include V
+
+  let eval_const op rt = eval_const op
+  let eval_unop op arg rt = eval_unop op (fst arg)
+  let eval_binop op arg1 arg2 rt = eval_binop op (fst arg1) (fst arg2)
+  let eval_intrin op args rt = eval_intrin op (List.map fst args)
+end
+
 module EvalStmt
-    (V : ValueAbstraction)
+    (V : TypedValueAbstraction with module E = Expr.BasilExpr)
     (S : StateAbstraction with type val_t = V.t with type key_t = V.E.var) =
 struct
   type t
 
-  module EV = EvalExpr (V)
+  module EV = EvalExprWithType (V)
 
   let stmt_eval_fwd stmt dom =
     Stmt.map ~f_lvar:id

lib/analysis/known_bits.ml

@@ -264,7 +264,13 @@ module IsKnownBitsValueAbstraction = struct
 end
 
 module IsKnownValueAbstractionBasil = struct
-  include IsKnownBitsValueAbstraction
+  include Intra_analysis.ValueAbstractionIgnoringTypes (struct
+    include IsKnownBitsValueAbstraction
+    module E = Lang.Expr.BasilExpr
+  end)
+
+  let top = IsKnownLattice.Top
+
   module E = Lang.Expr.BasilExpr
 end
 

lib/analysis/lattice_types.ml

@@ -1,6 +1,5 @@
 open Lang
 open Common
-open Containers
 
 module type Lattice = sig
   val name : string
@@ -27,6 +26,47 @@ module type ValueAbstraction = sig
   val eval_intrin : E.intrin -> t list -> t
 end
 
+module type TypedValueAbstraction = sig
+  (** A value abstraction that takes type information *)
+
+  include Lattice
+  module E : Expr.ExprType
+
+  (** evaluate operators *)
+
+  val eval_const : E.const -> E.ty -> t
+  (** Return an abstract value for a constant: [eval_const op rt]
+
+      @param op const op
+      @param rt type of constant [const]
+      @return abstract value for constant *)
+
+  val eval_unop : E.unary -> t * E.ty -> E.ty -> t
+  (** Abstract a unary op expression [eval_unop op arg rt]
+
+      @param op unary operator
+      @param arg tuple (argument value, type)
+      @param rt operation return type
+      @return abstract value operation result *)
+
+  val eval_binop : E.binary -> t * E.ty -> t * E.ty -> E.ty -> t
+  (** Abstract a binary expression [eval_binop op arg1 arg2 rt]
+
+      @param op binary operator
+      @param arg1 first arg tuple (abstract value, type)
+      @param arg2 second arg tuple (abstract value, type)
+      @param rt operation return type
+      @return abstract value result of operation *)
+
+  val eval_intrin : E.intrin -> (t * E.ty) list -> E.ty -> t
+  (** Abstract an n-ary intrinsic op [eval_intrin op args rt]
+
+      @param op operator
+      @param args argument list of tuples (abstract value, type)
+      @param rt operation return type
+      @return abstract value result of operation *)
+end
+
 (** a value abstraction providing variable store/load operations *)
 module type StateAbstraction = sig
   type val_t
@@ -46,3 +86,82 @@ module type Domain = sig
   val transfer : t -> Program.stmt -> t
   val init : Program.proc -> t
 end
+
+module FlatLattice (L : sig
+  include ORD_TYPE
+
+  val name : string
+end) =
+struct
+  type t = Top | V of L.t | Bot [@@deriving eq, ord]
+
+  let name = L.name ^ ".flat_lattice"
+  let bottom = Bot
+
+  let show a =
+    match a with
+    | Top -> Bincaml_util.Unicode.top_char
+    | Bot -> Bincaml_util.Unicode.bot_char
+    | V t -> L.show t
+
+  let pretty a =
+    Containers_pp.text
+    @@
+    match a with
+    | Top -> Bincaml_util.Unicode.top_char
+    | Bot -> Bincaml_util.Unicode.bot_char
+    | V t -> L.show t
+
+  let bind f a = match a with V x -> f x | o -> o
+
+  let bind2 f a b =
+    match (a, b) with
+    | V l, V r -> f l r
+    | Bot, _ -> Bot
+    | _, Bot -> Bot
+    | _ -> Top
+
+  let map f a = bind (fun x -> V (f x)) a
+  let map2 f a b = bind2 (fun x y -> V (f x y)) a b
+  let join a b = match (a, b) with Top, _ -> Top | _, Top -> Top | _ -> Bot
+  let widening a b = join a b
+end
+
+module LiftLattice (L : Lattice) : Lattice = struct
+  include FlatLattice (L)
+
+  let name = L.name ^ ".lift_lattice"
+  let widening a b = map2 L.widening a b
+
+  let join a b =
+    match (a, b) with
+    | Top, _ -> Top
+    | _, Top -> Top
+    | Bot, _ -> Bot
+    | _, Bot -> Bot
+    | V a, V b -> V (L.join a b)
+end
+
+(*
+module BitWidthLattice (L : Lattice) : TypedValueAbstraction = struct
+  module IL = FlatLattice (struct
+    include Int
+
+    let show = Int.to_string
+    let name = "int63"
+  end)
+
+  include IL
+  module E = Expr.BasilExpr
+
+  let width o =
+    match o with
+    | Ops.AllOps.Fun { ret } -> Types.bit_width ret
+    | _ -> failwith "type error"
+
+  type ty = Types.t
+  type t = IL.t * L.t
+
+  let eval_const op = Ops.AllOps.ret_type_const
+end
+*)