Port tutorial analyses to SimplifiedSpec and reuse SimplifiedUnitAnalysis defaults while preserving unitAnalysis compatibility

src/analyses/tutorials/constants.ml

@@ -2,21 +2,24 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 (** An analysis specification for didactic purposes.
  It only considers definite values of local variables.
  We do not pass information interprocedurally. *)
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  let name () = "constants"
+  let name = "constants"
+  module V = Printable.Unit
+  module G = Lattice.Unit
 
   module I = IntDomain.Flattened
 
   (* Map of (local int) variables to flat integers *)
   module D = MapDomain.MapBot (Basetype.Variables) (I)
 
   (* No contexts *)
-  include Analyses.IdentityUnitContextsSpec
+  module C = Printable.Unit
 
   let get_local = function
     | Var v, NoOffset when isIntegralType v.vtype && not (v.vglob || v.vaddrof) -> Some v (* local integer variable whose address is never taken *)
@@ -44,29 +47,31 @@ struct
     | _ -> I.top ()
 
   (* transfer functions *)
-  let assign man (lval:lval) (rval:exp) : D.t =
+  let query _ _ (type a) (q: a Queries.t): a Queries.result =
+    Queries.Result.top q
+
+  let assign _ state (lval:lval) (rval:exp) : D.t =
     match get_local lval with
-    | Some loc -> D.add loc (eval man.local rval) man.local
-    | None -> man.local
+    | Some loc -> D.add loc (eval state rval) state
+    | None -> state
 
-  let branch man (exp:exp) (tv:bool) : D.t =
-    let v = eval man.local exp in
+  let branch _ state (exp:exp) (tv:bool) : D.t =
+    let v = eval state exp in
     match I.to_bool v with
       | Some b when b <> tv -> raise Deadcode (* if the expression evaluates to not tv, the tv branch is not reachable *)
-      | _ -> man.local
+      | _ -> state
 
-  let body man (f:fundec) : D.t =
+  let body _ state (f:fundec) : D.t =
     (* Initialize locals to top *)
-    List.fold_left (fun m l -> D.add l (I.top ()) m) man.local f.slocals
+    List.fold_left (fun m l -> D.add l (I.top ()) m) state f.slocals
 
-  let return man (exp:exp option) (f:fundec) : D.t =
+  let return _ state (exp:exp option) (f:fundec) : D.t =
     (* Do nothing, as we are not interested in return values for now. *)
-    man.local
+    state
 
-  let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+  let enter _ (_: D.t) (_: lval option) (f:fundec) (_: exp list) : D.t =
     (* Set the formal int arguments to top *)
-    let callee_state = List.fold_left (fun m l -> D.add l (I.top ()) m) (D.bot ()) f.sformals in
-    [(man.local, callee_state)]
+    List.fold_left (fun m l -> D.add l (I.top ()) m) (D.bot ()) f.sformals
 
   let set_local_int_lval_top (state: D.t) (lval: lval option) =
     match lval with
@@ -77,22 +82,21 @@ struct
         )
       |_ -> state
 
-  let combine_env man lval fexp f args fc au f_ask =
-    man.local (* keep local as opposed to IdentitySpec *)
-
-  let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask): D.t =
+  let combine _ state (_: D.t) (lval:lval option) (_: fundec) (_: exp list): D.t =
     (* If we have a function call with assignment
         x = f (e1, ... , ek)
       with a local int variable x on the left, we set it to top *)
-    set_local_int_lval_top man.local lval
+    set_local_int_lval_top state lval
 
-  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+  let special _ state (lval: lval option) (_:varinfo) (_:exp list) : D.t =
     (* When calling a special function, and assign the result to some local int variable, we also set it to top. *)
-    set_local_int_lval_top man.local lval
+    set_local_int_lval_top state lval
 
-  let startstate v = D.bot ()
-  let exitstate v = D.top () (* TODO: why is this different from startstate? *)
+  let startstate = D.bot ()
+  let startcontext = ()
+  let context _ (_, c) _ _ = c
+  let threadenter _ _ _ _ = D.top ()
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)

src/analyses/tutorials/signs.ml

@@ -4,6 +4,7 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 module Signs =
 struct
@@ -44,18 +45,20 @@ struct
     | _ -> false
 end
 
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  let name () = "signs"
+  include SimplifiedUnitAnalysis.DefaultSpec
+
+  let name = "signs"
+  module V = Printable.Unit
+  module G = Lattice.Unit
 
   (* Map of integers variables to our signs lattice. *)
   module D = MapDomain.MapBot (Basetype.Variables) (SL)
-  include Analyses.ValueContexts(D)
+  module C = D
 
-  let startstate v = D.bot ()
-  let exitstate = startstate
-
-  include Analyses.IdentitySpec
+  let startstate = D.bot ()
+  let startcontext = D.bot ()
 
   (* This should now evaluate expressions. *)
   let eval (d: D.t) (exp: exp): SL.t = match exp with
@@ -67,8 +70,7 @@ struct
 
   (* Transfer functions: we only implement assignments here.
    * You can leave this code alone... *)
-  let assign man (lval:lval) (rval:exp) : D.t =
-    let d = man.local in
+  let assign _ d (lval:lval) (rval:exp) : D.t =
     match lval with
     | (Var x, NoOffset) when not x.vaddrof -> D.add x (eval d rval) d
     | _ -> D.top ()
@@ -79,17 +81,17 @@ struct
     | BinOp (Lt, e1, e2, _) -> SL.lt (eval d e1) (eval d e2)
     | _ -> false
 
-  (* We should now provide this information to Goblint. Assertions are integer expressions,
-   * so we implement here a response to EvalInt queries.
-   * You should definitely leave this alone... *)
-  let query man (type a) (q: a Queries.t): a Queries.result =
+  let query _ state (type a) (q: a Queries.t): a Queries.result =
     let open Queries in
     match q with
-    | EvalInt e when assert_holds man.local e ->
+    | EvalInt e when assert_holds state e ->
       let ik = Cilfacade.get_ikind_exp e in
       ID.of_bool ik true
     | _ -> Result.top q
+
+  let context _ ((state: D.t), _) _ _ = state
+  let threadenter _ state _ _ = state
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)

src/analyses/tutorials/simplifiedUnitAnalysis.ml

@@ -0,0 +1,50 @@
+(** Simplest possible analysis with unit domain ([simplifiedUnit]). *)
+
+open GoblintCil
+open SimplifiedAnalysis
+
+module DefaultSpec =
+struct
+  let query _ _ (type a) (q: a Queries.t) : a Queries.result =
+    Queries.Result.top q
+
+  let assign _ state (_: lval) (_: exp) =
+    state
+
+  let branch _ state (_: exp) (_: bool) =
+    state
+
+  let body _ state (_: fundec) =
+    state
+
+  let return _ state (_: exp option) (_: fundec) =
+    state
+
+  let enter _ state (_: lval option) (_: fundec) (_: exp list) =
+    state
+
+  let combine _ state _ (_: lval option) (_: fundec) (_: exp list) =
+    state
+
+  let special _ state (_: lval option) (_: varinfo) (_: exp list) =
+    state
+end
+
+module Spec : SimplifiedSpec =
+struct
+  include DefaultSpec
+
+  let name = "simplifiedUnit"
+  module V = Printable.Unit
+  module G = Lattice.Unit
+  module D = Lattice.Unit
+  module C = Printable.Unit
+
+  let startstate = D.bot ()
+  let startcontext = ()
+  let context _ (_, c) _ _ = c
+  let threadenter _ _ _ _ = D.top ()
+end
+
+let _ =
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)

src/analyses/tutorials/solution/signsExtendSol.ml

@@ -4,6 +4,7 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 module Signs =
 struct
@@ -46,18 +47,20 @@ struct
     for_all (fun x -> for_all (fun y -> Signs.lt x y) y) x
 end
 
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  let name () = "signsExtendSol"
+  include SimplifiedUnitAnalysis.DefaultSpec
+
+  let name = "signsExtendSol"
+  module V = Printable.Unit
+  module G = Lattice.Unit
 
   (* Map of integers variables to our signs lattice. *)
   module D = MapDomain.MapBot (Basetype.Variables) (SL)
-  include Analyses.ValueContexts(D)
-
-  let startstate v = D.bot ()
-  let exitstate = startstate
+  module C = D
 
-  include Analyses.IdentitySpec
+  let startstate = D.bot ()
+  let startcontext = D.bot ()
 
   (* This should now evaluate expressions. *)
   let eval (d: D.t) (exp: exp): SL.t = match exp with
@@ -69,8 +72,7 @@ struct
 
   (* Transfer functions: we only implement assignments here.
    * You can leave this code alone... *)
-  let assign man (lval:lval) (rval:exp) : D.t =
-    let d = man.local in
+  let assign _ d (lval:lval) (rval:exp) : D.t =
     match lval with
     | (Var x, NoOffset) when not x.vaddrof -> D.add x (eval d rval) d
     | _ -> D.top ()
@@ -81,17 +83,17 @@ struct
     | BinOp (Lt, e1, e2, _) -> SL.lt (eval d e1) (eval d e2)
     | _ -> false
 
-  (* We should now provide this information to Goblint. Assertions are integer expressions,
-   * so we implement here a response to EvalInt queries.
-   * You should definitely leave this alone... *)
-  let query man (type a) (q: a Queries.t): a Queries.result =
+  let query _ state (type a) (q: a Queries.t): a Queries.result =
     let open Queries in
     match q with
-    | EvalInt e when assert_holds man.local e ->
+    | EvalInt e when assert_holds state e ->
       let ik = Cilfacade.get_ikind_exp e in
       ID.of_bool ik true
     | _ -> Result.top q
+
+  let context _ ((state: D.t), _) _ _ = state
+  let threadenter _ state _ _ = state
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)

src/analyses/tutorials/solution/signsSol.ml

@@ -4,6 +4,7 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 module Signs =
 struct
@@ -44,18 +45,20 @@ struct
     | _ -> false
 end
 
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  let name () = "signsSol"
+  include SimplifiedUnitAnalysis.DefaultSpec
+
+  let name = "signsSol"
+  module V = Printable.Unit
+  module G = Lattice.Unit
 
   (* Map of integers variables to our signs lattice. *)
   module D = MapDomain.MapBot (Basetype.Variables) (SL)
-  include Analyses.ValueContexts(D)
-
-  let startstate v = D.bot ()
-  let exitstate = startstate
+  module C = D
 
-  include Analyses.IdentitySpec
+  let startstate = D.bot ()
+  let startcontext = D.bot ()
 
   (* This should now evaluate expressions. *)
   let eval (d: D.t) (exp: exp): SL.t = match exp with
@@ -67,8 +70,7 @@ struct
 
   (* Transfer functions: we only implement assignments here.
    * You can leave this code alone... *)
-  let assign man (lval:lval) (rval:exp) : D.t =
-    let d = man.local in
+  let assign _ d (lval:lval) (rval:exp) : D.t =
     match lval with
     | (Var x, NoOffset) when not x.vaddrof -> D.add x (eval d rval) d
     | _ -> D.top ()
@@ -79,17 +81,17 @@ struct
     | BinOp (Lt, e1, e2, _) -> SL.lt (eval d e1) (eval d e2)
     | _ -> false
 
-  (* We should now provide this information to Goblint. Assertions are integer expressions,
-   * so we implement here a response to EvalInt queries.
-   * You should definitely leave this alone... *)
-  let query man (type a) (q: a Queries.t): a Queries.result =
+  let query _ state (type a) (q: a Queries.t): a Queries.result =
     let open Queries in
     match q with
-    | EvalInt e when assert_holds man.local e ->
+    | EvalInt e when assert_holds state e ->
       let ik = Cilfacade.get_ikind_exp e in
       ID.of_bool ik true
     | _ -> Result.top q
+
+  let context _ ((state: D.t), _) _ _ = state
+  let threadenter _ state _ _ = state
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)