Skip to content

Instantly share code, notes, and snippets.

@teodorslisovenko

teodorslisovenko/Signs.java

Created June 3, 2025 15:12
Show Gist options
  • Save teodorslisovenko/64c015ad9c76dd58b18c907a312f8215 to your computer and use it in GitHub Desktop.
Save teodorslisovenko/64c015ad9c76dd58b18c907a312f8215 to your computer and use it in GitHub Desktop.
Download ZIP
LiSA analysing in Sign domain
Raw
loop.html
<html>
<head>
<title>untyped signs::loop(signs* this)</title>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width, user-scalable=no, initial-scale=1, maximum-scale=1" />
<script src="https://cdnjs.cloudflare.com/ajax/libs/cytoscape/3.21.1/cytoscape.min.js"></script>
<script src="https://code.jquery.com/jquery-3.0.0.min.js"></script>
<script src="https://cdn.jsdelivr.net/gh/iVis-at-Bilkent/cytoscape.js-graphml@master/cytoscape-graphml.js"></script>
<style>
body {
font-family: helvetica neue, helvetica, liberation sans, arial,
sans-serif;
font-size: 14px;
background-color: white;
}
html, body, #full {
height: 100%;
}
#full {
display: flex;
flex-direction: row;
}
#cy {
flex-grow: 0.5;
z-index: 10;
max-width: 70%;
}
#header {
position: fixed;
z-index: 11;
overflow-x: hidden;
}
#header div {
background-color: #e2e2e2;
padding: 20px 15px;
margin-bottom: 10px;
}
#header div b {
padding: 6px 0;
color: #333333;
display: block;
cursor: pointer;
}
#header div span {
padding: 6px 0;
display: block;
}
#header div span label b {
padding: 0;
display: inline;
}
#header div span input {
margin: 0;
}
#descriptions {
flex-grow: 0.5;
z-index: 11;
overflow: auto;
font-size: 18px;
border-left: 2px solid #e2e2e2;
padding-left: 20px;
}
.description-header {
font-weight: bold;
}
#descriptions ul {
padding-left: inherit;
margin: 5px 0;
}
.description-nest {
padding-left: 15px;
}
.header-hidden {
display: none;
}
.description-title-wrapper {
margin-top: 0.83em;
margin-bottom: 0.83em;
}
.description-title {
font-size: 1.5em;
font-weight: bold;
}
.description-title-text {
font-size: 1.5em;
font-family: monospace;
}
#header-none {
margin-top: 0.83em;
margin-bottom: 0.83em;
}
.no-results {
border: solid 2px #FF0000;
background-color: #FF000040;
}
</style>
</head>
<body>
<h1>untyped signs::loop(signs* this)</h1>
<h3></h3>
<hr />
<div id="full">
<div id="header">
<div>
<b>Node border: <font color="darkgray">gray</font>, single</b>
<b>Entrypoint border: black, single</b>
<b>Exitpoint border: black, double</b>
<b>Sequential edge: black, solid</b>
<b>False edge: <font color="red">red</font>, solid</b>
<b>True edge: <font color="blue">blue</font>, solid</b>
</div>
<div>
<input id="search" type="text" placeholder="Search node.."/>
<input id="next" type="button" value="Next" disabled/>
<input id="prev" type="button" value="Previous" disabled/>
<b id="relayout">Run layout</b>
<b id="fit">Fit to viewport</b>
</div>
</div>
<div id="cy"></div>
<div id="descriptions">
<div id="header-none">
No node selected. Select a node to show its results.
</div>
<div id="header-node0" class="header-hidden">
<div class="description-title-wrapper"><span class="description-title">Results for </span><span class="description-title-text">c = 1</span></div>
<span class="description-header">expressions: </span>[c]<br/>
<span class="description-header">state: </span><br/>
<div class="description-nest">
<span class="description-header">heap: </span>monolith<br/>
<span class="description-header">type: </span><br/>
<div class="description-nest">
<span class="description-header">c: </span>[int32]<br/>
<span class="description-header">this: </span>[signs*]<br/>
</div>
<span class="description-header">value: </span><br/>
<div class="description-nest">
<span class="description-header">c: </span>+<br/>
</div>
</div>
</div>
<div id="header-node3" class="header-hidden">
<div class="description-title-wrapper"><span class="description-title">Results for </span><span class="description-title-text">b = 0</span></div>
<span class="description-header">expressions: </span>[b]<br/>
<span class="description-header">state: </span><br/>
<div class="description-nest">
<span class="description-header">heap: </span>monolith<br/>
<span class="description-header">type: </span><br/>
<div class="description-nest">
<span class="description-header">b: </span>[int32]<br/>
<span class="description-header">c: </span>[int32]<br/>
<span class="description-header">this: </span>[signs*]<br/>
</div>
<span class="description-header">value: </span><br/>
<div class="description-nest">
<span class="description-header">b: </span>0<br/>
<span class="description-header">c: </span>+<br/>
</div>
</div>
</div>
<div id="header-node6" class="header-hidden">
<div class="description-title-wrapper"><span class="description-title">Results for </span><span class="description-title-text"><(b, 10)</span></div>
<span class="description-header">expressions: </span>[b < 10]<br/>
<span class="description-header">state: </span><br/>
<div class="description-nest">
<span class="description-header">heap: </span>monolith<br/>
<span class="description-header">type: </span><br/>
<div class="description-nest">
<span class="description-header">b: </span>[int32]<br/>
<span class="description-header">c: </span>[int32]<br/>
<span class="description-header">this: </span>[signs*]<br/>
</div>
<span class="description-header">value: </span><br/>
<div class="description-nest">
<span class="description-header">b: </span>#TOP#<br/>
<span class="description-header">c: </span>+<br/>
</div>
</div>
</div>
<div id="header-node9" class="header-hidden">
<div class="description-title-wrapper"><span class="description-title">Results for </span><span class="description-title-text">b = +(b, c)</span></div>
<span class="description-header">expressions: </span>[b]<br/>
<span class="description-header">state: </span><br/>
<div class="description-nest">
<span class="description-header">heap: </span>monolith<br/>
<span class="description-header">type: </span><br/>
<div class="description-nest">
<span class="description-header">b: </span>[int32]<br/>
<span class="description-header">c: </span>[int32]<br/>
<span class="description-header">this: </span>[signs*]<br/>
</div>
<span class="description-header">value: </span><br/>
<div class="description-nest">
<span class="description-header">b: </span>#TOP#<br/>
<span class="description-header">c: </span>+<br/>
</div>
</div>
</div>
<div id="header-node14" class="header-hidden">
<div class="description-title-wrapper"><span class="description-title">Results for </span><span class="description-title-text">return b</span></div>
<span class="description-header">expressions: </span>[ret_value@loop]<br/>
<span class="description-header">state: </span><br/>
<div class="description-nest">
<span class="description-header">heap: </span>monolith<br/>
<span class="description-header">type: </span><br/>
<div class="description-nest">
<span class="description-header">b: </span>[int32]<br/>
<span class="description-header">c: </span>[int32]<br/>
<span class="description-header">ret_value@loop: </span>[int32]<br/>
<span class="description-header">this: </span>[signs*]<br/>
</div>
<span class="description-header">value: </span><br/>
<div class="description-nest">
<span class="description-header">b: </span>#TOP#<br/>
<span class="description-header">c: </span>+<br/>
<span class="description-header">ret_value@loop: </span>#TOP#<br/>
</div>
</div>
</div>
</div>
</div>
<script>
var api;
var layoutOptions;
var cy = window.cy = cytoscape({
container: $('#cy'),
maxZoom: 100,
zoomingEnabled: true,
userZoomingEnabled: true,
style: [
{
selector: 'node',
css: {
'background-color': 'white',
'color': 'black',
'shape': 'rectangle',
'border-width': '1px',
'border-style': 'solid',
'border-color': 'darkgray',
'content': 'data(NODE_TEXT)',
'font-family': 'monospace',
'font-size': '18px',
'font-weight': 'bold',
'text-wrap': 'wrap',
}
},
{
selector: 'node[NODE_IS_ENTRY = "yes"]',
css: {
'border-width': '3px',
'border-style': 'solid',
'border-color': 'black',
}
},
{
selector: 'node[NODE_IS_EXIT = "yes"]',
css: {
'border-width': '5px',
'border-style': 'double',
'border-color': 'black',
}
},
{
selector: 'node:selected',
css: {
'border-color': 'orange',
'border-width': '2px',
}
},
{
selector: 'edge',
css: {
'curve-style': 'bezier',
'width': 4,
'line-color': 'black',
'target-arrow-shape': 'triangle',
'target-arrow-color': 'black',
'arrow-scale': '2'
}
},
{
selector: 'edge[EDGE_KIND = "TrueEdge"]',
css: {
'line-color': 'blue',
'target-arrow-color': 'blue',
}
},
{
selector: 'edge[EDGE_KIND = "FalseEdge"]',
css: {
'line-color': 'red',
'target-arrow-color': 'red',
}
},
],
ready: function () {
var data = '<?xml version="1.0" encoding="UTF-8"?><graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://graphml.graphdrawing.org/xmlns http://graphml.graphdrawing.org/xmlns/1.0/graphml.xsd"><key id="NODE_IS_ENTRY" for="node" attr.name="NODE_IS_ENTRY" attr.type="string"/><key id="NODE_IS_EXIT" for="node" attr.name="NODE_IS_EXIT" attr.type="string"/><key id="NODE_TEXT" for="node" attr.name="NODE_TEXT" attr.type="string"/><key id="EDGE_KIND" for="edge" attr.name="EDGE_KIND" attr.type="string"/><graph id="graph" edgedefault="directed"><node id="node0"><data key="NODE_IS_ENTRY">yes</data><data key="NODE_TEXT">c = 1</data><data key="NODE_IS_EXIT">no</data></node><node id="node3"><data key="NODE_IS_ENTRY">no</data><data key="NODE_TEXT">b = 0</data><data key="NODE_IS_EXIT">no</data></node><node id="node6"><data key="NODE_IS_ENTRY">no</data><data key="NODE_TEXT">&lt;(b, 10)</data><data key="NODE_IS_EXIT">no</data></node><node id="node9"><data key="NODE_IS_ENTRY">no</data><data key="NODE_TEXT">b = +(b, c)</data><data key="NODE_IS_EXIT">no</data></node><node id="node14"><data key="NODE_IS_ENTRY">no</data><data key="NODE_TEXT">return b</data><data key="NODE_IS_EXIT">yes</data></node><edge id="edge-0-3" source="node0" target="node3" directed="true"><data key="EDGE_KIND">SequentialEdge</data></edge><edge id="edge-3-6" source="node3" target="node6" directed="true"><data key="EDGE_KIND">SequentialEdge</data></edge><edge id="edge-6-9" source="node6" target="node9" directed="true"><data key="EDGE_KIND">TrueEdge</data></edge><edge id="edge-6-14" source="node6" target="node14" directed="true"><data key="EDGE_KIND">FalseEdge</data></edge><edge id="edge-9-6" source="node9" target="node6" directed="true"><data key="EDGE_KIND">SequentialEdge</data></edge></graph></graphml>'
this.graphml({layoutBy: null});
this.graphml(data);
layoutOptions = {
name: 'breadthfirst',
fit: false,
directed: true,
spacingFactor: 2.5,
};
var layout = this.layout(layoutOptions);
if (layout && layout.run) {
layout.run();
}
this.fit();
}
});
function relayout() {
var layout = cy.layout(layoutOptions);
if (layout && layout.run) {
layout.run();
}
}
$('#relayout').on('click', function () {
relayout();
});
$('#fit').on('click', function () {
cy.fit(cy.nodes(), 50);
});
var lastsearchresult = [];
var lastshownelement = -1;
function centerToSearch() {
var target = lastsearchresult[lastshownelement];
cy.$('node:selected').unselect();
target.select();
cy.animate({ center: { eles: target } }, { duration: 0 });
}
$('#search').on('input', function (e) {
var query = e.target.value;
lastsearchresult = cy.nodes('[NODE_TEXT @*= "' + query + '"]');
var hasresults = lastsearchresult.size() != 0;
if (hasresults) {
lastshownelement = 0;
centerToSearch();
e.target.classList.remove('no-results');
} else {
lastshownelement = -1;
cy.$('node:selected').unselect();
e.target.classList.add('no-results');
}
if (query === "" || !hasresults) {
$('#next').prop('disabled', true);
$('#prev').prop('disabled', true);
} else {
$('#next').prop('disabled', false);
$('#prev').prop('disabled', false);
}
});
$('#next').on('click', function (e) {
if (lastshownelement != -1) {
lastshownelement = (lastshownelement + 1) % lastsearchresult.size();
centerToSearch();
}
});
$('#prev').on('click', function (e) {
if (lastshownelement != -1) {
lastshownelement = ((lastshownelement - 1) + lastsearchresult.size()) % lastsearchresult.size();
centerToSearch();
}
});
cy.on('select', 'node', function(event) {
var id = event.target.id();
$('[id^=header-]').addClass('header-hidden');
$('#header-' + id).removeClass('header-hidden');
});
</script>
</body>
</html>
Raw
signs.imp
class signs {
loop() {
def c = 1;
def b = 0;
while (b < 10)
b = b + c;
return b;
}
basic() {
def i = 2;
def j = -10;
def a = i + j;
def s = i - j;
def m = i * j;
def d = i / j;
}
branches() {
def a = 3;
def b = 5;
def x = 0;
if (a > b)
x = x * 7;
else
x = -7;
def y = x / x;
}
}
Raw
Signs.java
package it.unive.scsr;
import it.unive.lisa.analysis.Lattice;
import it.unive.lisa.analysis.SemanticException;
import it.unive.lisa.analysis.SemanticOracle;
import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain;
import it.unive.lisa.program.cfg.ProgramPoint;
import it.unive.lisa.symbolic.value.Constant;
import it.unive.lisa.symbolic.value.operator.AdditionOperator;
import it.unive.lisa.symbolic.value.operator.DivisionOperator;
import it.unive.lisa.symbolic.value.operator.MultiplicationOperator;
import it.unive.lisa.symbolic.value.operator.SubtractionOperator;
import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator;
import it.unive.lisa.symbolic.value.operator.unary.NumericNegation;
import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator;
import it.unive.lisa.util.representation.StringRepresentation;
import it.unive.lisa.util.representation.StructuredRepresentation;
public class Signs
// instances of this class are lattice elements such that:
// - their state (fields) hold the information contained into a single
// variable
// - they provide logic for the evaluation of expressions
implements
BaseNonRelationalValueDomain<
// java requires this type parameter to have this class
// as type in fields/methods
Signs> {
// as this is a finite lattice, we can optimize by having constant elements
// for each of them
private static final Signs BOTTOM = new Signs("BOT");
private static final Signs NEGATIVE = new Signs("NEG");
private static final Signs ZERO = new Signs("ZERO");
private static final Signs POSITIVE = new Signs("POS");
private static final Signs TOP = new Signs("TOP");
// this is just needed to distinguish the elements
private final String sign;
public Signs() {
this("TOP");
}
public Signs(
String sign) {
this.sign = sign;
}
@Override
public boolean equals(
Object obj) {
if (this == obj)
return true;
if (obj == null)
return false;
if (getClass() != obj.getClass())
return false;
Signs other = (Signs) obj;
if (sign != other.sign)
return false;
return true;
}
@Override
public Signs top() {
// the top element of the lattice
// if this method does not return a constant value,
// you must override the isTop() method!
return TOP;
}
@Override
public Signs bottom() {
// the bottom element of the lattice
// if this method does not return a constant value,
// you must override the isBottom() method!
return BOTTOM;
}
@Override
public Signs lubAux(
Signs other)
throws SemanticException {
// this and other are always incomparable when we reach here
return TOP;
}
@Override
public boolean lessOrEqualAux(
Signs other)
throws SemanticException {
// this and other are always incomparable when we reach here
return false;
}
@Override
public StructuredRepresentation representation() {
if (this == TOP)
return Lattice.topRepresentation();
if (this == BOTTOM)
return Lattice.bottomRepresentation();
if (this == POSITIVE)
return new StringRepresentation("+");
if (this == NEGATIVE)
return new StringRepresentation("-");
return new StringRepresentation("0");
}
// logic for evaluating expressions below
@Override
public Signs evalNonNullConstant(
Constant constant,
ProgramPoint pp,
SemanticOracle oracle)
throws SemanticException {
if (constant.getValue() instanceof Integer) {
int v = (Integer) constant.getValue();
if (v > 0)
return POSITIVE;
else if (v == 0)
return ZERO;
else
return NEGATIVE;
}
return top();
}
private Signs negate() {
if (this == NEGATIVE)
return POSITIVE;
else if (this == POSITIVE)
return NEGATIVE;
else
return this;
}
@Override
public Signs evalUnaryExpression(
UnaryOperator operator,
Signs arg,
ProgramPoint pp,
SemanticOracle oracle)
throws SemanticException {
if (operator instanceof NumericNegation)
return arg.negate();
return TOP;
}
@Override
public Signs evalBinaryExpression(
BinaryOperator operator,
Signs left,
Signs right,
ProgramPoint pp,
SemanticOracle oracle)
throws SemanticException {
if (operator instanceof AdditionOperator) {
if (left == NEGATIVE) {
if (right == ZERO || right == NEGATIVE)
return left;
else
return TOP;
} else if (left == POSITIVE) {
if (right == ZERO || right == POSITIVE)
return left;
else
return TOP;
} else if (left == ZERO) {
return right;
} else
return TOP;
} else if (operator instanceof SubtractionOperator) {
if (left == NEGATIVE) {
if (right == ZERO || right == POSITIVE)
return left;
else
return TOP;
} else if (left == POSITIVE) {
if (right == ZERO || right == NEGATIVE)
return left;
else
return TOP;
} else if (left == ZERO) {
return right;
} else
return TOP;
} else if (operator instanceof MultiplicationOperator) {
if (left == NEGATIVE) {
return right.negate();
} else if (left == POSITIVE) {
return right;
} else if (left == ZERO) {
return ZERO;
} else
return TOP;
} else if (operator instanceof DivisionOperator) {
if (right == ZERO)
return BOTTOM;
if (left == NEGATIVE) {
return right.negate();
} else if (left == POSITIVE) {
return right;
} else if (left == ZERO) {
return ZERO;
} else
return TOP;
}
return TOP;
}
@Override
public int hashCode() {
return sign.hashCode();
}
}
Raw
test.java
package it.unive.scsr;
import org.junit.Test;
import it.unive.lisa.AnalysisException;
import it.unive.lisa.DefaultConfiguration;
import it.unive.lisa.LiSA;
import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
import it.unive.lisa.conf.LiSAConfiguration;
import it.unive.lisa.conf.LiSAConfiguration.GraphType;
import it.unive.lisa.imp.IMPFrontend;
import it.unive.lisa.imp.ParsingException;
import it.unive.lisa.program.Program;
public class SignsTest {
@Test
public void testSigns() throws ParsingException, AnalysisException {
// we parse the program to get the CFG representation of the code in it
Program program = IMPFrontend.processFile("inputs/signs.imp");
// we build a new configuration for the analysis
LiSAConfiguration conf = new DefaultConfiguration();
// we specify where we want files to be generated
conf.workdir = "outputs/sign";
// we specify the visual format of the analysis results
conf.analysisGraphs = GraphType.HTML;
// we specify the analysis that we want to execute
conf.abstractState = DefaultConfiguration.simpleState(
DefaultConfiguration.defaultHeapDomain(),
new ValueEnvironment<>(new Signs()),
DefaultConfiguration.defaultTypeDomain());
// we instantiate LiSA with our configuration*/
LiSA lisa = new LiSA(conf);
// finally, we tell LiSA to analyze the program
lisa.run(program);
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment