name
jpf/jpf-mango
description
unknown
owner
Mercurial Server
last change
Sat, 22 Feb 2014 19:49:04 -0500

Changes

2014-02-22 frank Removed demo, this belongs on the wiki default tip changeset | files
2014-02-20 frank Successful spec of Android sample code on 8gb laptop. Changed update site for zest, as it is now part of the integrated GEF4 Eclipse build. changeset | files
2014-02-20 frank TODO: get per-vulnerability dev projects up to date and make demo slides. changeset | files
2014-02-19 frankrimlinger Actually, deleted upload because it was incomplete. The new upload is called Bundle1667, because, when specified using the baseline 1667 changeset, it will replicate the demo stats. changeset | files
2014-02-19 frankrimlinger Clean link and spec of all five Android examples. Added localVar translation rule, PMinstall code fix. With this in place, clean link and spec of FirstYearCode. Uploaded spec as wiki SampleSpecBundle, a hefty 100MB, but for the record. Added Demo folder in documentation, with stats for this work, together with preferences used. (Of course, mileage will vary with changing preferences.) Removed unsatisfiable warning pref, it is now always on. TODO: review of the three vulnerabilities, confidential info, closer, and finalizer in prep for demo. changeset | files
2014-02-18 frankrimlinger Actually, there is a case where a patch method is not opaque, which arises during spec of SampleSyncAdapter. If the patch method is forced, then it may have a concrete spec, for example, anroid.database.Cursor.close()V is an interface, and its need for a patch is only discovered during specification, and it patches to the supplied approximation method java.io.Closable$Proxy.close(), which may or may not have been specified at the time it is discovered. If not, then spec must halt with replay advice. However, imagining the supplied approximation would involve the caller in a mutually co-recursive system is a bridge too far, so advice changed to just indicate a replay is necessary. On the other hand, if the spec exists, then fixed to proceed silently. This all goes down in Invoke.getMethod(). With this in place, clean two-pass link, spec of SampleSyncAdapter, with no unsatisfiable condition raised. Clean exhaust of NetworkUtilities.syncContacts, with 10 case, 7 of which had hot spots. The second link pass is to add native approximations for HttpClient, Uri, and Window. Spec takes about 30 minutes on a 64gb machine, although 32gb would probably be ample. The sample exhaust takes about 2 minutes, but a lower hotspot rate would of course require more time. This concludes the general development of Mango. Further feature development and tuning will be vulnerability specific. TODO: Acquire similar statistics for each project, and create demo. NOTE: The persistence bug for Patch List is not reproducible. Probably the internal persistent metadata on the laptop is broken somehow. changeset | files
2014-02-18 frankrimlinger Removed the code in the ContainsMethod action and the Resolves action causing dropped assumption if there was only one apparent resolution. Technically, this drop could be made "safe" by having resolve virtual method return status information about "why" the resolution set was a singleton. Punting on this for now. Fixed bug in Invoke.filterChoices, must check for maxCanddiates==0, which means maxCandidates is infinity. With this in place, the TestTime "works", in the sense that the approximation assumption does appear. It "should" have falsified, but apparently the compile time type was used to resolve the approximation assumptions. This really needs more work, but punting for now. NOTE: there is no danger of a patch choice being non-opaque. This is the whole point of building the class hierarchy of the source project, to populate the uniqueMap so that any non-opaque choice is *always* detected. Therefore, any patch or witness will necessarily have or require opaque spec. So the code to handle the non-opaque case can be dropped, but punting on this for now. TODO: attempt spec and spot exhaust of SampleSyncAdapter. changeset | files
2014-02-18 frankrimlinger Reinstated ClassResolver update from 1657, which enforces the "ForceMatch trumps required root" logic. changeset | files
2014-02-17 frank Addendum to sync: Actually, once a resolveVirtualMethod has been harvested and installed in a FreeChoice, there is no going back, not even in the driver SymbolHash. So the correct solution is to just swap out the resolveVirtualMethod rulekey for the resolveVirtualPatch rulekey. The understanding is that resolveVirtualPatch can only falsify if the two classes do not share a common ancestor, which probably would be a bug anyway. However, if resolveVirtualPatch would be false in the java interpretation, then translate by throwing in the word "approximation". This is the best compromise. changeset | files
2014-02-17 frank Reverted to 1654. The plan1659, if followed through, would lead to a ForceMatch for *every* virtual invocation. Not really a good idea. The assertion of 1655, that the "patch method" is unworkable, is also debatable. The patch method is a good dynamic solution during specification, and supplies a representative execution path during testing in the event the actual invoked method is unknown. The problem, as pointed out in 1654, is that the virtual resolution predicate may not be generated in the first place, creating misleading results. This is just a bug. But even worse, if generated, it may falsify if the method is known, leading to coverage bias. TODO: 1. ensure that the virtual resolution predicate is *always* generated. If there is enough information, it will rewrite to true and disappear anyway. 2. If a resolveVirtualMethod assumption falsifies during specification, then a patch can be created which is correct. This is a good thing. 3. If a resolveVirtualMethod falsifies during testing, the show must go on. Instead of rewriting to false and causing a commotion, rewrite to (patchInvocation objectRef unique patchMethod). This can translate as "objectRef.unique resolves to the approximation patchMethod". Then the user can fiddle with the patch list if required to redirect the simulation, or not. NOTE: this is the first time different driver versus non-driver SymbolHashes have offered differing rulekey semantics, but so what? changeset | files
...

Tags

...
2014-02-22 c8a7428795bc default changeset | changelog | files
...

mercurial