Upd to rc3

Author: Matthieu Lemerre

Dockerfile.alpine

@@ -19,23 +19,24 @@
 #                                                                        #
 ##########################################################################
 
-# Build with docker build -f release/Dockerfile -t codexmin .
-# Debug with docker run -ti num sh
-# Finish with docker cp codexmin:/home/ocaml/codex/_build/default/binsec/binsec_codex.exe .
+# Build with docker build -f Dockerfile.alpine -t codexalpine .
+# Debug with docker run -ti codexalpine sh
+# Finish with docker cp codexalpine:/home/ocaml/codex/_build/default/binsec/binsec_codex.exe .
 
 # Start with an alpine linux image with opam in it, for musl
 FROM ocamlpro/ocaml:4.14 as first
+RUN opam update
 RUN opam switch create optstatic --packages=ocaml-variants.4.14.1+options,ocaml-option-static,ocaml-option-flambda,ocaml-option-no-flat-float-array
 RUN opam switch optstatic
 RUN eval $(opam env)
-RUN opam install binsec bheap
+RUN opam install binsec bheap 
 # C++ is needed for cudd.
 RUN sudo apk add g++
 RUN opam install mlcuddidl 
 RUN opam install camlp-streams
 # bash needed for core, needed for ppx_inline_test.
 RUN sudo apk add bash
-RUN opam install qcheck-core ppx_inline_test unionFind
+RUN opam install qcheck-core ppx_inline_test unionFind pacomb patricia-tree
 
 
 # Install the patched Frama-C. This is cached if ext/frama_c_with_cudd does not change.

Dockerfile.debian

@@ -19,48 +19,48 @@
 #                                                                        #
 ##########################################################################
 
-# Build with docker build -t codexmin .
-# Run with docker run -ti codexmin bash
+# Build with: docker build -f Dockerfile.debian -t codexdebian .
+# Run with docker run -ti codexdebian bash
 # When a container runs:
-# Get frama_c_codex.exe with docker cp container:/home/opam/libase/_build/default/frama-c/frama_c_codex.exe .
-# Get binsec_codex.exe with docker cp container:/home/opam/libase/_build/default/binsec/binsec_codex.exe .
+# Get frama_c_codex.exe with docker cp container:/home/opam/codex/_build/default/frama-c/frama_c_codex.exe .
+# Get binsec_codex.exe with docker cp container:/home/opam/codex/_build/default/binsec/binsec_codex.exe .
 FROM ocaml/opam:debian-11-ocaml-4.14 as first
 ENV DEBIAN_FRONTEND=noninteractive
 # Installs binsec, then frama-c dependencies.
-RUN sudo apt-get update && sudo apt-get -y install --no-install-recommends libgmp-dev liblmdb-dev && \
+RUN sudo apt-get update && sudo apt-get -y install --no-install-recommends bc libgmp-dev liblmdb-dev && \
   sudo apt-get install -y --no-install-recommends pkg-config autoconf graphviz libexpat1-dev zlib1g-dev \
                          libcairo2-dev libexpat1-dev libgtk-3-dev libgtksourceview-3.0-dev \
                         libgnomecanvas2-dev cmake time z3 gcc-multilib && sudo apt-get clean
 # Install binsec and dependencies (libgmp, needed by zarith)
 RUN opam install binsec
 # Install Codex dependencies (including sexplib, optinonally used by frama-c dependencies)
-RUN opam install mlcuddidl lmdb sexplib ppx_sexp_conv
+RUN opam install mlcuddidl lmdb sexplib ppx_sexp_conv pacomb bheap qcheck-core ppx_inline_test
 # Install the Frama-C dependencies
 # RUN opam install --deps-only frama-c && opam install yojson=2.0.0
 # Install minimal frama-c dependencies.
-RUN opam install yojson=2.0.0 ppx_deriving_yojson ppx_import
+RUN opam install yojson=2.0.0 ppx_deriving_yojson ppx_import yaml ppx_deriving_yaml patricia-tree
 # Compile a patched version of Frama-C to support cudd.
 # The patched version also prevents the dynamic loading of JSON configuration, so that frama_c_codex.exe can be used as a standalone binary.
-RUN curl https://www.frama-c.com/download/frama-c-26.1-Iron.tar.gz -o frama-c-26.1-Iron.tar.gz
+RUN curl https://www.frama-c.com/download/frama-c-27.1-Cobalt.tar.gz -o frama-c-27.1-Cobalt.tar.gz
 COPY --chown=opam:opam nix/patch-frama-c.patch patch-frama-c.patch
 # Install frama-C, without the plugins to make the compilation faster.
 # We also remove the plugins so that the frama_c_codex.exe binary will not try loading them.
-RUN tar xzf frama-c-26.1-Iron.tar.gz \
+RUN tar xzf frama-c-27.1-Cobalt.tar.gz \
    && cd frama-c* \
    && patch -Np1 -i ../patch-frama-c.patch \
    && rm -R src/plugins \
    && eval $(opam env) && make && make install \
    && cd .. && rm -Rf frama-c*
 # Install more odvtk dependencies
-RUN sudo apt install libev-dev libssl-dev -y
+RUN sudo apt-get install libev-dev libssl-dev -y
 RUN opam install dream
 # Now install codex.
 RUN opam clean -a -c -s --logs && \
     rm -Rf opam-repository/.git && \
     rm -Rf opam-repository && \
     rm -Rf .opam/repo
-COPY --chown=opam:opam . /home/opam/libase
-RUN cd libase && eval $(opam env) && dune build binsec/binsec_codex.exe && cd frama-c && make build
+COPY --chown=opam:opam . /home/opam/codex
+RUN cd codex && eval $(opam env) && dune build
 # Optional: this further slims down the new image, which becomes kind of binary-only.
 # Works and allows a substantial gain in space, but currently the script for binsec call dune exec binsec_codex.exe, which tries to rebuild the binary and remove it. 
 # RUN cd  .opam && \
@@ -79,8 +79,6 @@ RUN cd libase && eval $(opam env) && dune build binsec/binsec_codex.exe && cd fr
 ## COPY --from=first /home/opam /home/opam
 ## 
 ## EXPOSE 8080
-# For an even slimmer version, we could just keep the binsec_codex.exe and frama_c_codex.exe executables.
-# This does not work for frama_c_codex.exe; maybe use appimage for that.
 
 
 # Local Variables:

Makefile

@@ -19,36 +19,83 @@
 #                                                                        #
 ##########################################################################
 
-test.opt:
+# See "make help" for a list of targets and brief documentation
+
+# set to ON/OFF to toggle ANSI escape sequences
+COLOR = ON
+
+# padding for help on targets
+# should be > than the longest target
+HELP_PADDING = 20
+
+ifeq ($(COLOR),ON)
+	color_yellow = \033[93;1m
+	color_orange = \033[33m
+	color_red    = \033[31m
+	color_green  = \033[32m
+	color_blue   = \033[34;1m
+	color_reset  = \033[0m
+endif
+
+test.opt:  ## Build and run frama-c/codex on root/test.c
 	cd frama-c && make test.opt
+.PHONY: test.opt
 
-dune:
+tests.opt:  ## Build and run frama-c/codex on all tests
+	cd frama-c && make tests.opt
+.PHONY: tests.opt
+
+test.diff:  ## Same as test.opt, but shows a diff with installed version of codex
+	cd frama-c && make test.diff
+.PHONY: test.diff
+
+dune: ## Build the project with dune
 	dune build
+.PHONY: dune
 
-binsec:
+binsec: ## Build binsec_codex.exe
 	dune build binsec/binsec_codex.exe
-
 .PHONY: binsec
 
+frama_c_codex: ## Build frama_c_codex.exe
+	dune build frama-c/frama_c_codex.exe
+	dune build -p codex,frama_c_codex
+.PHONY: frama_c_codex
+
+frama_c_codex_plugin: ## Build the codex frama-c plugin
+	dune build frama-c/frama_c_codex.exe
+	dune build -p codex,frama_c_codex,frama_c_codex_plugin
+.PHONY: frama_c_codex_plugin
+
+clean: ## Remove build files and executable
+	dune clean
+.PHONY: clean
+
+doc: ## Build the documentation (accessible at _build/default/_doc/_html)
+	dune build --display short @doc-private
+	@echo "$(color_yellow)Browse doc at _build/default/_doc/_html/index.html$(color_reset)"
+.PHONY: doc
+
 docker:
 	docker build -t codex .
 
-# Static version of BINSEC/Codex && FramaC/Codex.
-binsec_codex.exe frama_c_codex.exe: Dockerfile.alpine
+.PHONY: binsec_codex.exe frama_c_codex.exe
+binsec_codex.exe frama_c_codex.exe: Dockerfile.alpine ## Build static version of BINSEC/Codex && FramaC/Codex.
 	docker build -f Dockerfile.alpine -t codexstatic .
 	docker run --name my_container --detach codexstatic && docker cp my_container:/home/ocaml/codex/_build/default/binsec/binsec_codex.exe . && docker rm  my_container
 	docker run --name my_container --detach codexstatic && docker cp my_container:/home/ocaml/codex/_build/default/frama-c/frama_c_codex.exe . && docker rm  my_container
 
-
 install-opam:
 	opam init --compiler 4.14.1
 
 # We need a patched version of Frama-C. If you have opam,
 # just type make opam-install-frama-c-with-cudd.
-opam-install-frama-c-with-cudd:
+opam-install-frama-c-with-cudd: ## Install patched version of frama-c for codex
 	cd ext/frama_c_with_cudd && make
+.PHONY: opam-install-frama-c-with-cudd
 
-dependency_graph.png:
+.PHONY: dependency_graph.png
+dependency_graph.png: ## Generate the library dependency graph
 	dune-deps -x ext -x utils --no-ext | tred | dot -Tpng > $@
 
 ################ Rules to update headers and check that we did not forgot any file
@@ -62,14 +109,15 @@ FIND_EXCLUDE += -not -path './benchmarks/*'
 
 UPDATED_EXTENSIONS = mli ml c h
 
-update_headers:
+.PHONY: update_headers
+update_headers: ## Update file headers using headache
 	echo '$(patsubst %, -o -name "%", $(UPDATED_EXTENSIONS))'
 	find . $(FIND_EXCLUDE) -type f \
 	\( -name "*.ml" -o -name "*.mli" -o -name "*.mll" -o -name "*.mly" \
 	-o -name "*.c" -o -name "*.h" \
 	-o -name "dune" -o -name "dune-project" -o -name "Makefile" \
-	-o -name "Dockerfile.*" -o -name "*.ini"  \) \
-	-exec headache -c headers/headache_config.txt -h headers/CEA_LGPL21 {} \; 
+	-o -name "Dockerfile.*" -o -name "*.ini" -o -name "*.el" \) \
+	-exec headache -c headers/headache_config.txt -h headers/CEA_LGPL21 {} \;
 
 
 
@@ -86,6 +134,7 @@ EXTRA_EXCLUDE += -not -name 'dune-project'
 EXTRA_EXCLUDE += -not -name 'Makefile'
 EXTRA_EXCLUDE += -not -name 'Dockerfile.*'
 EXTRA_EXCLUDE += -not -name '*.ini'
+EXTRA_EXCLUDE += -not -name '*.el'
 EXTRA_EXCLUDE += -not -path './*.exp_dump'
 EXTRA_EXCLUDE += -not -path './*.dump'
 EXTRA_EXCLUDE += -not -path './*.result'
@@ -94,7 +143,22 @@ EXTRA_EXCLUDE += -not -path './*.exe'
 EXTRA_EXCLUDE += -not -path './*.orig'
 EXTRA_EXCLUDE += -not -path './*.patch'
 
-
-check_missing_files:
+.PHONY: check_missing_files
+check_missing_files: ## Check for files not update by update_headers
 	@echo "Generating the list of files whose headers we do not maintain"
-	find . -type f $(EXTRA_EXCLUDE) -print 
+	find . -type f $(EXTRA_EXCLUDE) -print
+
+source-distrib:
+	CUR=`git log -1 | head -n 1 | cut -d ' ' -f 2`; \
+	cd `mktemp -d --suffix codex` && \
+	git clone $(PWD) codex-$$CUR && \
+	rm -Rf codex-$$CUR/.git && \
+	rm -Rf codex-$$CUR/tests && \
+	rm -Rf codex-$$CUR/frama-c/tests && \
+	tar czf codex-$$CUR.tar.gz codex-$$CUR && \
+	echo "Created file "`pwd`"/codex-"$$CUR".tar.gz"
+
+.PHONY: help
+help:: ## Show this help
+	@echo "$(color_yellow)make codex:$(color_reset) list of useful targets :"
+	@egrep -h '\s##\s' $(MAKEFILE_LIST) | sort | awk 'BEGIN {FS = ":.*?## "}; {printf "  $(color_blue)%-$(HELP_PADDING)s$(color_reset) %s\n", $$1, $$2}'

README.org

@@ -34,7 +34,41 @@ The simplest way to try Binsec/Codex and Frama-C/Codex is to download the compil
 
 (note that framac_codex.exe is a stripped version of Frama-C, with no plugins and support for compiler builtins removed)
 
-** From source code
+** Install from source
+
+The easiest way is to use opam ( https://opam.ocaml.org/ ).
+
+Just locally pin the package with:
+
+#+begin_src shell
+$ opam pin . -n
+#+end_src
+
+You can then install the different packages:
+
+#+begin_src shell
+$ opam install codex # For the codex library
+$ opam install binsec_codex # For the binsec_codex executable
+$ opam install frama_c_codex # For the frama_c_codex executable.
+#+end_src
+
+You can also install the Frama-c/Codex plugin if you already have a version of Frama-C installed.
+
+#+begin_src shell
+$ opam install frama_c_codex_plugin
+#+end_src
+
+*** Testing your frama_c_codex installation
+
+You can test that frama_c_codex is working by typing:
+
+#+begin_src shell
+frama_c_codex -no-plugin-autoload -machdep x86_32 -codex test.c -codex-use-type-domain -codex-type-file frama-c/test.types  -codex-html-dump output.html
+#+end_src
+
+This should output an output.html with the results of the analysis, that you can inspect using your browser.
+
+** Working from source code locally
 
 *** Prerequisites
 
@@ -49,21 +83,22 @@ Install opam:
 Install the dependencies:
 
 #+begin_src shell
-opam install frama-c binsec lmdb llvm qcheck-core ppx_inline_test sexplib mlcuddidl bheap
+opam install frama-c binsec lmdb qcheck-core ppx_inline_test sexplib mlcuddidl bheap pacomb
 #+end_src
 
-*** Installing the codex library
+Note: there is a bug in Frama-C >= 28.0 that breaks some of the testsg, so stick to 27.1 if this matters to you (e.g. if you develop new Codex features).
+
+*** Building the codex library
 
 #+begin_src shell
 dune build
 #+end_src
 
-*** Installing Binsec/Codex
+*** Building Binsec/Codex
 
 #+begin_src shell
   opam install binsec
   dune build binsec/binsec_codex.exe
-  dune install binsec/binsec_codex.exe
 #+end_src
 
 *** Installing Frama-C/Codex