Submission 70

[Edkamb]

This issue will be used for the communication concerning the testing phase of submission 70.

[aff2bfe]

The installation (I followed the online, automatic one) went smoothly. I did not find the PDF of the related publication. When running the examples of the two programs, some outputs seem different from the expected ones, in the README. I'd like the author to confirm this is the expected behaviour and I did not make some mistakes in launching the commands.

FamilySketcher

./Main.native -tree -domain polyhedra bench/loop1a-5.c

Gives

Solution: A-B >= 3 && B >= 0 && -A >= -31
Ranking function is: 
[A-B >= 3 && B >= 0 && -A >= -31 ?? A-B >= 3 && B >= 0 && -A >= -31 ? 3A-3B+4
] 
Minimal objective is: 13 
Hole {B} is: 0 
Hole {A} is: 3 
Time: 0.032110 s

instead of (** delimit relevant syntactic differences)

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

Also ./Main.native -tree -domain polyhedra bench/loop1b-5.c gives a similar result

with

Solution: A-B >= 1 && B >= 0 && -A+B >= -7 && -A >= -31
Ranking function is: 
[A-B >= 1 && B >= 0 && -A+B >= -7 && -A >= -31 ?? A >= 1 && -A >= -31 && -A+B == -1 ? 7
A-B >= 2 && B >= 0 && -A+B >= -7 && -A >= -31 ? 3A-3B+4
] 
Minimal objective is: 7 
Hole {B} is: 0 
Hole {A} is: 1 

Solution: A >= 0 && -B >= -31 && -A+B >= 0
Ranking function is: 
[A >= 0 && -B >= -31 && -A+B >= 0 ?? A >= 0 && -B >= -31 && -A+B >= 0 ? 4
] 
Minimal objective is: 4 
Hole {B} is: 0 
Hole {A} is: 0 
Time: 0.067643 s

instead of (** delimit syntactic differences)

Detailed output: 
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

Sketch

The first example

./sketch --bnd-cbits 5 --bnd-inbits 5 --bnd-unroll-amnt 8 tests/loop1a.sk

gives

SKETCH version 1.7.6
Benchmark = tests/loop1a.sk
/* BEGIN PACKAGE ANONYMOUS*/
/*tests/loop1a.sk:4*/

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)
}
/*tests/loop1a.sk:4*/

void sketch__Wrapper ()  implements sketch__WrapperNospec/*tests/loop1a.sk:4*/
{
  sketch();
}
/*tests/loop1a.sk:4*/

void sketch__WrapperNospec ()/*tests/loop1a.sk:4*/
{ }
/* END PACKAGE ANONYMOUS*/
[SKETCH] DONE
Total time = 1438

instead of

Detailed output: 
Solution (optimal) is: ??_1=4 and ??_2=1

The second example

./sketch --bnd-cbits 5 --bnd-inbits 5 --bnd-unroll-amnt 11 tests/loop1b.sk

gives

SKETCH version 1.7.6
Benchmark = tests/loop1b.sk
/* BEGIN PACKAGE ANONYMOUS*/
/*tests/loop1b.sk:4*/

void sketch ()/*tests/loop1b.sk:4*/
{ }
/*tests/loop1b.sk:4*/

void sketch__Wrapper ()  implements sketch__WrapperNospec/*tests/loop1b.sk:4*/
{
  sketch();
}
/*tests/loop1b.sk:4*/

void sketch__WrapperNospec ()/*tests/loop1b.sk:4*/
{ }
/* END PACKAGE ANONYMOUS*/
[SKETCH] DONE
Total time = 460

instead of

Detailed output: 
Solution (not optimal) is: ??_1=20 and ??_2=17 
Total Time: 0.203 sec

[dadacapo]

I also follow the the ONLINE version of README. ./install script, compilation of sketch-1.7.6 and all the examples run smoothly without any errors. But I observe the same output (except the time used) as @aff2bfe did, which do not match the given solutions in README. And it seems that we do not have the access to the full paper.

[aleksdimovski]

paper23.pdf loop1a-5.txt

Dear Reviewers,

Thank you for installing my tool, FamilySketcher2, as well as Sketch 1.7.6.

I attached the final version of my paper "Quantitative Program Sketching using Lifted Static Analysis". I have also re-submitted at easychair a merged pdf of the tool artifact and the paper. Initially, I thought you can access the submitted version of this paper, under Submission 23.

FamilySketcher2

Examples loop1a, loop1b, loop2a, and loop2b are explained in Section 2 (Motivating Examples) of the paper.

I will explain the output of the first example "bench/loop1a-5.c": $ ./Main.native -tree -domain polyhedra bench/loop1a-5.c

The complete output can be found in loop1a-5.txt (find it attached).

We first print the Abstract syntax of the input program loop1a-5.c Abstract Syntax: [ 1:] int main( ): [ 2:] $4{x} := $1{A} [ 3:] $5{y} := 0 [ 4:] while [ 5:] ( $4{x} > $2{B} ) do [ 6:] $4{x} := $4{x} - 1 [ 7:] $5{y} := $5{y} + 1 [ 8:] od [ 9:] assert( $5{y} > 2 ) [10:] $3{$3} := 0 [11:] return [12:]

With each variable, we assoiciate an unique number identifier. E.g., (4,x), (5,y), (3, output), etc.

A and B represent feature variables with domains [0,31], i.e. 5-bits size. They replace two holes ??_1 and ??_2. The aim of the tool is to replace these two holes (feature variables), such that the given assertion is "correct" and additionally the resulting complete program is "optimal" with respect to the number of execution steps to termination.

As explained in the paper, to solve this problem we perform two lifted static analysis. Forward numerical analysis computes lifted numerical invariants in all program locations. For example, the lifted invariant computed in location [9:] before assertion is (see also Fig. 1 on pp.4 in the paper):

[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 ?. Some of the constraints represent the domain of A, B \in [0,31], and constraints from decision nodes are also reproduced in leaves again. So if we remove them for brevity (we think of them as implict constraints), we obtain the decision tree in Fig. 1 on pp. 4. That is, [-A+B >= 0 ? y == 0 && -A+x == 0] [A-B >= 1 ? -B+x == 0 && -A+B+y == 0]

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 ? ; }

This means that the correct sub-family, i.e. Solution, is: (A-B >= 3 && B >= 0 && -A >= -31), as reported by the tool.

Next, we perform the backward termination analysis that computes lifted ranking functions in all program locations for this correct sub-family. The obtained lifted ranking function in intial location [1:] is (see also Fig. 2 on pp.4 in the paper):

[A-B >= 3 && B >= 0 && -A >= -31 ?? A-B >= 3 && B >= 0 && -A >= -31 ? 3A-3B+4]

As explained in the paper, 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 ?. We can see that the ranking function is: 3A-3B+4 for the whole correct sub-family.

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

This means the minimum of ranking function is 13, when B=0 and A=3. If we replace A with 3 and B with 0 in the original program family, we obtain a complete program that satisfies the assertion and is optimal wrt to number of execution steps to termination.

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

Sketch 1.7.6

Given the Sketch "tests/loop1a.sk", i.e. a partial program with two holes ??_1 and ??_2:

harness void sketch() { int x=??; int y=0; while (x > ??) {
x = x - 1; y = y + 1; } assert (y>2); }

The Sketch tool reports one possible ``correct'' solution, where ??_1=4 and ??_2 =1:

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) }

The Sketch tool reports only "correct" solutions, but not necessarly "optimal". As explained in the paper, in some cases Sketch reports an empty trivial solutions, or fails to solve some examples. In case of empty trivial solutions, you can try to perform several executions of the given example in order to obtain a non-trivial solution. This is the case with "tests/loop1b.sk" example. The Reviewer has obtained one trivial empty solution after one execution, and I have obtained a non-trivial solution: ??_1=20 and ??_2=17, after maybe several executions of this example.

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

[aff2bfe]

Dear @aleksdimovski,

Thanks for the detailed answer.

Regarding FamilySketcher, my question was far shallower: I saw some syntactic differences between the expected output and the actual one and I'd have liked you to confirm this is the expected behaviour. If that is the case — it seems so, given your text above —, I'd suggest updating the README to avoid this small (although noticed by both reviewers) discrepancy.

Regarding the second point, on Sketch 1.7.6, I'd suggest making it super-clear in the README that the user can see two possible kinds of outputs — a brief explanation of why that happens can also help to understand the tool better —, detailing what is their expected form and that they may need multiple runs to observe both of them.

[aleksdimovski]

Dear Reviewers,

I have now updated both README-ONLINE-SH.txt and README-OFFLINE-SH.txt at the tool’s web site: https://zenodo.org/record/5898643#.Ye7fA_7MLIV (new version). I make now difference between “Detailed output” of a tool where I refer to .txt files obtained by running the tools on a given example, and “Output summary” where I explain the final obtained results in short. I also describe the most important parts of “Detailed output”.

I also explain why Sketch 1.7.6 may produce different solutions in different executions. 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 this empirical hypothesis, several executions of the same example may produce different results (see # Note on results reported by Sketch 1.7.6 in README-ONLINE-SH.txt).