
This documents shows how to install all required tools from the paper 
¨Quantitative Program Sketching using Lifted Static Analysis¨
if there is NO INTERNET CONNECTION 

####################################################################################
## FamilySketcher2 --- Quantitative Program Sketcher using Lifted Static Analysis ## 
####################################################################################

FamilySketcher2 is a research prototype quantitative program sketcher designed for 
resolving numerical sketches using lifted static analysis based on abstract interpretation.


## Author

	Aleksandar Dimovski
	
	
# OFFLINE Installation

	$ cd Sketching2
	
* Initialize OPAM state [YOU NEED ONLINE CONNECTION for ´opam init´]
	```
	$ opam init      % [INTERNET] during initilization allow with Yes opam to modify ~/.profile
	```	
	```
	$ eval $(opam env)      % update the current shell environment
	```  
* Run the script installOff [answer with ´Yes´ on all questions during installation]
	```
	$ ./installOff
	```
* Set the Library Path variable in ~/.bashrc 
	```
	$ gedit ~/.bashrc
	```
Then, set the Library Path by appending at the end of the ~/.bashrc file:
	```
	LD_LIBRARY_PATH=/home/fase2022/.opam/default/share/apron/lib
	export LD_LIBRARY_PATH
	```
Log out of the current session, then log in and check:
	```
	$ echo $LD_LIBRARY_PATH
	```



# Compiling FamilySketcher2

Enter folder 
```
$ cd family_sketcher2
```
Once all required libraries are installed, 'ocamlbuild' can be used to build FamilySketcher with the following two commands:

```
$ eval $(opam config env)                 % It will setup environment variables, that are necessary for the toolchain to work properly

$ ocamlbuild Main.native -use-ocamlfind -use-menhir -pkgs 'apron,gmp,zarith' -I utils -I domains -I frontend -I main -libs boxMPQ,octD,polkaMPQ,str,zarith
```

# Test 

The program sketcher performs a forward reachability analysis and a backward termination analysis of program families and resolves the holes (features) so that 
the found solutions are 'correct & optimal' with respect to the final assertions and the given quantitative objective that counts the number of execution steps to termination. 

The following general command-line options are recognized
(showing their default value):

	 -tree					set to perform decision tree-based lifted analysis
	 -single 				set to perform brute force enumeration approach using single analysis for each variant
	 -main main                         set the analyzer entry point (defaults to main)
	 -domain boxes|octagons|polyhedra   set the abstract domain (defaults to boxes)
	 -joinfwd 2   			     set the widening delay in forward analysis


First examples

```
$ ./Main.native -tree -domain polyhedra bench/loop1a-5.c         
```
Detailed output is given in loop1a-5.txt. 
We now present some excerpts of the output with explanations of their meaning: 

Forward numerical analysis computes lifted numerical invariants in all program locations. 
For example, the lifted invariant computed in location [9:] before assertion is: 
[A >= 0 && -B >= -31 && -A+B >= 0 ? A >= 0 && -B >= -31 && -A+B >= 0 && y == 0 && -A+x == 0] 
[A-B >= 1 && B >= 0 && -A >= -31 ? A-B >= 1 && B >= 0 && -A >= -31 && -B+x == 0 && -A+B+y == 0] 
It represents a decision tree with two leaves given in the form [...?...]. 
The part before ? explains the constraints found in decision nodes that needs to be satisfied in order to reach the given 
node which is given after ?. 

We examine for which values of A, B \in [0,31], the assertion in location [9:] will be correct. 
The obtained result is: 
Assertion Analysis:
{ CORRECT: A-B >= 3 && B >= 0 && -A >= -31 ? ; DON'T KNOW: others;ERROR: A >= 0 && -B >= -31 && -A+B >= 0 ? ;  }

The backward termination analysis computes lifted ranking functions in all program locations for the correct sub-family. 
The obtained lifted ranking function in intial location [1:] is:  
[A-B >= 3 && B >= 0 && -A >= -31 ?? A-B >= 3 && B >= 0 && -A >= -31 ? 3A-3B+4]
There are two-level decision nodes in decision trees represnting lifted ranking functions.
In this case, we obtain a decision tree with one leaf node, where the first-level decision node is before ??, 
the second level decision node is after ??, and the leaf is after ?. 

Finally, we call the Z3 SMT solver to find the minimum of the ranking function (3A-3B+4), when the constraint 
(A-B >= 3 && B >= 0 && -A >= -31) is satisfied.
We obtain the following solution:
Minimal objective is: 13 
Hole {B} is: 0 
Hole {A} is: 3

The output summary: 
Forward analysis returns that the assertion is CORRECT for: A-B>=3 && B>=0 && A<=31 (note that both holes are of 5-bits size, so dom(A)=dom(B)=[0,31])
Backward analysis returns the ranking function at location [1:] is: 3A-3B+4
Solution: A=3 and B=0
Total Time: 0.016 sec

Similarly, we can read the output of the other examples using FamilySketcher2.

```
$ ./Main.native -tree -domain polyhedra bench/loop1b-5.c         
```
The output summary:
Forward analysis returns that the assertion is CORRECT for: solution (1) 1<=A-B<=7 && B>=0 && A<=31; and solution (2) A<=B && A>=0 && B<=31 (note that both holes are of 5-bits size, so dom(A)=dom(B)=[0,31])
Backward analysis returns the ranking function at location [1:] is: 3A-3B+4 for solution (1); and 4 for solution (2)
Solution (1): A=1 and B=0
Solution (2): A=0 and B=0
Total Time: 0.026 sec



################################################################################
##Brute Force approach --- Single-Program Analysis of all variants one by one ##
################################################################################

We stay in the same folder ¨family_sketcher2¨ as for FamilySketcher2, we run the same example files, but now  
we use command-line option ¨-single¨ instead of ¨-tree¨. 

# Test

First examples
```
$ ./Main.native -single -domain polyhedra bench/loop1a-5.c 
```
or you can redirect the output to a .txt file by: 
```
$ ./Main.native -single -domain polyhedra bench/loop1a-5.c >> loop1a-5.txt
```
Detailed output is given in loop1a-5single.txt. 
It analyzes all variants one-by-one and checks the correctness of assertions and computes the ranking function 
in case of correct variants. 

The output summary: 
SUMMARY RESULTS report all correct variants and the corresponding ranking functions
Solutions with minimal ranking function 13 are: A=3 and B=0; A=4 and B=1; ...; A=31 and B=28
Total Time: 4.66 sec

$ ./Main.native -single -domain polyhedra bench/loop1b-5.c >> loop1b-5.txt
```
The output summary: 
SUMMARY RESULTS report all correct variants and the corresponding ranking functions
Solutions (1) with minimal ranking function 4 are: A=0 and B=0; A=0 and B=1; ...; A=31 and B=31
Solutions (2) with minimal ranking function 7 are: A=1 and B=0; A=2 and B=1; ...; A=31 and B=30
Total Time: 4.77 sec



###########################################################################################
## Sketch 1.7.6 --- Program Sketcher available from https://people.csail.mit.edu/asolar/ ##
###########################################################################################

The tool can be downloaded either from https://people.csail.mit.edu/asolar/ or can be found here
as sketch-1.7.6.tar.gz. 

	$ cd Sketching2

* unzip the file sketch-1.7.6.tar.gz
	```
	$ tar -xf sketch-1.7.6.tar.gz
	```  
* copy ¨tests¨ folder to ¨sketch-1.7.6/sketch-frontend¨ 
	```
	$ cp -r ./tests ./sketch-1.7.6/sketch-frontend
	```	

# the following tools need to be installed: 
* bison and flex

	```
	$ cd lib
	$ cd bison
	$ sudo dpkg -i * 
	$ cd ..

	$ sudo dpkg -i flex_2.6.4-6.2_amd64.deb
	$ cd ..
	```

# under the sketch-1.7.6 directory, execute:
	```
	$ cd sketch-1.7.6
	$ cd sketch-backend
	$ chmod +x ./configure
	$ ./configure
	$ make
	$ cd ..
	```
	
# Testing the sketch
	```
	$ cd sketch-frontend
	$ chmod +x ./sketch
	$ ./sketch test/sk/seq/miniTest1.sk 
	```
	
# from "sketch-frontend" directory you can test all sketches. 
Note that we use the following ¨./sketch¨ options

option --bnd-cbits determines the size in bits of control holes [default is 5]
option --bnd-inbits determines the size in bits of inputs [default is 5]
option --bnd-unroll-amnt determines the unroll amount for loops [default is 8]

# Examples from the paper are in ¨tests¨ folder (copy 'tests' subfolder into 'sketch-1.7.6/sketch-frontend'): 	

# Test

First examples

```  (current folder: ~/Sketching2/sketch-1.7.6/sketch-frontend)
$ ./sketch --bnd-cbits 5 --bnd-inbits 5 --bnd-unroll-amnt 8 tests/loop1a.sk
```
Detailed output is given in loop1a.txt. 
The obtained complete program is: 
void sketch ()/tests/loop1a.sk:4/
{
int y = 0;
int x = 4;
while(x > 1)
{
x = x - 1;
y = y + 1;
}
assert (y > 2); //Assert at tests/loop1a.sk:11 (2)
}
This means that the hole ??_1 is replaced with 4, and hole ??_2 with 1. 

The output summary:
Solution (optimal) is: ??_1=4 and ??_2=1 
Total Time: 0.192 sec   [* Note that Sketch reports the results in miliseconds]

Similarly, we can read the output of the other examples using Sketch 1.7.6.

```
$ ./sketch --bnd-cbits 5 --bnd-inbits 5 --bnd-unroll-amnt 11 tests/loop1b.sk
```
The output summary: 
Solution (not optimal) is: ??_1=20 and ??_2=17 
Total Time: 0.203 sec  

# Note on results reported by Sketch 1.7.6

Sketch 1.7.6 uses a CounterExample Guided Inductive Synthesis (CEGIS) technique and SAT solvers 
to produce candidate solutions from small set of inputs. Initially, the set of inputs contains 
only a random input. 
Because of the empirical hypothesis, several executions of the same example may produce different results. 
For more details on Sketch 1.7.6, we refer to PhD Thesis "Program Synthesis by Sketching" by Armando Solar-Lezama. 
