433601 - Treehydra: need example ESP analysis

Status: RESOLVED WONTFIX

(Developer Infrastructure :: Source Code Analysis, defect)

Description

[David Mandelin [:dmandelin]]

Create a small ESP analysis application to show how to use the ESP framework and place it as a test case for Treehydra.

Comment 1

[David Mandelin [:dmandelin]]

Attachment: Rough draft

Here's the quick and dirty version so you can start reading it. It really needs the dependent bugs fixed before it's done. Also, it's not an actual test case yet.

The other deficiency (IMO) is that it's longer than I wanted it to be. A fair amount of it is "sort-of boilerplate", e.g., flowState, processAssign. What I mean is that that code is reusable for different analyses, but as designed, it does need to be modified for different analyses. It would be better engineered if there was an underlying abstract state space and transition that just takes care of stuff related to GCC control flow, int constants, etc., and the user just added customizations on top.

I'm not sure what's best yet. Hopefully this draft version is somewhat helpful, and readers/users can give suggestions on how to make it better.

Comment 2

[(dormant account)]

I'm trying to figure out how to iterate states in the exit block, but all of the variables appear to be set to BOTTOM by then. I haven't debugged as to why yet, but I did notice that the bottom parameter to Analysis does not seem to get used.

Comment 3

[(dormant account)]

nevermind about BOTTOM not being used.

Comment 4

[(dormant account)]

Seems that liveness analysis was screwing me up. Seems like we should setup the minimal esp example to be truly minimal. Took me a while to figure out all of the objects involved.
Of course the minimal analysis should be complemented with progressively more complicated analyses showing off the framework features.

Comment 5

[(dormant account)]

Also, i'm not sure why but switch cases do not appear to be visited. if statements seem to work.

Comment 6

[(dormant account)]

Seems that either esp.js should start using a custom value comparison func or makeIntAv should return ZERO/NONZERO...then switch() works fine.

Comment 7

[David Mandelin [:dmandelin]]

(In reply to comment #4)

Actually, the use of liveness information to drop state information should be customizable--in fact it had to be customized even for outparams. I think I'll retitle the bug on the deps to reflect that.

(In reply to comment #6)

Good catch. The source of the problem is that the abstract state machinery isn't using a true lattice, so the filter function doesn't know that a pair of states like "2" and "NONZERO" overlap. I'll file a bug for this.

Comment 8

[David Mandelin [:dmandelin]]

Attachment: Updated for recent libs bugfixes

Just an update to work with the changes made for the bugs this deps on.

Comment 9

[(dormant account)]

Please go ahead and commit this to the tests directory, it'll make it easier for me to work on this file too, instead of exchanging patches on bugzilla.

We'll make a test out of it later, so keep the bug open

Comment 10

[David Mandelin [:dmandelin]]

Agreed, pushed.

Comment 11

[(dormant account)]

So it doesn't look like we can keep the example fully featured and within 100lines, but at least the code is more concise..except for this the liveness stuff.

could the for loop around bb.keepVars = bb.stateIn; be moved into LivenessAnalysis?

Comment 12

[David Mandelin [:dmandelin]]

(In reply to comment #11)
> could the for loop around bb.keepVars = bb.stateIn; be moved into
> LivenessAnalysis?
 
As long as it is still separate from the liveness analysis, yes. I think it would be good to move that entire {} block in as a function 'initKeepVars' or 'initKeepVarsFromLiveness' or something like that. 

Comment 13

[Joshua Cranmer [:jcranmer]]

Dehydra and treehydra are no longer maintained by Mozilla.