In this artifact we provide (Java) implementations for the symbolic execution approach LISSA and the SymSolve solver for partially symbolic structures. The symbolic execution approach of LISSA is tailored to efficiently deal with programs manipulating heap-allocated inputs that impose complex structural constraints (preconditions) on the inputs, operationally captured via repOK (Java) methods. LISSA is implemented on top of the lazy initialization engine of Symbolic Java PathFinder.

LISSA is based on a novel solver, SymSolve, that automatically and efficiently decides whether partially symbolic structures produced by lazy initialization can be extended to fully concrete structures satisfying the precondition (repOK). LISSA employs SymSolve to identify spurious symbolic structures (those that cannot be extended to concrete structures) and prune their corresponding paths in the symbolic execution tree, significantly reducing the number of paths LISSA needs to explore, and making it faster than related approaches.

We also provide a replication package for the experiments in the ASE’22 paper introducing LISSA: “LISSA: Lazy Initialization with Specialized Solver Aid”. In the experiments, we assessed LISSA against related techniques over various case studies consisting of programs manipulating heap-allocated inputs with complex constraints, and observed that LISSA is faster and scales better than related techniques.

Juan Manuel Copia

IMDEA Software Institute; Universidad Politécnica de Madrid

Spain

Pablo Ponzio

Dept. of Computer Science FCEFQyN, University of Rio Cuarto

Nazareno Aguirre

University of Rio Cuarto and CONICET, Argentina

Alessandra Gorla

IMDEA Software Institute

Spain

Marcelo F. Frias

Dept. of Software Engineering Instituto Tecnológico de Buenos Aires

Automated program repair (APR) techniques have shown great success in automatically finding fixes for programs in programming languages such as C or Java. In this work, we focus on repairing formal specifications, in particular for the Alloy specification language. As opposed to most APR tools, our approach to repair Alloy specifications, named ICEBAR, does not use test-based oracles for patch assessment. Instead, ICEBAR relies on the use of property-based oracles, commonly found in Alloy specifications as predicates and assertions. These property-based oracles define stronger conditions for patch assessment, thus reducing the notorious overfitting issue caused by using test-based oracles, typically observed in APR contexts. Moreover, as assertions and predicates are inherent to Alloy, whereas test cases are not, our tool is potentially more appealing to Alloy users than test-based Alloy repair tools.

At a high level, ICEBAR is an iterative, counterexample-based process, that generates and validates repair candidates. ICEBAR receives a faulty Alloy specification with a failing property-based oracle, and uses Alloy’s counterexamples to build tests and feed ARepair, a test-based Alloy repair tool, in order to produce a repair candidate. The candidate is then checked against the property oracle for overfitting: if the candidate passes, a repair has been found; if not, further counterexamples are generated to construct tests and enhance the test suite, and the process is iterated. ICEBAR includes different mechanisms, with different degrees of reliability, to generate counterexamples from failing predicates and assertions.

Our evaluation shows that ICEBAR significantly improves over ARepair, in both reducing overfitting and improving the repair rate. Moreover, ICEBAR shows that iterative refinement allows us to significantly improve a state-of-the-art tool for automated repair of Alloy specifications without any modifications to the tool.

Simón Gutiérrez Brida

University of Rio Cuarto and CONICET, Argentina

Argentina

Germán Regis

Universidad Nacional de Río Cuarto

Argentina

Guolong Zheng

University of Nebraska Lincoln

Hamid Bagheri

University of Nebraska-Lincoln

ThanhVu Nguyen

George Mason University

United States

Nazareno Aguirre

University of Rio Cuarto and CONICET, Argentina

Marcelo F. Frias

Dept. of Software Engineering Instituto Tecnológico de Buenos Aires

Programs that deal with heap-allocated inputs are difficult to analyze with symbolic execution (SE). Lazy Initialization (LI) is an approach to SE that deals with heap-allocated inputs by starting SE over a fully symbolic heap, and initializing the inputs’ fields on demand, as the program under analysis accesses them. However, when the program’s assumed precondition has structural constraints over the inputs, operationally captured via repOK routines, LI may produce spurious symbolic structures, making SE traverse infeasible paths and undermining SE’s performance. repOK can only decide the feasibility of fully concrete structures, and thus previous work relied on manually crafted specifications designed to decide the (in)validity of partially symbolic inputs, to avoid producing spurious symbolic structures. However, these additional specifications require significant further effort from developers.

To deal with this issue, we introduce SymSolve, a test generation based approach that, given a partially symbolic structure and a repOK, automatically decides if the structure can be extended to a fully concrete one satisfying repOK. As opposed to previous approaches, SymSolve does not require additional specifications. It works by exploring feasible concretizations of partially symbolic structures in a bounded-exhaustive manner, until it finds a fully concrete structure satisfying repOK, or it exhausts the search space, deeming the corresponding partially symbolic structure spurious. SymSolve exploits sound pruning of the search space, combined with symmetry breaking (to discard structures isomorphic to previously explored ones), to efficiently explore very large search spaces.

We incorporate SymSolve into LI in order to decide the feasibility of partially symbolic inputs, obtaining our LISSA technique. We experimentally assess LISSA against related techniques over various case studies, consisting of programs with heap-allocated inputs with complex constraints. The results show that LISSA is faster and scales better than related techniques.

Juan Manuel Copia

IMDEA Software Institute; Universidad Politécnica de Madrid

Spain

Pablo Ponzio

Dept. of Computer Science FCEFQyN, University of Rio Cuarto

Nazareno Aguirre

University of Rio Cuarto and CONICET, Argentina

Alessandra Gorla

IMDEA Software Institute

Spain

Marcelo F. Frias

Dept. of Software Engineering Instituto Tecnológico de Buenos Aires

Automated program repair (APR) techniques have shown great success in automatically finding fixes for programs in programming languages such as C or Java. In this work, we focus on repairing formal specifications, in particular for the Alloy specification language. As opposed to most APR tools, our approach to repair Alloy specifications, named ICEBAR, does not use test-based oracles for patch assessment. Instead, ICEBAR relies on the use of property-based oracles, commonly found in Alloy specifications as predicates and assertions. These property-based oracles define stronger conditions for patch assessment, thus reducing the notorious overfitting issue caused by using test-based oracles, typically observed in APR contexts. Moreover, as assertions and predicates are inherent to Alloy, whereas test cases are not, our tool is potentially more appealing to Alloy users than test-based Alloy repair tools.

At a high level, ICEBAR is an iterative, counterexample-based process, that generates and validates repair candidates. ICEBAR receives a faulty Alloy specification with a failing property-based oracle, and uses Alloy’s counterexamples to build tests and feed ARepair, a test-based Alloy repair tool, in order to produce a repair candidate. The candidate is then checked against the property oracle for overfitting: if the candidate passes, a repair has been found; if not, further counterexamples are generated to construct tests and enhance the test suite, and the process is iterated. ICEBAR includes different mechanisms, with different degrees of reliability, to generate counterexamples from failing predicates and assertions.

Our evaluation shows that ICEBAR significantly improves over ARepair, in both reducing overfitting and improving the repair rate. Moreover, ICEBAR shows that iterative refinement allows us to significantly improve a state-of-the-art tool for automated repair of Alloy specifications without any modifications to the tool.

Simón Gutiérrez Brida

University of Rio Cuarto and CONICET, Argentina

Argentina

Germán Regis

Universidad Nacional de Río Cuarto

Argentina

Guolong Zheng

University of Nebraska Lincoln

Hamid Bagheri

University of Nebraska-Lincoln

ThanhVu Nguyen

George Mason University

United States

Nazareno Aguirre

University of Rio Cuarto and CONICET, Argentina

Marcelo F. Frias

Dept. of Software Engineering Instituto Tecnológico de Buenos Aires