Commit f4553bd0 authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

APLAS response v0

parent 84d7592e
We thank the reviewers for their constructive comments. All the minor issues will be dealt in the final version of this paper. Answers to the reviewers' questions and comments are given below.
---------- Reviews A, B and C ----------
Q: The proposed solution can be applied to efficiently analyze real-world large-sized projects
and not handcrafted benchmarks?
We did apply our decision procedures to ‘real’ problems, namely, the MEM-SAT and MEM-ENT benchmark suites (occupying more than half of our benchmarks), which are generated from the path constraints and verification conditions of the building blocks of well-known open-source memory allocators.
Although this work focuses on heap lists, it shows that even heap lists are already nontrivial to deal with automatically. Therefore, our work is a solid foundation for the extension of ASL with more general inductive definitions containing pointer arithmetic.
Q: Why not extracting pointer-arithmetic programs from other benchmarks, e.g., SV-COMP?
SV-COMP includes some benchmarks using pointer arithmetics, but most of them
employ pointer arithmetics to access the content of arrays or to encode the
access to fields in branching data structures.
We did not found a benchmark using the heap list data structure, but we plan
to propose our code for the next editions of SV-COMP.
---------- Review A ----------
Q: What are the other heuristics employed to make the decision procedure practical?
The only heuristics we employ currently are those explained in the paper.
They help to compute the total order of addresses in the consequent by inferring
this order from the syntax of spatial atoms.
Q: Is the use of \infinity in predicate definition a thread for validity?
We first notice that the semantics of SLAH fixes to \top only the upper bound constraint, \Pi', and not the full pure constraint.
When a formula contains multiple unbounded blocks, they shall be ordered because of the separating conjunction composing these blocks. For the entailment, the antecedent and the consequent shall denote the same memory block, finite block even if not bounded.
---------- Review B ----------
Q: How does SLAH compare to the decidable logics in [1-3]?
The Kimura & Tatsuka work (reference [1] for the reviewer, [22] in our paper,
whose complete version is [23]) proposes a version of ASL with only the
memory block predicate and a list segment predicate that does not include
the memory block predicate. Therefore, this fragment does not deal with
heap list.
The reference [2] (POPL'17 paper of Vazou et al.) proposes a general approach
on defining logics and verifying programs based on a decidable SMT theory.
The refinement for our fragment of separation logics using this approach is
an interesting idea. It is not clear how to obtain the complexity of decision
problems for this fragment using this approach. Our work provide such results.
Another idea suggested by the reviewer is the verification of programs
manipulating heap lists using the approach of [2], without using
separation logic (SL) or ASL. It seems to us that the framework in [2] is
mainly dedicated to functional languages with simulated side-effects.
We did try to verify the C programs manipulating heap list using existing
verification tools for SL, but the annotation work was heavy (lemmas about
heap lists, for example) even if the fragment is decidable.
The reference [3] (VMCAI'19 paper of Qiu and Wang) proposes an extension of DRYAD
with recursive definitions over dynamic data structures, like lists and trees.
The support for memory blocs is not directly provided.
Concerning the recursive definitions, heap lists are linear recursive definitions,
as allowed by DRYAD, but heap list requires the memory block predicate.
The presence of the memory block predicate is important because these
memory blocks shall not overlap and the decision procedure deals with
this semantics of ASL.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment