Symbolic abstractions #131

giltho · 2025-09-10T20:58:58Z

This PR introduces the Sym_data folder, which contains utilities for what I call (in my thesis) Symbolic Abstractions. Really... simple abstract domains.

S_eq is an abstraction that implements equality, while S_int is an abstraction over integers (i.e. a symbolic "thing" that can be interpreted as an integer).
I also add S_range (used for TreeBlocks) and S_map (used for PMap) -- We really need a linter to enforce naming conventions 😭

I also extract more clearly what sbool is and explicitly, i.e. an abstraction over booleans. Some of the resulting code is slightly more verbose but I think that's ok.

Also, some of the code in TreeBlock is a bit verbose because of MemVal.S_int.zero () everywhere but #125 fixes this already :)

N1ark

Conceptually this is cool but I am not very convinced, because rn it adds a lot of code and signatures that are barely used, even where they seem to fit (Symex).

The dependency Symex -> Sym_data is quite unpractical, and I wonder if there is not a cleverer split to do, like:

Sym_val for symbolic values, ie. just defining the shape of different sorts of values (with S_bool, S_int, S_eq, S_elt, S_range)
Symex, defines symbolic processes using symbolic values
Sym_data, defines data structures using symbolic values processes. s_map right now, but could include sets, maybe binary trees, idk.

We could just re-export Sym_val from Sym_data to only provide one module of symbolic things, but at least it would avoid the weird split we have rn, because Symex not reusing S_eq etc. is super weird to me

N1ark · 2025-09-11T09:27:59Z

soteria-c/lib/globs.ml

    let open Typed.Infix in
    let* loc = Csymex.nondet Typed.t_loc in
-    let+ () = Symex.assume [ Typed.not (loc ==@ Typed.Ptr.null_loc) ] in
+    let+ () = Symex.assume [ Typed.S_bool.not (loc ==@ Typed.Ptr.null_loc) ] in


what I did for bv_values to avoid this, which is super unpractical, is that I include S_bool in Typed -- would make these simpler since bool operations are primitive enough that you always want them imo

ah nvm you can't because the type is t so it'd override stuff.... hmm

N1ark · 2025-09-11T09:30:39Z

soteria/lib/c_values/svalue.ml

-    | _ -> Unop (Not, sv) <| TBool
+let conj l = List.fold_left S_bool.and_ v_true l

 let rec split_ands (sv : t) (f : t -> unit) : unit =


why not include split_ands and conj in S_bool? You're not restricting its type to the module type S_bool anyways so you can add stuff

N1ark · 2025-09-11T09:33:09Z

soteria/lib/symex/value.ml

+module S_bool = struct
+  module type S = sig
+    type +'a v
+    type t
+
+    val not : t v -> t v
+    val and_ : t v -> t v -> t v
+    val or_ : t v -> t v -> t v
+    val to_bool : t v -> bool option
+    val of_bool : bool -> t v
+  end
+
+  module Make_syntax (S_bool : S) = struct
+    let ( &&@ ) = S_bool.and_
+    let ( ||@ ) = S_bool.or_
+    let not = S_bool.not
+  end
+end
+


Maybe I'm being picky but it was very weird seeing s_int.ml in sym_data but having to go here for S_bool

ok it's because module sym_data depends on Symex but Symex depends on this.... :s

N1ark · 2025-09-11T09:34:07Z

soteria/lib/c_values/typed.mli

-(** Typed constructors *)
+(** {3 Typed constructors} *)
+
+module S_bool : Symex.Value.S_bool.S with type 'a v = 'a t and type t = sbool


here you could do sig include Symex.Value.S_bool.S ... val split_ands : ... end

at least to me it makes a lot more sense if you package all bool operations together

soteria/lib/sym_data/s_map.ml

soteria/lib/sym_data/sym_data.ml

N1ark · 2025-09-11T09:38:43Z

soteria/lib/sym_states/tree_block.ml

+  open Sym_data.S_int.Make_syntax (MemVal.S_int)
+  open Make_bool_syntax (Symex.Value.S_bool)
+  module Range = Sym_data.S_range.Make (MemVal.S_int)


ok this is quite nice -- only thing is the weird mismatch in names/paths between Sym_data.S_int.Make_syntax and Make_bool_syntax but ok

It's because Symex is overriden so I can't go and fetch Symex.Value.S_bool.Syntax :/

N1ark · 2025-09-11T09:41:58Z

soteria/lib/symex/value.ml

  val iter_vars : 'a t -> 'b ty Var.iter_vars
  val subst : (Var.t -> Var.t) -> 'a t -> 'a t


again maybe i'm being slow but I find it confusing we still have this here despite defining the same functions is s_elt

yeah :/ It's a bit messy I agree

soteria-c/lib/ctree_block.ml

N1ark · 2025-09-11T09:54:36Z

The State_monad i made for rust could also fit in sym_data maybe

giltho · 2025-09-11T11:11:25Z

The State_monad i made for rust could also fit in sym_data maybe

I don't think so, the state_monad you have is not necessarily symbolic. It's just a state monad transformer

giltho · 2025-09-11T12:48:48Z

Gave it a thought and I agree: I should declare S_eq and S_elt in Value, and then declare that value is just

include S_eq
include S_elt
module S_bool : S_bool

...

Signed-off-by: Sacha Ayoun <[email protected]>

Co-authored-by: N1ark <[email protected]>

Signed-off-by: Sacha Ayoun <[email protected]>

N1ark · 2025-09-30T19:05:55Z

soteria/lib/sym_data/s_map.ml

+  S with type key = Key.t and module Symex = Symex = struct
+  module Symex = Symex
+  open Symex.Syntax
+  module Raw_map = Stdlib.Map.Make (Key)


looking back -- why don't you include Raw_map? or at least reexpose some of it, since e.g. one probably wants add, empty functions

Signed-off-by: Sacha Ayoun <[email protected]>

N1ark

still not convinced tbh :/ (sorry if this wasnt ready for review)

N1ark · 2025-11-21T09:06:37Z

soteria-c/lib/ctree_block.ml

+    let add = Infix.( +!@ )
+    let sub = Infix.( -!@ )


you should mark these as checked since we assume no overflows within blocktrees

Suggested change

let add = Infix.( +!@ )

let sub = Infix.( -!@ )

let add = Infix.( +!!@ )

let sub = Infix.( -!!@ )

N1ark · 2025-11-21T09:08:05Z

soteria-rust/lib/rtree_block.ml

+      let add = Infix.( +!@ )
+      let sub = Infix.( -!@ )


same here, see original code

Suggested change

let add = Infix.( +!@ )

let sub = Infix.( -!@ )

(* We assume addition/overflow within the range of an allocation may never overflow.

This allows extremely good reductions around inequalities, which Tree_block relies on. *)

let ( +@ ) = Infix.( +!!@ )

let ( -@ ) = Infix.( -!!@ )

N1ark · 2025-11-21T09:13:18Z

soteria/lib/bv_values/bv_solver.ml

          | Unop (Not, e) ->
              let e' = simplify e in
-              if Svalue.equal e e' then fallback v else Svalue.Bool.not e'
+              if Svalue.equal e e' then v else Svalue.S_bool.not e'


So here fallback is basically Analyses.simplify. If you remove the fallback here you get less reductions, in particular in some corner cases.

e.g. if you have a state where x is in [3, INT_MAX] you cannot simplify x < 5 (that would be OX), but you can simplify !(x < 5) (which is x >= 5) into true.

(ofc this example in particular cannot happen since we'd reduce !(x < 5) to x >= 5 directly but i know there are cases where this applies)

i think i would rather keep all these inner fallbacks if possible, we can always do some benchmarking at some point to see how useful they are

Yes, this is just a mismanaged merge conflict, thanks for catching this

N1ark · 2025-11-21T09:20:13Z

soteria/lib/bv_values/typed.mli

 val v_true : [> sbool ] t
 val v_false : [> sbool ] t
-val bool : bool -> [> sbool ] t
-val as_bool : 'a t -> bool option
-val and_ : [< sbool ] t -> [< sbool ] t -> [> sbool ] t
 val conj : [< sbool ] t list -> [> sbool ] t
 val split_ands : [< sbool ] t -> ([> sbool ] t -> unit) -> unit
-val or_ : [< sbool ] t -> [< sbool ] t -> [> sbool ] t
 val not : sbool t -> sbool t


curiosity : why would you unexport some of these but not all ? maybe in this case it makes sense in the module S_bool : Symex.Value.S_bool.S declaration to instead have something like

module S_bool : sig include Symex.Value.S_bool.S with ... val v_true : ... etc end

I really messed up that merge didn't I? 😆

N1ark · 2025-11-21T09:37:43Z

soteria/lib/bv_values/svalue.ml

+module type S_bool = sig
  val v_true : t
  val v_false : t
-  val as_bool : t -> bool option
-  val bool : bool -> t
+  val to_bool : t -> bool option
+  val of_bool : bool -> t


here you could do

module type S_bool = sig include Symex.Value.S_bool.S with ... val v_true : ... etc end

Signed-off-by: Sacha Ayoun <[email protected]>

giltho · 2025-12-15T16:28:47Z

I think I won't merge this, but here's a list of things that are in this PR, and I will import them as needed in other PRs.

✅ means I'm sure I want Soteria to have this
❓means I'm not sure
Sym_data.Map and rewriting Sym_states.PMap using Sym_data.Map ✅
S_bool as a module ❓
S_int❓
S_elt (t + iter_vars + subst) ✅
S_range ❓(would be sure, but not sure I want it without S_int)

Opinions are welcome btw

giltho requested a review from N1ark as a code owner September 10, 2025 20:58

N1ark reviewed Sep 11, 2025

View reviewed changes

giltho and others added 20 commits September 16, 2025 10:41

more doc

e55d996

Signed-off-by: Sacha Ayoun <[email protected]>

doc

0862a8a

In progress

31b8647

Implement symbolic maps

aa8c50a

tinsy bit of doc

face434

Signed-off-by: Sacha Ayoun <[email protected]>

kill channels.ml

8a33485

Signed-off-by: Sacha Ayoun <[email protected]>

more doc

587668a

Signed-off-by: Sacha Ayoun <[email protected]>

bits of doc

20a8a91

Signed-off-by: Sacha Ayoun <[email protected]>

symbolic integers

d5f1bec

Signed-off-by: Sacha Ayoun <[email protected]>

Explicit S_bool module

ac53dd3

Signed-off-by: Sacha Ayoun <[email protected]>

S_elt is printable

a14070f

Signed-off-by: Sacha Ayoun <[email protected]>

Symbolic ranges

7e9c460

Signed-off-by: Sacha Ayoun <[email protected]>

S_int doesn't use infix

cd94263

Signed-off-by: Sacha Ayoun <[email protected]>

Make_syntax for S_int

6b3244d

Signed-off-by: Sacha Ayoun <[email protected]>

syntaxes

6a4556c

Signed-off-by: Sacha Ayoun <[email protected]>

this is actually what I need

4445595

Signed-off-by: Sacha Ayoun <[email protected]>

more juggling around

6144648

Signed-off-by: Sacha Ayoun <[email protected]>

let's go! Tree_block now uses proper S_int

186ce51

Signed-off-by: Sacha Ayoun <[email protected]>

Update soteria/lib/sym_data/sym_data.ml

0c4413c

Co-authored-by: N1ark <[email protected]>

post-rebase fixups

c34fa4f

Signed-off-by: Sacha Ayoun <[email protected]>

giltho force-pushed the cleanup-4 branch from 3b45825 to c34fa4f Compare September 16, 2025 11:47

N1ark reviewed Sep 30, 2025

View reviewed changes

Merge branch 'main' into cleanup-4

a90dd45

N1ark added soteria-core Issues related to the Soteria core library cleanliness Quality of life improvements, to keep the codebase clean and healthy labels Nov 11, 2025

giltho added 2 commits November 20, 2025 23:07

Merge branch 'main' into cleanup-4

9b1e149

Signed-off-by: Sacha Ayoun <[email protected]>

promote test

0bac1ec

Signed-off-by: Sacha Ayoun <[email protected]>

N1ark requested changes Nov 21, 2025

View reviewed changes

N1ark reviewed Nov 21, 2025

View reviewed changes

woops

b6e0ad2

Signed-off-by: Sacha Ayoun <[email protected]>

		val iter_vars : 'a t -> 'b ty Var.iter_vars
		val subst : (Var.t -> Var.t) -> 'a t -> 'a t

-      let add = Infix.( +!@ )
-      let sub = Infix.( -!@ )
+      (* We assume addition/overflow within the range of an allocation may never overflow.
+         This allows extremely good reductions around inequalities, which Tree_block relies on.  *)
+      let ( +@ ) = Infix.( +!!@ )
+      let ( -@ ) = Infix.( -!!@ )

Symbolic abstractions #131

Are you sure you want to change the base?

Symbolic abstractions #131

Uh oh!

Conversation

giltho commented Sep 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

N1ark left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

N1ark commented Sep 11, 2025

Uh oh!

giltho commented Sep 11, 2025

Uh oh!

giltho commented Sep 11, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

N1ark left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

giltho commented Dec 15, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

giltho commented Sep 10, 2025 •

edited

Loading

N1ark left a comment •

edited

Loading

giltho commented Dec 15, 2025 •

edited

Loading