v0.1

Caml.mk

+##########################################################################
+#  This file is part of Binsec.                                          #
+#                                                                        #
+#  Copyright (C) 2016-2017                                               #
+#    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).            #
+#                                                                        #
+##########################################################################
+
+.PHONY: default all bin byt clean cleandir configure depend beforedepend
+
+# Compilation rules
+.SUFFIXES: .o .c
+.SUFFIXES: .cmx .cmxa .cmo .cmi .cma .ml .mli .mll .mly
+
+.cmo.o:
+	$(PP) "COBJ $@"
+	$(CAMLBYT) -custom -output-obj -o $@ $<
+
+.c.o:
+	$(CAMLBYT) -ccopt "-fPIC -o $@" -c $<
+
+.ml.cmo:
+	$(PP_BYT) $@
+	$(CAMLBYT)  $(CAMLINCLUDES) $(CAMLFLAGS) $(CAMLWARNINGS) -c $<
+
+.mli.cmi:
+	$(PP_BYT) $@
+	$(CAMLBYT)  $(CAMLINCLUDES) -c $<
+
+.ml.cmx:
+	$(PP_OPT) $@
+	$(CAMLBIN) $(CAMLINCLUDES) $(CAMLFLAGS) $(CAMLWARNINGS) -c $<
+
+.mly.ml:
+	$(PP_YACC) $@
+	$(CAMLYAC) $(CAMLYACOPTS) $<
+
+.mly.mli:
+	$(PP_YACC) $@
+	$(CAMLYAC)  $(CAMLYACOPTS) $<
+
+.mll.ml:
+	$(PP_LEX) $@
+	$(CAMLLEX) $(CAMLLEXOPTS) $<
+
+# Generic clean up
+cleandir::
+	$(RRM) *.cm[ioxa] *.cmxa *.o *.a *.annot *.obj *.lib *~ .*~ a.out .\#*
+
+
+configure:: cleandir
+
+# Rebuilding dependencies
+depend:: beforedepend
+	$(CAMLDEP) $(CAMLINCLUDES) $(CAMLFILES) > .depend
+
+include .depend

Config.mk.in

+##########################################################################
+#  This file is part of Binsec.                                          #
+#                                                                        #
+#  Copyright (C) 2016-2017                                               #
+#    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).            #
+#                                                                        #
+##########################################################################
+
+CAMLC		?=@OCAMLC@
+CAMLOPT		?=@OCAMLOPT@
+CAMLLEX		?=@OCAMLLEX@
+CAMLLEXOPTS?	?=
+CAMLYAC		?=@MENHIR@
+CAMLYACOPTS	?=
+CAMLDEP		?=@OCAMLDEP@
+CAMLWARNINGS?	?=-w +a-4-3
+CAMLFLAGS?	?=-g -annot
+CAMLDOC		?=@OCAMLDOC@
+CAMLFIND	?=@OCAMLFIND@
+BEST		?=@OCAMLBEST@
+
+OCAMLBUILD?=@OCAMLBUILD@
+OCB_OPTIONS?=-use-ocamlfind -no-hygiene -libs str,bigarray -I .
+
+PIQI ?=@PIQI@
+PIQI_FLAGS ?= of-proto -I $(PROTO_DIR)
+
+PROTOC ?=@PROTOC@
+PROTOC_FLAGS ?= --proto_path=$(BINSEC_DIR)/$(PROTO_DIR) --cpp_out=$(CPP_PROTOBUF_DIR)
+
+PIQI2CAML ?=@PIQI2CAML@
+PIQI2CAML_FLAGS ?= --multi-format -C $(PIQI_DIR) 
+
+DESTDIR         ?=
+prefix          ?=@prefix@
+exec_prefix     ?=@exec_prefix@
+datarootdir     ?=@datarootdir@
+datadir         ?=@datadir@
+BINDIR          ?="$(DESTDIR)@bindir@"
+LIBDIR          ?="$(DESTDIR)@libdir@"
+DATADIR         ?="$(DESTDIR)@datarootdir@"
+MANDIR          ?="$(DESTDIR)@mandir@"
+
+VERBOSEMAKE?=no
+
+ifneq ($(VERBOSEMAKE),no) # Do not change to ifeq ($(VERBOSEMAKE),yes), as this
+			  # version makes it easier for the user to set the
+			  # option on the command-line to investigate
+			  # Makefile-related problems
+# ignore the PRINT_* materials but print all the other commands
+  PP = @true
+# prevent the warning "jobserver unavailable: using -j1".
+# see GNU make manual (section 5.7.1 and appendix B)
+  QUIET_MAKE:= + $(MAKE)
+# prevent the warning: "-jN forced in submake: disabling jobserver mode".
+# see GNU make manual (appendix B)
+  MAKE := MAKEFLAGS="$(patsubst j,,$(MAKEFLAGS))" $(MAKE)
+else
+# print the PP_* materials
+  PP = @echo
+# but silently execute all the other commands
+# fixed bug #637: do not write spaces between flags
+  OLDFLAGS:=r$(MAKEFLAGS)
+  MAKEFLAGS:=rs$(MAKEFLAGS)
+# do not silently execute other makefiles (e.g the one of why):
+# the redefinition of MAKE below is for this purpose
+# but use QUIET_MAKE in order to call silently the initial Makefile
+  QUIET_MAKE:= $(MAKE)
+  MAKE := MAKEFLAGS="$(OLDFLAGS)" $(MAKE)
+endif
+
+PP_BYT   = $(PP) 'BYT  '
+PP_OPT   = $(PP) 'BIN  '
+PP_YACC  = $(PP) 'MENHIR '
+PP_LEX   = $(PP) 'LEX  '
+
+RM ?= rm -rf
+RRM ?= rm -rf
+CP ?= cp -r
+MKDIR ?= mkdir -p
+CD ?= cd
+TAR ?= tar cvzf
+INSTALL ?= install
+
+HEADACHE=@HEADACHE@
+HEADACHE_CONFIG?=headers/headache_config.txt
+
+DOT2SVG = dot -Tsvg
+
+%.svg : %.dot
+	$(DOT2SVG) -o $@ $<

Makefile

+##########################################################################
+#  This file is part of Binsec.                                          #
+#                                                                        #
+#  Copyright (C) 2016-2017                                               #
+#    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).            #
+#                                                                        #
+##########################################################################
+
+all : binsec pinsec
+
+# The order of includes is important
+# Piqi.mk depends on values set from Config.mk
+include Config.mk
+include Piqi.mk
+
+
+PINSEC_DIR = pinsec
+PINSEC_BUILD_DIR = $(PINSEC_DIR)/build
+CMAKE = cmake
+PIN_ROOT_DIR ?= pin-2.14-71313-gcc.4.4.7-linux
+pinsec: protoc
+	$(MKDIR) $(PINSEC_BUILD_DIR)
+	$(PP) "Using PIN from $(PIN_ROOT_DIR)"
+	($(CD) $(PINSEC_BUILD_DIR); \
+	$(CMAKE) -DPIN_ROOT_DIR=$(PIN_ROOT_DIR) ..)
+	$(PP) "Finish the build with cd $(PINSEC_BUILD_DIR); make"
+
+.PHONY: pinsec-clean pinsec
+pinsec-clean:
+	$(RRM) $(PINSEC_BUILD_DIR)
+
+
+BINSEC_DIR = src
+binsec:
+	$(MAKE) -C $(BINSEC_DIR)
+
+binsec-clean:
+	$(MAKE) -C $(BINSEC_DIR) clean
+
+clean:: binsec-clean pinsec-clean
+
+clean-configure:
+	$(RRM) autom4te.cache config.status configure
+
+veryclean: clean clean-configure
+
+
+.PHONY: tests
+tests:
+	$(MAKE) -C tests
+
+
+include $(PINSEC_DIR)/Targets.mk
+include $(BINSEC_DIR)/Targets.mk

Piqi.mk

+##########################################################################
+#  This file is part of Binsec.                                          #
+#                                                                        #
+#  Copyright (C) 2016-2017                                               #
+#    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).            #
+#                                                                        #
+##########################################################################
+
+.SUFFIXES: .piqi .proto .pb.cc
+
+%_piqi.ml %_ext.ml: %.piqi
+	$(PP) 'PIQIML $@'
+	$(PIQI2CAML) $(PIQI2CAML_FLAGS) $<
+
+$(PIQI_DIR)/%.piqi: $(PROTO_DIR)/%.proto
+	$(PP) 'PIQI $@'
+	$(PIQI) $(PIQI_FLAGS) -o $@ $<
+
+CPP_PROTOBUF_DIR = $(PINSEC_DIR)/$(PINSEC_TYPES_DIR)/protobuf
+
+.PHONY: pre-protoc
+
+pre-protoc:
+	$(MKDIR) $(CPP_PROTOBUF_DIR)
+
+%.pb.cc: src/proto/%.proto
+	$(PP) 'PROTOC $@'
+	$(PROTOC) $(PROTOC_FLAGS) $<
+
+PROTOC_FILES = $(PROTO_SRC_FILES:%=$(CPP_PROTOBUF_DIR)/%.pb.cc)
+
+$(PROTOC_FILES) : pre-protoc
+
+PROTO_LSRC_FILES = $(PROTO_FILES:%=$(BINSEC_DIR)/%)
+
+protoc: pre-protoc $(PROTO_LSRC_FILES)
+	$(PROTOC) $(PROTOC_FLAGS) $(PROTO_LSRC_FILES)
+
+clean::
+	$(RRM) $(CPP_PROTOBUF_DIR)
+
+.PHONY: prepiqi
+prepiqi:
+	$(MKDIR) $(PIQI_DIR)
+
+$(PIQI_FILES): prepiqi
+$(PIQI_ML_FILES) : $(PIQI_FILES)
+piqi-ml : $(PIQI_ML_FILES)

README

+# Compilation #
+
+## BINSEC 
+
+The following usual steps should do the trick:
+
+```
+% ./configure
+% make binsec
+```
+
+To install `BINSEC`, do `cd src; make install`.
+
+## PINSEC
+
+```
+% ./configure
+% make pinsec
+```
+
+Then, go to the directory pinsec/build, and configure your build.
+
+The build needs `CMake`.
+
+
+# Use
+
+## BINSEC
+
+In the `src` directory.
+
+- List of available commands:
+     ./binsec --help
+
+ - Help about a specific command:
+     ./binsec COMMAND --help
+
+
+### Simple examples ###
+
+
+- Linear (objdump-like) disassembly of text section
+
+    ```
+    ./binsec disasm -sections .text -dmode linear BINARY_FILE
+    ```
+
+- Recursive disassembly of text section
+
+    ```
+    ./binsec disasm -sections .text -dmode rec BINARY_FILE
+    ```
+
+- Simulation:
+
+    ```
+    ./binsec simulate -entrypoint INIT_ADDR BINARY_FILE
+    ```
+
+

configure.ac

+##########################################################################
+#  This file is part of Binsec.                                          #
+#                                                                        #
+#  Copyright (C) 2016-2017                                               #
+#    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).            #
+#                                                                        #
+##########################################################################
+
+AC_INIT()
+
+has_or_die ()
+{
+    if test "$1" = no; then
+        AC_MSG_ERROR($2)
+    fi
+}
+
+has_lib_or_die ()
+{
+    if test "$1" = ""; then
+        AC_MSG_ERROR($2)
+    fi
+}
+
+AC_CHECK_PROG(MAKE, make, make, no)
+
+AC_CHECK_PROG(OCAMLFIND, ocamlfind, ocamlfind, no)
+has_or_die $OCAMLFIND "Could not find ocamlfind"
+
+# ocamlc bytecode compiler
+AC_CHECK_PROG(OCAMLC,ocamlc,ocamlc,no)
+if test "$OCAMLC" = no; then
+    AC_MSG_ERROR("Could not find ocamlc.")
+else
+    AC_CHECK_PROG(OCAMLCDOTOPT,ocamlc.opt,ocamlc.opt, no)
+    if test "$OCAMLCDOTOPT" != no; then
+        OCAMLC=$OCAMLCDOTOPT
+    fi
+    OCAMLBEST=byt
+fi
+
+AC_MSG_CHECKING([version of OCaml])
+OCAMLCVERSION=`$OCAMLC -version`
+LEAST_VERSION="4.02.1"
+case $OCAMLCVERSION in
+     4.02*) AS_ECHO("Good! ($OCAMLCVERSION)");;
+     4.03*) AS_ECHO("Good! ($OCAMLCVERSION)");;
+     4.04*) AS_ECHO("Good! ($OCAMLCVERSION)");;
+     *) AC_MSG_ERROR("Please use at least $LEAST_VERSION (found $OCAMLCVERSION).");;
+esac
+
+
+# ocamlopt native compiler
+AC_CHECK_PROG(OCAMLOPT, ocamlopt, ocamlopt, no)
+
+if test "$OCAMLOPT" = no; then
+    AC_MSG_WARN("Bytecode compilation only.")
+else
+    AC_CHECK_PROG(OCAMLOPTDOTOPT,ocamlopt.opt,ocamlopt.opt,no)
+    if test "$OCAMLOPTDOTOPT" != no; then
+        OCAMLOPT=$OCAMLOPTDOTOPT
+    fi
+    OCAMLOPTVERSION=`$OCAMLOPT -version`
+    OCAMLBEST=opt
+    if test "$OCAMLOPTVERSION" != "$OCAMLCVERSION"; then
+       AC_MSG_ERROR("OCaml bytecode and optimized compilers have version number conflicts ($OCAMLCVERSION) vs ($OCAMLOPTVERSION) . Should be the same")
+    fi
+fi
+
+# ocamlbuild
+AC_CHECK_PROG(OCAMLBUILD,ocamlbuild,ocamlbuild,no)
+has_or_die $OCAMLBUILD "Could not find ocamlbuild"
+
+OCB_OPTIONS="-use-ocamlfind -no-hygiene -lflags ../loader_ml.o -libs nums,str -I ."
+
+AC_SUBST(OCAMLBUILD)
+AC_SUBST(OCB_OPTIONS)
+
+
+# ocamldep
+AC_CHECK_PROG(OCAMLDEP,ocamldep,ocamldep, no)
+has_or_die $OCAMLDEP "Could not find ocamldep"
+OCAMLDEPVERSION=`ocamldep -version | sed -e 's/ocamldep, version \(.*\)/\1/'`
+if test "$OCAMLDEPVERSION" != "$OCAMLCVERSION"; then
+       AC_MSG_ERROR("ocamldep version $OCAMLCVERSION conflicts with ocamlc version $OCAMLCVERSION. Should be the same.")
+fi
+
+# ocamllex
+AC_CHECK_PROG(OCAMLLEX,ocamllex,ocamllex,no)
+has_or_die $OCAMLLEX "Could not find ocamllex"
+
+# menhir
+AC_CHECK_PROG(MENHIR,menhir,menhir,no)
+has_or_die $MENHIR  "Could not find menhir"
+
+# Checking other libraries
+# Each check updates the LIB_FOUND variable to "yes" or "no"
+# and MYLIBPATH to the actual path found if needed
+LIB_FOUND="no"
+MYLIBPATH=""
+check_lib ()
+{
+  LIB_FOUND="no"
+  AC_MSG_CHECKING(for library $1)
+  MYLIBPATH=$($OCAMLFIND query $1 2>/dev/null | tr -d '\r\n')
+  has_lib_or_die $MYLIBPATH "Could not find $1"
+  AC_MSG_RESULT($MYLIBPATH)
+  if test "$MYLIBPATH" = ""; then
+     LIB_FOUND="no"
+  else
+     LIB_FOUND="yes"
+  fi
+  return 0
+}
+
+
+check_lib "ocamlgraph"
+OCAMLGRAPH=$MYLIBPATH
+if test "$LIB_FOUND" = "no"; then
+  AC_MSG_ERROR("ocamlgraph not found")
+fi
+
+check_lib "piqilib"
+PIQILIB=$MYLIBPATH
+if test "$LIB_FOUND" = "no"; then
+  AC_MSG_ERROR("piqilib not found")
+fi
+
+check_lib "zarith"
+ZARITH=$MYLIBPATH
+if test "$LIB_FOUND" = "no"; then
+  AC_MSG_ERROR("zarith not found")
+fi
+
+check_lib "ZMQ"
+ZMQ=$MYLIBPATH
+if test "$LIB_FOUND" = "no"; then
+  AC_MSG_ERROR("zmq not found")
+fi
+
+check_lib "llvm"
+LLVM=$MYLIBPATH
+if test "$LIB_FOUND" = "no"; then
+  AC_MSG_ERROR("llvm not found")
+fi
+
+
+
+AC_CHECK_PROG(PIQI, piqi, piqi, no)
+has_or_die $PIQI "Could not find piqi"
+
+AC_CHECK_PROG(PIQI2CAML, piqic-ocaml , piqic-ocaml, no)
+has_or_die $PIQI2CAML "Could not find piqic-ocaml"
+
+AC_CHECK_PROG(PROTOC, protoc, protoc, no)
+has_or_die $PROTOC "Could not find protoc"
+
+
+
+# Optional libraries #
+## ocamldoc
+AC_CHECK_PROG(OCAMLDOC, ocamldoc, ocamldoc, no)
+if test "$OCAMLDOC" = no; then
+    AC_MSG_WARN("Documentation generation disabled.")
+else
+    OCAMLDOCVERSION=`ocamldoc -version`
+fi
+
+
+AC_CHECK_PROG(CMAKE, cmake, cmake, no)
+if test "$CMAKE" = no; then
+   AC_MSG_WARN("You will not be able to compile PINSEC")
+fi
+
+## headache
+AC_CHECK_PROG(HEADACHE, headache, headache, no)
+if test "$HEADACHE" = no; then
+    AC_MSG_WARN("License generation disabled.")
+fi
+
+AC_CHECK_PROG(DOT, dot, dot, no)
+if test "$DOT" = no; then
+    AC_MSG_WARN("dot not found: disabling documentation generation.")
+fi
+
+## SMT Provers ##
+AC_CHECK_PROG(Z3, z3, z3, no)
+if test "$Z3" = no; then
+    AC_MSG_WARN("z3 not found: some parts of binsec might not work.")
+fi
+
+AC_CHECK_PROG(CVC4, cvc4, cvc4, no)
+if test "$CVC4" = no; then
+    AC_MSG_WARN("cvc4 not found: some parts of binsec might not work.")
+fi
+
+AC_CHECK_PROG(YICES, yices-smt2, yices-smt2, no)
+if test "$YICES" = no; then
+    AC_MSG_WARN("yices-smt2 not found: some parts of binsec might not work.")
+fi
+
+AC_CHECK_PROG(BOOLECTOR, boolector, boolector, no)
+if test "$BOOLECTOR" = no; then
+    AC_MSG_WARN("boolector not found: some parts of binsec might not work.")
+fi
+
+
+# Substitutions #
+
+AC_SUBST(OCAMLC)
+AC_SUBST(OCAMLOPT)
+AC_SUBST(OCAMLDEP)
+AC_SUBST(OCAMLLEX)
+AC_SUBST(MENHIR)
+AC_SUBST(OCAMLDOC)
+AC_SUBST(OCAMLFIND)
+AC_SUBST(OCAMLBEST)
+AC_SUBST(HEADACHE)
+AC_SUBST(PIQI)
+AC_SUBST(PIQI2CAML)
+AC_SUBST(PROTOC)
+
+AC_CONFIG_FILES([Config.mk], [chmod a-w Config.mk])
+AC_OUTPUT()
+
+depend_file="src/.depend"
+AS_ECHO(".depend: touching ${depend_file}")
+touch ${depend_file}
+
+AS_ECHO("")
+AS_ECHO("")
+AS_ECHO("Configuration summary")
+AS_ECHO("---------------------")
+AS_ECHO("ocamlc: $OCAMLC $OCAMLCVERSION")
+AS_ECHO("ocamlopt: $OCAMLOPT $OCAMLOPTVERSION")
+AS_ECHO("ocamldep: $OCAMLDEP $OCAMLDEPVERSION")
+AS_ECHO("ocamllex: $OCAMLLEX")
+AS_ECHO("menhir: $MENHIR")
+AS_ECHO("ocamldoc: $OCAMLDOC $OCAMLDOCVERSION")
+AS_ECHO("target: $OCAMLBEST")
+AS_ECHO("headache: $HEADACHE")

opam/files/run_autoconf_if_needed.sh

+#!/bin/sh -eux
+
+if [ ! -f "configure" ]; then
+  autoconf
+fi

opam/files/run_configure.sh

+#!/bin/sh -eux
+
+
+exec ./configure "$@"