|
|
|
This is a small intro to the savage tool.
|
|
|
|
It's an allusion to the generated svg (SaVaGe) and the "wild" nature of SDE's execution, if one doesn't see the underlying vstate structure.
|
|
|
|
|
|
|
|
Savage reads a KleeNet Log (.knl) file and visualises a real run of KleeNet on actual code.
|
|
|
|
|
|
|
|
### Less talk more fancy pictures
|
|
|
|
|
|
|
|
Savage creates both animated and static [SVG 1.1](http://www.w3.org/TR/SVG/) pictures. To view this, you require a user agent that supports svg. As of this writing opera is the only web-browser capable of correctly displaying svg animations. The following static svg might display correctly in other browsers, too. Who knows.
|
|
|
|
|
|
|
|
*Note: The svgs seem not to be served correctly. You may experience problems with displaying them directly from the server.* **Download them and open them locally!**
|
|
|
|
|
|
|
|
[Static SVG](https://code.comsys.rwth-aachen.de/redmine/attachments/241/static.svg)
|
|
|
|
|
|
|
|
[Animated SVG](https://code.comsys.rwth-aachen.de/redmine/attachments/242/log.svg)
|
|
|
|
|
|
|
|
[Rendered Video in the Ogg-Video format](https://code.comsys.rwth-aachen.de/redmine/attachments/243/animation-render.ogv)
|
|
|
|
|
|
|
|
```
|
|
|
|
wget 'https://code.comsys.rwth-aachen.de/redmine/attachments/242/log.svg' -O /tmp/log.svg && opera /tmp/log.svg
|
|
|
|
```
|
|
|
|
|
|
|
|
|
|
|
|
If your browser cannot correctly display the svgs, check out the ogg video to get an impression of how it would look like on the [Presto](http://en.wikipedia.org/wiki/Presto_(layout_engine)) engine.
|
|
|
|
|
|
|
|
#### State Mapping Algorithms
|
|
|
|
Here is a comparison (of a slightly modified scenario) of the COW and SDS state mapping algorithm:
|
|
|
|
|
|
|
|
[Copy-on-Write Algorithm](https://code.comsys.rwth-aachen.de/redmine/attachments/244/log-cow.svg)
|
|
|
|
|
|
|
|
[Super-Distributed-State Algorithm](https://code.comsys.rwth-aachen.de/redmine/attachments/245/log-sds.svg)
|
|
|
|
|
|
|
|
```
|
|
|
|
wget 'https://code.comsys.rwth-aachen.de/redmine/attachments/244/log-cow.svg' -O /tmp/log-cow.svg && opera /tmp/log-cow.svg
|
|
|
|
wget 'https://code.comsys.rwth-aachen.de/redmine/attachments/245/log-sds.svg' -O /tmp/log-sds.svg && opera /tmp/log-sds.svg
|
|
|
|
```
|
|
|
|
|
|
|
|
### Mobile World Congress Demo
|
|
|
|
Here is the demo we presented on the [MWC'13](http://www.mobileworldcongress.com/)
|
|
|
|
|
|
|
|
#### Build yourself
|
|
|
|
```
|
|
|
|
wget 'https://code.comsys.rwth-aachen.de/redmine/attachments/246/mwc.knl' -O mwc.knl && $KLEE/tools/savage -i mwc.knl -o mwc.svg && opera mwc.svg
|
|
|
|
```
|
|
|
|
|
|
|
|
#### Download built svg
|
|
|
|
```
|
|
|
|
wget 'https://code.comsys.rwth-aachen.de/redmine/attachments/247/mwc.svg' -O mwc.svg && opera mwc.svg
|
|
|
|
```
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
[mwc.knl](uploads/ee4858a65da5518b8fbf970b42e23e0c/mwc.knl)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
 |
|
|
|
\ No newline at end of file |
