Large diffs are not rendered by default.

This file was deleted.

@@ -170,126 +170,3 @@ def iterate(values, do_widen = True):
iterations > iterations_without_widening)
iterations += 1

if __name__ == '__main__':

boxes_factory = boxes.BoxDomainFactory(-128, 128)

# example bounds001.c

boxes_factory.add_var('index', -65536, 65536)
boxes_factory.add_var('length', -65536, 65536)
boxes_factory.add_var('access', -65536, 65536)

def bounds_001():

cfg = Method_CFG(1, 5)
cfg.add_control_loc(2)
cfg.add_control_loc(3)
cfg.add_control_loc(4)

cfg.set_edge(1, 2, None, [['length', [5]], ['access', [0]]])
cfg.set_edge(2, 3,
['>','index', 'length'],
[])
cfg.set_edge(3, 5,
None,
[['access', [ '-', 'index', 'length']]])

cfg.set_edge(2, 4,
['<=','index', 'length'],
[])
cfg.set_edge(4, 5,
None,
[['access', ['index']]])

print cfg.to_string()

cfg.forward_analyze(boxes_factory, boxes_factory.get_top(), boxes_factory.get_bot())


def bounds_002():

cfg = Method_CFG(1, 5)
cfg.add_control_loc(2)
cfg.add_control_loc(3)
cfg.add_control_loc(4)

cfg.set_edge(1, 2, None, [['length', [5]], ['access', [0]]])
cfg.set_edge(2, 3,
['>','index', 'length'],
[])
cfg.set_edge(3, 5,
None,
[['access', [ '-', 'length', 1]]])

cfg.set_edge(2, 4,
['<=','index', 'length'],
[])
cfg.set_edge(4, 5,
None,
[['access', ['index']]])

print cfg.to_string()
cfg.forward_analyze(boxes_factory, boxes_factory.get_top(), boxes_factory.get_bot())


def bounds_003():

cfg = Method_CFG(1, 6)
cfg.add_control_loc(2)
cfg.add_control_loc(3)
cfg.add_control_loc(4)
cfg.add_control_loc(5)

cfg.set_edge(1, 2, None, [['length', [5]], ['access', [0]]])
cfg.set_edge(2, 4,
['>','index', 'length'],
[])
cfg.set_edge(2, 3,
['<=','index', 'length'],
[])
cfg.set_edge(3, 4,
['<','index', 0],
[])
cfg.set_edge(3, 5,
['>=','index', 0],
[])

cfg.set_edge(4, 6,
None,
[['access', [ '-', 'length', 1]]])

cfg.set_edge(5, 6,
None,
[['access', ['index']]])


print cfg.to_string()
cfg.forward_analyze(boxes_factory, boxes_factory.get_top(), boxes_factory.get_bot())


def bounds_004():

cfg = Method_CFG(1, 3)
cfg.add_control_loc(2)

cfg.set_edge(1, 2, None, [['length', [5]], ['access', [0]]])
cfg.set_edge(2, 3,
None,
[['index', [ '%', 'index', 2]]])

print cfg.to_string()
cfg.forward_analyze(boxes_factory, boxes_factory.get_top(), boxes_factory.get_bot())

print "BOUNDS 001"
bounds_001()

print "BOUNDS 002"
bounds_002()

print "BOUNDS 003"
bounds_003()

print "BOUNDS 004"
bounds_004()

@@ -8,8 +8,6 @@
##############################


import boxes

# (I) Arithmetic expressions
#
# CONST
@@ -24,7 +22,6 @@
#
# No nested expressions supported yet.


#
# (II) Assignments
#
@@ -45,7 +42,7 @@
# ['<=', 'x', 'y']


class Method_CFG():
class MethodCFG():

def __init__(self, init_location, end_location):
self.control_locs = [init_location, end_location]
@@ -56,7 +53,6 @@ def __init__(self, init_location, end_location):

def to_string(self):
result = ''

for (s, t) in self.edges:
(cond, actions) = self.edges[(s, t)]
result += '%s -> %s \n\t' % (s, t)
@@ -97,7 +93,7 @@ def apply_assignment(assignment, value):
return dom.op_binary(value,
'+',
variable,
expression[0],
op1,
0)
elif len(expression) == 3:
(operator, op1, op2) = expression
@@ -1,11 +1,10 @@
import pytest

import graph_algorithms
import dbms
import dbm

def test_dbm_set_weight_get_weight():

d = dbms.DBM()
d = dbm.DBM()
d.set_weight(1, 3, 2)
assert d.get_weight(1, 2) == 3
d.set_weight(2, 4, 2)
@@ -27,7 +26,7 @@ def test_dbm_set_weight_get_weight():

def test_dbm_copy():

d = dbms.DBM()
d = dbm.DBM()
x = [1,2]
y = [3,4]
d.set_weight(1, x , 2)
@@ -37,15 +36,15 @@ def test_dbm_copy():

def test_dbm_exists_negative_cycle():

d1 = dbms.DBM()
d1 = dbm.DBM()
d1.set_weight(1, 1, 2)
d1.set_weight(2, -2, 1)
assert d1.exists_negative_cycle()
d2 = dbms.DBM()
d2 = dbm.DBM()
d2.set_weight(1, -2, 2)
d2.set_weight(2, 3, 1)
assert not d2.exists_negative_cycle()
d3 = dbms.DBM()
d3 = dbm.DBM()
for i in range(0, 500):
d3.set_weight(i, i*((-1)**(i % 2)), i+1)
d3.set_weight(500, 100, 50)
@@ -56,7 +55,7 @@ def test_dbm_exists_negative_cycle():
def test_dbm_find_shortest_paths():

# example from wikipedia, slightly extended
d1 = dbms.DBM()
d1 = dbm.DBM()
d1.set_weight(1, -2, 3)
d1.set_weight(3, 2, 4)
d1.set_weight(4, -1, 2)
@@ -5,17 +5,16 @@

def test_dbms_conditions_intersect_1():
factory = dbms.DBMFactory(-512, 512)
factory.add_var(0, 0, 0)
factory.add_var('x', -512, 512)
factory.add_var('y', -512, 512)
factory.add_var('z', -512, 512)
factory.add_integer_var(0, 0, 0)
factory.add_integer_var('x', -512, 512)
factory.add_integer_var('y', -512, 512)
factory.add_integer_var('z', -512, 512)

e1 = factory.get_top()
e2 = factory.get_top()
e3 = factory.get_top()
e4 = factory.get_top()


# e1: x = y && z > x
e1 = factory.cond_binary(e1, '==', 'x', 'y')
e1 = factory.cond_binary(e1, '>', 'z', 'x')
@@ -47,27 +46,24 @@ def test_dbms_conditions_intersect_1():
def test_dbms_operations_1():

factory = dbms.DBMFactory(-512, 512)
factory.add_var(0, 0, 0)
factory.add_var('x', -512, 512)
factory.add_var('y', -512, 512)
factory.add_var('z', -512, 512)
factory.add_integer_var(0, 0, 0)
factory.add_integer_var('x', -512, 512)
factory.add_integer_var('y', -512, 512)
factory.add_integer_var('z', -512, 512)

e1 = factory.get_top()
e2 = factory.get_top()
e3 = factory.get_top()
e4 = factory.get_top()

# e1: x > y

# e1 := x > y
e1 = factory.cond_binary(e1, '>', 'x', 'y')

# z = x
# e1 := e1 and z = x
e1 = factory.op_binary(e1, '+', 'z', 'x', 0)
print factory.to_string(factory._normalize(e1))

# now: z < y should be impossible
e2 = factory.cond_binary(e1, '<', 'z', 'y')

assert factory.is_eq(e2,
factory.get_bot())
print factory.to_string(factory._normalize(e2))
assert factory.is_eq(e2, factory.get_bot())


@@ -2,9 +2,5 @@ int main()
{
int x;
int y;
if (x > y)
{
if (x < y)
{ x = 1000; }
}
x = y % 10;
}