diff options
-rw-r--r-- | Makefile | 17 | ||||
-rw-r--r-- | _tags | 2 | ||||
-rw-r--r-- | exportclight/Clightdefs.v | 53 | ||||
-rw-r--r-- | exportclight/Clightgen.ml (renamed from driver/Clightgen.ml) | 0 | ||||
-rw-r--r-- | exportclight/ExportClight.ml (renamed from cfrontend/ExportClight.ml) | 37 | ||||
-rw-r--r-- | exportclight/README | 34 |
6 files changed, 99 insertions, 44 deletions
@@ -33,6 +33,9 @@ OCB_OPTIONS_CHECKLINK=\ $(OCB_OPTIONS) \ -I checklink \ -use-ocamlfind +OCB_OPTIONS_CLIGHTGEN=\ + $(OCB_OPTIONS) \ + -I exportclight VPATH=$(DIRS) GPATH=$(DIRS) @@ -154,13 +157,13 @@ cchecklink.byte: driver/Configuration.ml $(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.d.byte \ && rm -f cchecklink.byte && $(SLN) _build/checklink/Validator.d.byte cchecklink.byte -clightgen: extraction/STAMP driver/Configuration.ml - $(OCAMLBUILD) $(OCB_OPTIONS) Clightgen.native \ - && rm -f clightgen && $(SLN) _build/driver/Clightgen.native clightgen +clightgen: extraction/STAMP driver/Configuration.ml exportclight/Clightdefs.vo + $(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.native \ + && rm -f clightgen && $(SLN) _build/exportclight/Clightgen.native clightgen -clightgen.byte: extraction/STAMP driver/Configuration.ml - $(OCAMLBUILD) $(OCB_OPTIONS) Clightgen.d.byte \ - && rm -f clightgen.byte && $(SLN) _build/driver/Clightgen.d.byte clightgen.byte +clightgen.byte: extraction/STAMP driver/Configuration.ml exportclight/Clightdefs.vo + $(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.d.byte \ + && rm -f clightgen.byte && $(SLN) _build/exportclight/Clightgen.d.byte clightgen.byte .PHONY: proof extraction ccomp ccomp.prof ccomp.byte runtime cchecklink cchecklink.byte clightgen clightgen.byte @@ -222,7 +225,7 @@ endif $(MAKE) -C runtime install clean: - rm -f $(patsubst %, %/*.vo, $(DIRS)) + rm -f $(patsubst %, %/*.vo, $(DIRS) exportclight) rm -f ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte rm -rf _build rm -rf doc/html doc/*.glob @@ -1,4 +1,4 @@ <driver/Driver.*{byte,native}>: use_unix,use_str,use_Cparser -<driver/Clightgen.*{byte,native}>: use_unix,use_str,use_Cparser +<exportclight/Clightgen.*{byte,native}>: use_unix,use_str,use_Cparser <checklink/*.ml>: pkg_bitstring,warn_error_A <checklink/Validator.*{byte,native}>: pkg_unix,pkg_str,pkg_bitstring,use_Cparser diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v new file mode 100644 index 00000000..4c3c942a --- /dev/null +++ b/exportclight/Clightdefs.v @@ -0,0 +1,53 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** All imports and definitions used by .v Clight files generated by clightgen *) + +Require Export List. +Require Export ZArith. +Require Export Integers. +Require Export Floats. +Require Export AST. +Require Export Ctypes. +Require Export Cop. +Require Export Clight. + +Definition tvoid := Tvoid. +Definition tschar := Tint I8 Signed noattr. +Definition tuchar := Tint I8 Unsigned noattr. +Definition tshort := Tint I16 Signed noattr. +Definition tushort := Tint I16 Unsigned noattr. +Definition tint := Tint I32 Signed noattr. +Definition tuint := Tint I32 Unsigned noattr. +Definition tbool := Tint IBool Unsigned noattr. +Definition tfloat := Tfloat F32 noattr. +Definition tdouble := Tfloat F64 noattr. +Definition tptr (t: type) := Tpointer t noattr. +Definition tarray (t: type) (sz: Z) := Tarray t sz noattr. + +Definition volatile_attr := {| attr_volatile := true |}. + +Definition tvolatile (ty: type) := + match ty with + | Tvoid => Tvoid + | Tint sz si a => Tint sz si volatile_attr + | Tfloat sz a => Tfloat sz volatile_attr + | Tpointer elt a => Tpointer elt volatile_attr + | Tarray elt sz a => Tarray elt sz volatile_attr + | Tfunction args res => Tfunction args res + | Tstruct id fld a => Tstruct id fld volatile_attr + | Tunion id fld a => Tunion id fld volatile_attr + | Tcomp_ptr id a => Tcomp_ptr id volatile_attr + end. diff --git a/driver/Clightgen.ml b/exportclight/Clightgen.ml index 1805573e..1805573e 100644 --- a/driver/Clightgen.ml +++ b/exportclight/Clightgen.ml diff --git a/cfrontend/ExportClight.ml b/exportclight/ExportClight.ml index d7a80a56..452693c3 100644 --- a/cfrontend/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -480,45 +480,10 @@ let print_assertions p = (* The prologue *) let prologue = "\ -Require Import List. -Require Import ZArith. -Require Import Integers. -Require Import Floats. -Require Import AST. -Require Import Ctypes. -Require Import Cop. -Require Import Clight. +Require Import Clightdefs. Local Open Scope Z_scope. -Definition tvoid := Tvoid. -Definition tschar := Tint I8 Signed noattr. -Definition tuchar := Tint I8 Unsigned noattr. -Definition tshort := Tint I16 Signed noattr. -Definition tushort := Tint I16 Unsigned noattr. -Definition tint := Tint I32 Signed noattr. -Definition tuint := Tint I32 Unsigned noattr. -Definition tbool := Tint IBool Unsigned noattr. -Definition tfloat := Tfloat F32 noattr. -Definition tdouble := Tfloat F64 noattr. -Definition tptr (t: type) := Tpointer t noattr. -Definition tarray (t: type) (sz: Z) := Tarray t sz noattr. - -Definition volatile_attr := {| attr_volatile := true |}. - -Definition tvolatile (ty: type) := - match ty with - | Tvoid => Tvoid - | Tint sz si a => Tint sz si volatile_attr - | Tfloat sz a => Tfloat sz volatile_attr - | Tpointer elt a => Tpointer elt volatile_attr - | Tarray elt sz a => Tarray elt sz volatile_attr - | Tfunction args res => Tfunction args res - | Tstruct id fld a => Tstruct id fld volatile_attr - | Tunion id fld a => Tunion id fld volatile_attr - | Tcomp_ptr id a => Tcomp_ptr id volatile_attr - end. - " (* All together *) diff --git a/exportclight/README b/exportclight/README new file mode 100644 index 00000000..3fd8c0ae --- /dev/null +++ b/exportclight/README @@ -0,0 +1,34 @@ + The clightgen tool + ------------------ + +OVERVIEW + +"clightgen" is an experimental tool that transforms C source files +into Clight abstract syntax, pretty-printed in Coq format in .v files. +These generated .v files can be loaded in a Coq session for +interactive verification, typically. + + +HOW TO BUILD + +Change to the top-level CompCert directory and issue + + make clightgen + + +USAGE + + clightgen [options] <C source files> + +For each source file "src.c", its Clight abstract syntax is generated +in "src.v". + +The options recognized are a subset of those of the CompCert compiler ccomp +(see http://compcert.inria.fr/man/manual003.html for full documentation): + + -I<dir> search <dir> for include files + -D<symbol> define preprocessor macro + -U<symbol> undefine preprocessor macro + -Wp,<opts> pass options to C preprocessor + -f<feature> activate emulation of the given C feature + |