Souffle VSA

[codyroux]

I'm trying to write a dead simple souffle Value Set Analysis for binaries, but I'm having a bit of trouble. Basically I want an abstract domain where the value of a register at a given point is:

1. A concrete integer if it is the only possible value
2. Top otherwise

I'm having trouble expressing this without (non-stratifiable) negation. Is there any sample code I could look at?

Thanks a bunch!

[langston-barrett]

@codyroux I think it will be very difficult (if not impossible) to express an infinite abstract domain like this in Datalog. If you have a finite abstract domain, then there is (an inefficient) way. Consider a constant propagation analysis with the abstract domain D consisting of all constant integers that appear in the program text. Then for each program statement, write the straightforward rules that propagate constants across them (e.g., if an addition has two constant operands and their sum is in D, then the result is that sum). At this point, each statement will be associated with some number of elements of the abstract domain. In a second "pass" or "phase" (in Datalog terms, a second stratum), you can count the number of domain elements associated with each statement, and replace them with Top if there are multiple, or pass the result through if there is just one. (To be clear, by "replace with...", I really mean "have a second relation with output...")

[thinkmoore]

I think you can improve on this a little using the recent "subsumption" feature added to souffle: https://souffle-lang.github.io/subsumption. Might look something like:

type Domain = Number { x : number } | Top {}

.decl value(var: symbol, val: Domain) btree_delete
.decl decl(var: symbol, val: number)
.decl add(res: symbol, var1: symbol, var2: symbol)

// Deal with constants
value(Var,$Number(Val)) :- decl(Var,Val).
value(Var,$Number(Result)) :- add(Var, Var1, Var2), value(Var1, $Number(Val1)), value(Var2, $Number(Val2)), Result = Val1 + Val2.

// Top always wins
value(Var,_) <= value(Var, $Top()) :- true.

// Multiple values implies Top
value(Var,$Top()) :- value(Var,$Number(V1)), value(Var,$Number(V2)), V1 != V2.

// Top propagates
value(Var,$Top()) :- add(Var, Var1, _Var2), value(Var1, $Top()).
value(Var,$Top()) :- add(Var, _Var1, Var2), value(Var2, $Top()).

.output value

decl("x", 1).
decl("y", 2).

add("a", "x", "y").
add("b", "x", "x").
add("c", "x", "y").
add("c", "y", "x").
add("d", "x", "x").
add("d", "y", "y").

[thinkmoore]

Outputs:

a	$Number(3)
x	$Number(1)
y	$Number(2)
b	$Number(2)
c	$Number(3)
d	$Top

[codyroux]

That does look promising! I've let this project fall a bit by the wayside, I'm afraid, but I'm going to try to get back on the horse and try this out!

[b-scholz]

I think this is possible using ADTs. Have you looked into this?

.type ADom = value { x:number} | bottom {} 

Can you provide more of the semantics you are interested in?

[codyroux]

@b-scholz I did try this, but ran into the following difficulty: naively trying to define a join(V1, V2, V3) predicate fails, as it does not ground the inputs: one would naively like the clauses join(V, bottom, V). (if we're using the "usual" lattice ordering).

This can probably be worked around, though I'd like to see an example rather than trying to come up with it on my own (as I am very lazy).

Thanks for the input!

[b-scholz]

Can you para-phrase a simple example of what you want to achieve / pseudo-code etc. so that I have an idea? I am happy to help.