INTRODUCTION This directory contains the source code for Banal. Banal is a static analyzer by abstract interpretation that computes sufficient conditions using backward under-approximations in numeric abstract domains. Banal is a proof-of-concept, a research prototype, and a work in progress. It is very simple and featureless, and has probably some bugs. It handles only small programs in a toy programming language. It is intended for research purposes only. It should not be used in production. Banal was developed to implement and test the analysis method described in the article: A. Miné. Inferring sufficient conditions with backward polyhedral under-approximations. In Proc. of the 4th International Workshop on Numerical and Symbolic Abstract Domains (NSAD 2012). Electronic Notes in Theoretical Computer Science, Elsevier. Sept. 2012, Deauville, France. LICENSE Banal is distributed under the CRAPL license (except where another license is explicitly mentioned). See the CRAPL-LICENSE.txt file. Banal is copyright (C) Antoine Miné 2011-2012 (except where another author is explicitly mentioned). The file utils/mapext.ml is a modification of the map.ml file from the standard OCaml distribution. It retains its LGPL-derived original licence. REQUIREMENTS Banal is written in OCaml. It requires the following non-standard applications and libraries: - OCaml 3.12.1 (untested on later versions) - Menhir: LR(1) parser generator - ZArith: OCaml library for arbitrary precision numbers - Apron: numerical abstract domain library - GMP and MPFR (required by Apron and ZArith) COMPILATION Compilation has only been tested on Linux. It may work on other Unix-like operating systems as it uses mostly portable code and libraries (with the possible exception of utils/ml_float.c). If some tools are not installed in a PATH-visible directory, you may need to modify the "tools" part of the Makefile. If some libraries are not installed in the default OCaml library directory (ocamlc -where), you may need to modify the "external libs" part of the Makefile. To compile Banal, simple typing "make" should work. It will build: banal command-line analyzer wanalyzer.cgi WEB-based analyzer (CGI script or server) wtest.cgi a sample CGI program (to test your CGI installation) "make install" will attempt to install the WEB-based analyzer in public_html/ USAGE To launch the command-line analyzer, simply call "./banal" followed with the file (or list of files) to analyze. Example: ./banal tests/bubblesort.c The analyzer first performs a forward over-approximating analysis to compute invariants, and then a backward under-approximating analysis to find sufficient conditions at the entry point for the assertions to always hold. The result is dumped in text-format on the standard output. Additional information files in SVG and LaTeX format are output in the out/ directory (it is a good idea to clean it before each analysis). Extra information (useful for debugging) can be output by hacking some ref to true at the head of driver/iterator.ml and domains/apron_domain.ml. The following command-line options are recognized (showing their default value): -pp preprocessor pass the program through a proprecessor (e.g., cpp) -main main set the analyzer entry point (defaults to main) -domain poly|oct set the abstract domain (defaults to poly) -unroll 2 set the number of unrolled iterations in forward pass -join 2 set the widening delay in forward pass -down 2 set the number of decreasing iterations in forward pass -meet 4 set the widening delay in backward pass We do not detail the usage of the WEB-based analyzer wanalyzer.cgi as it is quite dependent on your installation. Some paths and URI are hardcoded: see WEBCGIINSTALL and WEBSTATICINSTALL in Makefile, static_root in web/webmain.ml, and the action="..." field in static/index.html . By default, wanalyzer.cgi behaves as a CGI script, invoked by a WEB server. However, the -server option orders it to behave as a stand-alone HTTP server on port 8080. A WEB-based analyzer instance runs at: http://www.di.ens.fr/~mine/banal/ . DOCUMENTATION Being a research prototype, the documentation on Banal is scarce. The main source of documentation is the HTML pages found in the static/ directory. In particular, static/syntax.html describes the syntax of the programming language analyzed by Banal. SOURCE TREE domains/ abstract domain implementations driver/ iterator and command-line analyzer frontend/ front-end for the toy language accepted by Banal utils/ data-structures and math utilities web/ WEB-based analyzer static/ resources for the WEB-based analyzer tests/ sample programs analyzables by Banal Most files in utils/ and web/ are reusable modules independent from Banal.