Release version 0.1.0

.gitignore

@@ -0,0 +1,12 @@
+/target/
+/preca/
+.settings/
+*.class
+bin
+.classpath
+.project
+**/*.pyc
+**/__pycache__
+binsecplugin/concrete/binsec
+binsecplugin/concrete/_build
+_opam

README.md

@@ -1,19 +1,219 @@
-# PreCA
+# PreCA : Precondition Constraint Acquisition
 
-Constraint acquisition based precondition learner
+PreCA performs precondition inference relying on constraint acquisition. PreCA does not need the source code of the function under analysis but only the binary.
+PRECA is part of the BINSEC toolbox for binary-level program analysis and is build on top of the [constraint acquisition plateform](https://github.com/lirmm/ConstraintAcquisition).
 
-## Description
+# Table of Contents
 
-Paper: *Automated Program Analysis: Revisiting Precondition Inference through Constraint Acquisition*
+1.  [Requirements](#requirements)
+2.  [Installation](#installation)
+3.  [Usage](#usage)
+4.  [Experiments](#experiments)
+    1. [IJCAI'22](ijcai23)
+    2. [KR'23](kr23)
+5.  [Run your own example](#run-your-own-example)
+6.  [VM artifact (OUTDATED)](#vm-artifact-outdated)
+7.  [Cite us](#cite-us)
+8.  [References](#references)
 
-Authors: [Grégoire Menguy](https://gregoiremenguy.github.io/), [Sébastien Bardin](http://sebastien.bardin.free.fr/), [Nadjib Lazaar](http://www.lirmm.fr/~lazaar/), [Arnaud Gotlieb](https://www.simula.no/people/arnaud)
+# Requirements
 
-Published at: [The 31st International Joint Conference on Artificial Intelligence (IJCAI 2022)](https://ijcai-22.org/)
+The PreCA framework depends on:
+- [The Java Runtime Environment](https://www.java.com/en/download/)
+- [Maven](https://maven.apache.org/) if you want to recompile PreCA
+- [Binsec](https://github.com/binsec/binsec) (>= 0.8.1) with Unisim\*
+- Python 3 (to run the experiments)
 
-Details about the paper: [https://binsec.github.io/nutshells/ijcai-22.html](https://binsec.github.io/nutshells/ijcai-22.html)
 
+\*We recommend to install Binsec through [opam](https://opam.ocaml.org/), by following these steps: 
+```shell
+cd path/to/preca
+opam switch create . <OCAML_VERSION> # OCAML_VERSION < 5.0.0
+opam pin ./binsecplugin/concrete/   # pin the libconcrete package and install its dependencies (Binsec, Unisim ...)
+```
 
-## Artifacts
+To install the python dependencies, run:
+```
+python3 -m venv path/to/venv
+source path/to/venv/bin/activate
+pip install -r requirements.txt
+```
 
-A virtual machine (~2.6G) is available [here](https://zenodo.org/record/6513522#.YnD1GnVfjmE). It contains the PreCA jar file, the dataset and scripts to exercise PreCA and replay major experiments. The user and root password is "password".
+# Installation
+
+To use PreCA the `PRECA_PATH` environment variable should be set:
+```shell
+# You can put the following line in your .bashrc file (or equivalent file)
+export PRECA_PATH=/path/to/preca/directory   
+```
+
+## Run from JAR
+
+The `preca.jar` file is available to use PreCA without compiling it. See the [usage](#usage) section to found out how to use it.
+
+## Compile from source
+
+You can compile the code using maven (the generated jar file is then in the `target` directory):
+```shell
+mvn clean compile assembly:single
+cp target/<jarfile> preca.jar
+```
+
+# Usage
+
+You can get PreCA's available options:
+```shell
+java -jar preca.jar -help
+```
+
+PreCA takes as input the path to the configuration file as follows:
+```shell
+java -jar preca.jar -file <config>
+```
+
+Such a configuration file enables to specify which binary and which function is analyzed. You can get the documentation for the configuration file format with:
+```shell
+java -jar preca.jar -helpconf
+```
+
+## Example
+
+To check that your install works correctly, you can run PreCA over the given strcat example:
+```shell
+java -ea -jar preca.jar -file ./examples/strcat_conacq.txt
+```
+
+The output should end with:
+```
+*************Learned Network CL example ******
+network var=4 cst=3
+-------------------------
+CONSTRAINTS:
+Valid(var0)
+Valid(var1)
+NotOverlap(var0, var1)_or_StrlenEq0(var1)[0, 1, 2, 3]
+-------------------------
+
+*************Learned Network CL example (SMTLIB) ******
+(and (valid v0) (valid v1) (or (not (overlap v0 v1)) (strleneq v1 #x00000000)))
+```
+
+# Experiments
+
+We provide the needed datasets in the `datasets` directory and the script `scripts/bench.py` to replicate the results from our IJCAI'22 and KR'23 papers. 
+The help is available through
+```shell
+python3 ./scripts/bench.py -h
+```
+
+Moreover, after running your experiments, you can always recompute the statistics as follows:
+```shell
+python3 ./scripts/recompute_stats.py --file <json-file> --timeout <seconds>
+```
+
+Finally, since our IJCAI'22 paper, we added new constraint to our constraint language. Still, as both our IJCAI'22 and KR'23 papers consider the original set of constraint, it is possible retrict to it through the `--ijcai22` option.
+
+## IJCAI'22
+
+To replicate experiments from our IJCAI'22 paper [1] run the following commands:
+```
+python3 ./scripts/bench.py --dataset ./datasets/ijcai22/nopost --timeout 3600 --emulto 5 --out <out json> --disj auto --biaslvl max --ijcai22
+python3 ./scripts/bench.py --dataset ./datasets/ijcai22/post --timeout 3600 --emulto 5 --out <out json> --disj auto --biaslvl max --ijcai22
+```
+
+## KR'23
+
+To replicate results from our KR'23 paper [2], run the following commands:
+```
+python3 ./scripts/bench.py --dataset ./datasets/kr2023 --timeout 3600 --emulto 5 --out <out json> --disj <disj> --biaslvl <lvl> --ijcai22
+```
+
+The `<disj>` option states which methods is used to handle disjunction (see the following table).  
+The `<lvl>` states the size of the bias considered and takes value among `min`, `avg` and `max`.
+
+<table border="2" cellspacing="0" cellpadding="6" rules="groups" frame="hsides">
+
+
+<colgroup>
+<col  class="org-left" />
+
+<col  class="org-left" />
+</colgroup>
+<thead>
+<tr>
+<th scope="col" class="org-left">Abbreviation</th>
+<th scope="col" class="org-left">Description</th>
+</tr>
+</thead>
+
+<tbody>
+<tr>
+<td class="org-left">auto</td>
+<td class="org-left">We rely on the heuristics from [1] to generate the considered disjunctions</td>
+</tr>
+
+
+<tr>
+<td class="org-left">mss</td>
+<td class="org-left">we use DCA [2] to handle disjunctions</td>
+</tr>
+
+
+<tr>
+<td class="org-left"> n : int </td>
+<td class="org-left">add disjunctions of size up to n</td>
+</tr>
+
+
+<tr>
+<td class="org-left"> { i1, ..., in } </td>
+<td class="org-left">add disjunctions of size i1, ..., in</td>
+</tr>
+
+</tbody>
+</table>
+
+# Run your own example
+
+To run your own example, you must create a config file and a Binsec script associated to the function you want to analyze. 
+You can take example to the given `examples/strcat_conacq.txt` and `examples/strcat_dca.txt` configuration files, 
+as well as their corresponding Binsec script (`datasets/binsec_ini/ijcai22/nopost/strcat.ini`).
+
+For more examples, check the `datasets` directory.
+
+# VM artifact (OUTDATED)
+
+The PreCA artifact for the paper [1] was first published as a a virtual machine (~2.6G), which is available [here](https://zenodo.org/records/6513522#.YnD1GnVfjmE). 
+It contains the PreCA jar file, the datasets, and scripts to exercise PreCA and replay major experiments. The user and root password is "password".
+
+# Cite us
+
+```
+@inproceedings{DBLP:conf/ijcai/MenguyBLG22,
+  author       = {Gr{\'{e}}goire Menguy and
+                  S{\'{e}}bastien Bardin and
+                  Nadjib Lazaar and
+                  Arnaud Gotlieb},
+  editor       = {Luc De Raedt},
+  title        = {Automated Program Analysis: Revisiting Precondition Inference through
+                  Constraint Acquisition},
+  booktitle    = {Proceedings of the Thirty-First International Joint Conference on
+                  Artificial Intelligence, {IJCAI} 2022, Vienna, Austria, 23-29 July
+                  2022},
+  pages        = {1873--1879},
+  publisher    = {ijcai.org},
+  year         = {2022},
+  url          = {https://doi.org/10.24963/ijcai.2022/260},
+  doi          = {10.24963/ijcai.2022/260},
+  timestamp    = {Wed, 27 Jul 2022 16:43:00 +0200},
+  biburl       = {https://dblp.org/rec/conf/ijcai/MenguyBLG22.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+```
+
+# References
+
+1. [Menguy, Grégoire, et al. "Automated program analysis: Revisiting precondition inference through constraint acquisition." Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-ECAI 2022), Vienna, Austria. 2022.](https://www.ijcai.org/proceedings/2022/260)
+
+2. [Menguy, Grégoire, et al. "Active disjunctive constraint acquisition." Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning. Vol. 19. No. 1. 2023.](https://proceedings.kr.org/2023/50/)
 

binsecplugin/concrete/concrete_options.ml

@@ -0,0 +1,33 @@
+(****************************************************************************)
+(*  This file is part of PRECA.                                             *)
+(*  PRECA is part of the BINSEC toolbox for binary-level program analysis.  *)
+(*                                                                          *)
+(*  Copyright (C) 2019-2023                                                 *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies                *)
+(*         alternatives)                                                    *)
+(*                                                                          *)
+(*  you can redistribute it and/or modify it under the terms of the GNU     *)
+(*  Lesser General Public License as published by the Free Software         *)
+(*  Foundation, version 2.1.                                                *)
+(*                                                                          *)
+(*  It is distributed in the hope that it will be useful,                   *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of          *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the           *)
+(*  GNU Lesser General Public License for more details.                     *)
+(*                                                                          *)
+(*  See the GNU Lesser General Public License version 2.1                   *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).              *)
+(*                                                                          *)
+(****************************************************************************)
+
+include Cli.Make (struct
+  let name = "Emulation"
+
+  let shortname = "emul"
+end)
+
+module PermFile = Builder.String_option (struct
+  let name = "perm"
+
+  let doc = "path to the permision file"
+end)

binsecplugin/concrete/concrete_options.mli

@@ -0,0 +1,25 @@
+(****************************************************************************)
+(*  This file is part of PRECA.                                             *)
+(*  PRECA is part of the BINSEC toolbox for binary-level program analysis.  *)
+(*                                                                          *)
+(*  Copyright (C) 2019-2023                                                 *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies                *)
+(*         alternatives)                                                    *)
+(*                                                                          *)
+(*  you can redistribute it and/or modify it under the terms of the GNU     *)
+(*  Lesser General Public License as published by the Free Software         *)
+(*  Foundation, version 2.1.                                                *)
+(*                                                                          *)
+(*  It is distributed in the hope that it will be useful,                   *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of          *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the           *)
+(*  GNU Lesser General Public License for more details.                     *)
+(*                                                                          *)
+(*  See the GNU Lesser General Public License version 2.1                   *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).              *)
+(*                                                                          *)
+(****************************************************************************)
+
+include Cli.S
+
+module PermFile : Cli.STRING

binsecplugin/concrete/dune

@@ -0,0 +1,19 @@
+(library
+ (public_name libconcrete)
+ (name libconcrete)
+ (libraries binsec.sse)
+ (flags
+   (:standard -open Binsec -open Libsse -open Plugins))
+)
+
+(plugin
+ (name concrete)
+ (libraries libconcrete)
+ (site
+  (binsec plugins)))
+
+(plugin
+ (name emul)
+ (libraries libconcrete)
+ (site
+  (binsec plugins)))

binsecplugin/concrete/dune-project

@@ -0,0 +1,20 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+(generate_opam_files true)
+(maintainers "BINSEC <binsec@saxifrage.saclay.cea.fr>")
+
+(authors
+  "Grégoire Menguy"
+)
+(license LGPL-2.1-or-later)
+(homepage "https://binsec.github.io")
+(bug_reports "mailto:binsec@saxifrage.saclay.cea.fr")
+
+
+(package
+ (name libconcrete)
+ (synopsis "Precondition inference with constraint acquisition")
+ (depends
+  (binsec (>= 0.8.1))
+  unisim_archisec))
+