Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Copilot wants to merge 14 commits into
base: master
Choose a base branch
from
Open

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

Show file tree
Hide file tree
Changes from 9 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
3d99dec
Initial plan
Copilot May 23, 2026
9a91271
port tutorial analyses to simplified spec interface
Copilot May 23, 2026
54ce701
restore unitAnalysis and add simplifiedUnitAnalysis
Copilot May 23, 2026
812244e
export SimplifiedUnitAnalysis from goblint_lib
Copilot May 23, 2026
7aa7b6a
Reuse SimplifiedUnitAnalysis defaults in signs tutorials
Copilot May 25, 2026
2afea51
Adjust SimplifiedUnitAnalysis defaults to safe shared subset
Copilot May 25, 2026
ae90222
Potential fix for pull request finding
michael-schwarz May 25, 2026
a8ffdb7
Merge branch 'master' into copilot/port-tutorial-analyses
michael-schwarz Jul 14, 2026
2967be9
Restore named arguments: replace _ with descriptive names in tutorial…
Copilot Jul 15, 2026
4284b18
Add back comment
michael-schwarz Jul 31, 2026
a6f9ea9
Add DefaultSpec for simplified analyses
michael-schwarz Jul 31, 2026
82488eb
Address comments
michael-schwarz Jul 31, 2026
4fcc63d
Address comment
michael-schwarz Jul 31, 2026
5b3ad4f
Address remaining comments
michael-schwarz Jul 31, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 30 additions & 26 deletions src/analyses/tutorials/constants.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down Expand Up @@ -44,29 +47,31 @@ struct
| _ -> I.top ()

(* transfer functions *)
let assign man (lval:lval) (rval:exp) : D.t =
let query man state (type a) (q: a Queries.t): a Queries.result =
Queries.Result.top q
Comment thread
michael-schwarz marked this conversation as resolved.
Outdated

let assign man 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 man 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 man 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 man 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 man caller_state (lval: lval option) (f:fundec) (args: 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
Expand All @@ -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 man state (callee_local: D.t) (lval:lval option) (f: fundec) (args: 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 man state (lval: lval option) (f:varinfo) (arglist: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 man (_, c) f callee_state = c
let threadenter man state f args = D.top ()
Comment thread
michael-schwarz marked this conversation as resolved.
Outdated
end

let _ =
MCP.register_analysis (module Spec : MCPSpec)
MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
32 changes: 17 additions & 15 deletions src/analyses/tutorials/signs.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@

open GoblintCil
open Analyses
open SimplifiedAnalysis

module Signs =
struct
Expand Down Expand Up @@ -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
Expand All @@ -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 man 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 ()
Expand All @@ -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... *)
Comment thread
michael-schwarz marked this conversation as resolved.
let query man (type a) (q: a Queries.t): a Queries.result =
let query man 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 man ((state: D.t), _) f callee_state = state
let threadenter man state f args = state
end

let _ =
MCP.register_analysis (module Spec : MCPSpec)
MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
50 changes: 50 additions & 0 deletions src/analyses/tutorials/simplifiedUnitAnalysis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
(** Simplest possible analysis with unit domain ([simplifiedUnit]). *)

open GoblintCil
open SimplifiedAnalysis

module DefaultSpec =
struct
let query man state (type a) (q: a Queries.t) : a Queries.result =
Queries.Result.top q

let assign man state (lval: lval) (rval: exp) =
state

let branch man state (exp: exp) (tv: bool) =
state

let body man state (f: fundec) =
state

let return man state (exp: exp option) (f: fundec) =
state

let enter man state (lval: lval option) (f: fundec) (args: exp list) =
state

let combine man caller_state callee_local (lval: lval option) (f: fundec) (args: exp list) =
callee_local

let special man state (lval: lval option) (f: varinfo) (args: exp list) =
state
end

module Spec : SimplifiedSpec =
struct
include DefaultSpec
Comment thread
michael-schwarz marked this conversation as resolved.
Outdated

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 man (_, c) f callee_state = c
let threadenter man state f args = D.top ()
end

let _ =
MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
32 changes: 17 additions & 15 deletions src/analyses/tutorials/solution/signsExtendSol.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@

open GoblintCil
open Analyses
open SimplifiedAnalysis

module Signs =
struct
Expand Down Expand Up @@ -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
Comment thread
michael-schwarz marked this conversation as resolved.
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
Expand All @@ -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 man 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 ()
Expand All @@ -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 man 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 man ((state: D.t), _) f callee_state = state
let threadenter man state f args = state
end

let _ =
MCP.register_analysis (module Spec : MCPSpec)
MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
32 changes: 17 additions & 15 deletions src/analyses/tutorials/solution/signsSol.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@

open GoblintCil
open Analyses
open SimplifiedAnalysis

module Signs =
struct
Expand Down Expand Up @@ -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
Expand All @@ -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 man 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 ()
Expand All @@ -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 man 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 man ((state: D.t), _) f callee_state = state
let threadenter man state f args = state
end

let _ =
MCP.register_analysis (module Spec : MCPSpec)
MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
Loading
Loading