This paper proposes two decision procedures for a fragment of separation logic called SLAH---a fragment which comprises arrays and linked lists and which is shown to be suitable for the specification and verification of heap manipulating programs with pointer arithmetic. SLAH is thus an extension of array separation logic (ASL) with support for a special inductive predicate `hls` to describe linked lists. The semantics of SLAH is rather standard, except for the `hls` atom which imposes a size constraint on all memory chunks within the list.

The satisfiability problem in SLAH is shown to be NP-complete by reducing it to the satisfiability of existentially quantified Presburger arithmetic formulae. This is achieved by performing an abstraction of a SLAH formula according to a case analysis on the structure of the formula. The trickiest point is of course that of abstracting the `hls` atoms which works by summarising the relation between the predicate’s parameters for all possible unfoldings. The result is an existentially quantified Presburger arithmetic formula shown to be further reducible to a quantifier free Presburger arithmetic formula.

The entailment problem of SLAH is shown to be coNP-complete. The trick in this case is to decompose an entailment into a finite number of ordered entailment problems while proving the coNP upper bound. The paper defines a preorder relation to relate the start and end addresses of the spatial atoms in the entailment and shows how to use this order to perform the aforementioned decomposition. The proof continues with a case analysis on the number of spatial atoms in the consequent, assuming all spatial atoms are sorted.

Comments for author

-------------------

This work is certainly within the scope of APLAS and tackling pointer manipulation is an important problem in program verification in general, and Separation Logic in particular. The work has theoretical value, but I am not sure how to grasp the experimental setup: it seems like the good performance can be attributed to the heuristics which have only been briefly mentioned. Furthermore, the benchmarks are all handcrafted.

Please see further remarks under `Questions`

Minor typos:

=========

Pg 2: "None of the aforementioned work" => "None of the aforementioned works"

Pg 2: "NP-complete and and coNP-complete respectively" => "NP-complete and and coNP-complete, respectively"

Pg 4: "means that the line 14" => "means that line 14"

Pg 5: "lines 9-15and 14 9"

Pg 5: "to prove the matching found" => "to prove the found match"

Pg 9: "in polynomial time an QFPA" => "in polynomial time a QFPA"

Questions for authors’ response

---------------------------------

1. Since solving the entailment is indeed expensive, except for matching the contiguous spatial atoms, I am curious what are the other heuristics employed to make the decision procedure practical? In conclusions you mention that this solver is able to efficiently solve the considered benchmark, however, I assume the efficiency comes in part thanks to these heuristics.

2. The authors implemented these decision procedures and experimented on a set of 190 problems, divided into four suites corresponding to SAT and ENT queries, respectively, which are further split into queries automatically generated as proof obligations during the verification process and manually generated ones. The results show an overall good performance. However, I do not know how to quantify the evaluation. I do understand that SL-COMP does not cover this theory, but is there a reason for not extracting pointer-arithmetic programs from the benchmarks of SV-COMP? As of now the problems look a bit cherry-picked, though I am aware that benchmarks for SAT and ENT check are not available for Separation Logic.

3. A major threat to the validity of the results is posed by the use of `\infinity`. The semantics of SLAH states that an infinite upper bound abstracts `\Pi` to be `\top`. In that case, are order guarantees preserved without coinductive reasoning? Moreover, what happens when a formula contains multiple unbounded blocks? Would it make sense to allow one such formula since two unbounded structures cannot be ordered?

This paper presents SLAH, a fragment of separation logic. The logic extends array separation logic (ASL) with a salient `hls` predicate, which represents a continuous sequence of memory chunks, each chunk starting with a header indicating the size of the chunk. The paper shows that the satisfiability and entailment problems are decidable and in NP-complete and co-NP-complete, respectively. In a nutshell, the decision procedures guess a preorder of the addresses involved in the formula and decompose the original problem to a sequence of subproblems (called special ordered entailment problem in the paper) and encode the arithmetic constraints to Presburger Arithmetic. The decision procedures are implemented, based on enumeration and with some optimizations, and evaluated on a set of 190 problems. Experiments show that the decision procedure solved all these problems efficiently.

Comments for author

-------------------

The technical aspects of the paper are presented clearly. I especially appreciate the example given in Section 2, which is interesting as the heap list data structure involves pointer arithmetic and seems to be beyond the expressiveness of existing decidable logics. The techniques used in the decision procedures (enumerating address orders, case analysis, etc.) are straightforward and common in literature. However, my major concern is the practicality of SLAH. The `hlt` predicate, the only thing new in the logic, seems to be very specialized for the heap list data structure. While the motivating example is interesting, the paper lacks a justification for the predicate's general usefulness. How often is the predicate used in a practical verification problem? The experiments contain 190 examples; but they seem to be artificial and it is not clear how realistic they are.

Another missing part is a comparison to existing decidable logics for heaps, both SL-based (e.g., SLar[1]) and non-SL-based (e.g., the decidable fragments for LiquidHaskell [2] and Dryad [3]). I would like to see both theoretical comparison on expressiveness and practical comparison on real-world problem solving. What properties are only expressible in SLAH and not in other decidable logics? And vice versa? I actually do not understand why the authors do not run the solver against existing benchmarks solved by these decision procedures. I understand that the SLar solver is probably not available, but it looks like the benchmarks they reported are available at https://github.com/DaisukeKimura/slar . How many of them can actually be expressed in or converted to SLAH? And how efficient can SLAH solve these benchmarks?

I am somewhat disappointed by the experiments. Besides the benchmark selection issues mentioned above, a lot of details are missed in the paper. It is even not clear what the solving results are -- how many problems have yes-answers and how many have no-answers? Any performance discrepancy for these two categories? I also suggest the authors to replace Table 1 by a "Time vs. #solved benchmarks" figure.

[1] Kimura, D. and Tatsuta, M., 2017, November. Decision procedure for entailment of symbolic heaps with arrays. In Asian Symposium on Programming Languages and Systems (pp. 169-189). Springer, Cham.

[2] Vazou, N., Tondwalkar, A., Choudhury, V., Scott, R.G., Newton, R.R., Wadler, Jhala, R.: Refinement refiection: Complete verification with smt. Proc. ACM Program. Lang. 2(POPL) (Dec 2017)

[3] Qiu, X. and Wang, Y., 2019, January. A decidable logic for tree data-structures with measurements. In International Conference on Verification, Model Checking, and Abstract Interpretation (pp. 318-341). Springer, Cham.

Questions for authors’ response

---------------------------------

How does SLAH compare to the decidable logics in [1-3]?

The authors propose decision procedures for a fragment of separation logic called

SLAH. It allows some form of pointer arithmetic inside inductive definitions. Two concrete problems, i.e., satisfiability and entailment, are considered, and the decision procedure has been implemented for the two problems by computing summaries of the inductive definition for heap lists. The tool built on an open-source project and evaluation shows very good results.

Comments for author

-------------------

Strengths

+ A decision procedure and automated solver for decision problems in a separation logic fragment allowing both pointer arithmetic and memory block inside inductive definitions.

+ The experimental evaluation on top of the benchmarks is very good. For the satisfiability problem, all instances pass the tests. For the entailment problem, only 2 out of 102 instances have a timeout. Overall, the structure of the paper is well organized and the results are clear with evidence.

Weaknesses

- It is unclear whether the proposed solution can be applied to efficiently analyze real-world large-sized projects.