Boxed octagon and test framework #12

ptal · 2018-12-07T11:13:23Z

A first draft of the boxed octagon abstract domain on floating bound as described in the thesis of Marie (Pelleau, 2012), also with a closure algorithm described in (Bagnara, 2009) -- however it does not work for floating point numbers (will be useful for integers and rational though).
Drawer for octagon.
Add the test framework with alcotest, closing issue Choosing a testing library for AbSolute #6
Add meet_var for boxes in order to meet a value in a specific variable.
Add an icon for Travis in the README, closing issue Continuous integration service (travis) #9

…domain.

…rshall along with the box representation of the DBM (yet untested).

… communicating information between the boxes intersection and the DBM.

…octagonalisation strategies.

…functions (to meet the dbm into the boxes).

…nara et al., 2009) and add the optimization appearing in the same paper.

…e the easy way of relying on abstract box (for now)).

… base = (0,0)). Fix index bugs in the closure algorithm, and correct the Bagnara version by using a classical Floyd Washall algorithm.

…ition of LB and UB.

…nvertion from DBM to BOX and vice-versa.

…ix bugs.

…nts, tests and fix bugs.

…d in the DBM instead of filtering them in boxes.

…int extraction function.

… checker framework.

… than in boxes.

…r floating point computation.

…resentation of octagon. Rewriter now holds the mapping between var and dbm_interval.

… modularity. Incremental closure is working.

…ark run.

…e the strategies to avoid incompatibilities.

…gies.

…egies.

…several files depends on it).

…Prepare to implement the DBM as a functional array.

…ute MiniZinc model (flatten and with any model).

… is unsat.

…in a database.

…t can be imperative or functional.

…y absolute-bench.

ptal added 30 commits September 29, 2018 14:59

[abstract domain][octagon] Base files for the boxed octagon abstract …

291f8b1

…domain.

[abstract domain][octagon] implement the 'easy' functions on the DBM.

011e712

merge conflicts.

3db20c5

[abstract domain][octagon] implement the modified version of Floyd Wa…

cf1fd1b

…rshall along with the box representation of the DBM (yet untested).

[abstract domain][octagon] add a first filter procedure and functions…

4eaaf65

… communicating information between the boxes intersection and the DBM.

[abstract domain][octagon] add infrastructure to specify a split and …

ffb2848

…octagonalisation strategies.

[abstract domain][octagon] Add rotated boxes, and generalize several …

7c2fe10

…functions (to meet the dbm into the boxes).

[abstract domain][octagon] Add rotated constraints and their filtering.

254f4c4

[abstract domain][octagon] Decompose the closure algorithm as in (Bag…

c286e4c

…nara et al., 2009) and add the optimization appearing in the same paper.

[abstract domain][octagon] Implement missing functions (sometimes tak…

535520e

…e the easy way of relying on abstract box (for now)).

merge upstream.

e50ab72

merge upstream

8ae0173

[travis] Add an initial Travis file for continuous integration.

7c1beff

[travis][readme] Add the icon for Travis build.

5a51c1f

[travis] fix travis build using docker.

afc962a

merge upstream

1e4be39

Merge remote-tracking branch 'upstream/master'

c012b4d

[test] Add tests infrastructure using the framework Alcotest.

1ffaa96

[abstract domain][octagon] Change base option to base (with canonical…

7f3383c

… base = (0,0)). Fix index bugs in the closure algorithm, and correct the Bagnara version by using a classical Floyd Washall algorithm.

[abstract domain][octagon][test] add tests of functions computing pos…

910cca8

…ition of LB and UB.

[BoxedOctagon][refactor] Use only one box for all planes. Test the co…

2c6235f

…nvertion from DBM to BOX and vice-versa.

[octagon][tests] Test adding a variable and a plane in the octagon, f…

52e93aa

…ix bugs.

[octagon][tests] Closure of the DBM and filtering of rotated constrai…

3d84109

…nts, tests and fix bugs.

[BoxedOctagon] Detect octagonal constraints and directly set the boun…

fc5c111

…d in the DBM instead of filtering them in boxes.

[BoxedOctagon] Add join and meet operators and test them.

8db5d3b

[BoxedOctagon] Implement is_representable using the octagonal constra…

9efdd98

…int extraction function.

[BoxedOctagon] Implement all the functions and test them. Link to the…

c32bfa9

… checker framework.

[BoxedOctagon] implemented is_abstraction with a better approximation…

b91ef9e

… than in boxes.

merge with master.

d57cbdc

[BoxedOctagon] Fix a bug in which bagnara closure was wrongly used fo…

fce1468

…r floating point computation.

ptal added 29 commits March 15, 2019 16:25

[octagon][rewriting] Refactor rewriting to use the new constraint rep…

7adce62

…resentation of octagon. Rewriter now holds the mapping between var and dbm_interval.

[refactoring] Fix various bugs in box-octagon and refactor for better…

cfc4fb2

… modularity. Incremental closure is working.

[octagon] Add a reverse bisection, and more information on the benchm…

60dac66

…ark run.

[octagon][splitting] Fix bugs in splitting strategies, better organiz…

cefe403

…e the strategies to avoid incompatibilities.

[benchmark] Benchmark of several domains with different search strate…

8e1f15b

…gies.

[octagon][split] Fix a bug on min max split. Predefined various strat…

3e2d040

…egies.

[octagon] Add an old version of octagon to avoid broken compilation (…

bc86b9e

…several files depends on it).

[octagon] Add several search strategies on min/max LB/UB.

808fc44

[octagon] Change the DBM and closure interface for a functional one. …

5a4a93a

…Prepare to implement the DBM as a functional array.

[octagon] Shorter version of the entailment operation.

865fa7b

[benchmark] Output MiniZinc results with the CSV format.

9e02f78

[DBM][Persistent] Add a persistent DBM using Filliatre persistent array.

21914a8

[benchmark] Fix a bug when computing the horizon. Add support to exec…

2247c2b

…ute MiniZinc model (flatten and with any model).

[benchmark] Fix some problems with the MiniZinc output when the model…

787781b

… is unsat.

[benchmark][data] Organize the data for benchmarks and store results …

3f4c13a

…in a database.

Add optimisation flags to compile with flambda activated.

61280da

Merge branch 'master' of https://github.com/ptal/AbSolute

d9d6042

[Octagon][restoration strategy] Parametrize the DBM with an array tha…

1a501cc

…t can be imperative or functional.

Add data from the Patterson benchmark.

4ed92e9

merge conflicts.

1896cf4

[Octagon][Branching] Add the MSLF strategy with tie-breaking.

2087b0d

[benchmark] Add MiniZinc model with smallest search annotation.

ca3f8b0

merge conflicts.

6c61503

Merge branch 'master' of https://github.com/ptal/AbSolute

54284d6

[Benchmarks][database] Add benches on Patterson instances and J30.

55a9395

[benchmark][database] Update the benches for UBO100 and J30.

00b9189

[benchmarks] Unify the format of the database files and add optimum.

dde88b6

[benchmarks][analyzer] Draft of an analyzer of the database created b…

3b8bbc8

…y absolute-bench.

[Octagon][closure] Improve the closure with code hoisting.

68e120c

ptal closed this May 17, 2019

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Boxed octagon and test framework #12

Boxed octagon and test framework #12

ptal commented Dec 7, 2018

Boxed octagon and test framework #12

Boxed octagon and test framework #12

Conversation

ptal commented Dec 7, 2018