Skip to content

Add csyntaxgen tool for exporting CompCert C (Csyntax) AST as .v file #404

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
btj wants to merge 4 commits into from
Closed

Add csyntaxgen tool for exporting CompCert C (Csyntax) AST as .v file #404

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
71ea0d7
Copied exportclight into exportcsyntax
btj Jul 28, 2021
f9257bc
csyntaxgen tool
btj Jul 30, 2021
2cb2c6a
Copied test/clightgen to test/csyntaxgen
btj Jul 30, 2021
8d0d2c2
csyntaxgen test suite
btj Jul 30, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,8 @@
/ccomp.prof
/clightgen
/clightgen.byte
/csyntaxgen
/csyntaxgen.byte
/tools/ndfun
/tools/modorder
/Makefile.config
Expand Down Expand Up @@ -75,6 +77,7 @@
.DS_Store
# Test generated data
/test/clightgen/*.v
/test/csyntaxgen/*.v
# Coq caches
.lia.cache
.nia.cache
Expand Down
13 changes: 12 additions & 1 deletion Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ else
ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH)
endif

DIRS := lib common $(ARCHDIRS) backend cfrontend driver exportclight cparser
DIRS := lib common $(ARCHDIRS) backend cfrontend driver exportclight exportcsyntax cparser

COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(d))

Expand Down Expand Up @@ -179,6 +179,9 @@ endif
ifeq ($(CLIGHTGEN),true)
$(MAKE) clightgen
endif
ifeq ($(CSYNTAXGEN),true)
$(MAKE) csyntaxgen
endif
ifeq ($(INSTALL_COQDEV),true)
$(MAKE) compcert.config
endif
Expand Down Expand Up @@ -208,6 +211,11 @@ clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.m
clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE
$(MAKE) -f Makefile.extr clightgen.byte

csyntaxgen: .depend.extr compcert.ini exportcsyntax/Csyntaxdefs.vo driver/Version.ml FORCE
$(MAKE) -f Makefile.extr csyntaxgen
csyntaxgen.byte: .depend.extr compcert.ini exportcsyntax/Csyntaxdefs.vo driver/Version.ml FORCE
$(MAKE) -f Makefile.extr csyntaxgen.byte

runtime:
$(MAKE) -C runtime

Expand Down Expand Up @@ -310,6 +318,9 @@ install:
ifeq ($(CLIGHTGEN),true)
install -m 0755 ./clightgen $(DESTDIR)$(BINDIR)
endif
ifeq ($(CSYNTAXGEN),true)
install -m 0755 ./csyntaxgen $(DESTDIR)$(BINDIR)
endif
ifeq ($(INSTALL_COQDEV),true)
install -d $(DESTDIR)$(COQDEVDIR)
for d in $(DIRS); do \
Expand Down
20 changes: 18 additions & 2 deletions Makefile.extr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ cparser/pre_parser_messages.ml:

DIRS=extraction \
lib common $(ARCH) backend cfrontend cparser driver \
exportclight debug
exportclight exportcsyntax debug

INCLUDES=$(patsubst %,-I %, $(DIRS))

Expand Down Expand Up @@ -89,7 +89,7 @@ LEXERS=cparser/Lexer.mll lib/Tokenize.mll \
LIBS=str.cmxa unix.cmxa $(MENHIR_LIBS)
LIBS_BYTE=$(patsubst %.cmxa,%.cma,$(patsubst %.cmx,%.cmo,$(LIBS)))

EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte
EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte csyntaxgen csyntaxgen.byte
GENERATED=$(PARSERS:.mly=.mli) $(PARSERS:.mly=.ml) $(LEXERS:.mll=.ml) cparser/pre_parser_messages.ml

# Beginning of part that assumes .depend.extr already exists
Expand Down Expand Up @@ -128,6 +128,22 @@ clightgen.byte: $(CLIGHTGEN_OBJS:.cmx=.cmo)
@echo "Linking $@"
@$(OCAMLC) -o $@ $(LIBS_BYTE) $+

CSYNTAXGEN_OBJS:=$(shell $(MODORDER) exportcsyntax/Csyntaxgen.cmx)

ifeq ($(OCAML_NATIVE_COMP),true)
csyntaxgen: $(CSYNTAXGEN_OBJS)
@echo "Linking $@"
@$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+
else
csyntaxgen: csyntaxgen.byte
@echo "Copying to $@"
@$(COPY) $+ $@
endif

csyntaxgen.byte: $(CSYNTAXGEN_OBJS:.cmx=.cmo)
@echo "Linking $@"
@$(OCAMLC) -o $@ $(LIBS_BYTE) $+

include .depend.extr

endif
Expand Down
13 changes: 12 additions & 1 deletion configure
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ target=''
has_runtime_lib=true
has_standard_headers=true
clightgen=false
csyntaxgen=false
install_coqdev=false
ignore_coq_version=false
library_Flocq=local
Expand Down Expand Up @@ -95,7 +96,8 @@ Options:
-no-runtime-lib Do not compile nor install the runtime support library
-no-standard-headers Do not install nor use the standard .h headers
-clightgen Also compile and install the clightgen tool
-install-coqdev Also install the Coq development (implied by -clightgen)
-csyntaxgen Also compile and install the csyntaxgen tool
-install-coqdev Also install the Coq development (implied by -clightgen and -csyntaxgen)
-ignore-coq-version Accept to use experimental or unsupported versions of Coq
'

Expand Down Expand Up @@ -130,6 +132,9 @@ while : ; do
-clightgen)
clightgen=true
install_coqdev=true;;
-csyntaxgen)
csyntaxgen=true
install_coqdev=true;;
-ignore-coq-version|--ignore-coq-version)
ignore_coq_version=true;;
-install-coqdev|--install-coqdev|-install-coq-dev|--install-coq-dev)
Expand Down Expand Up @@ -639,6 +644,7 @@ CASM_OPTIONS=$casm_options
CASMRUNTIME=$casmruntime
CC=$cc $cc_options
CLIGHTGEN=$clightgen
CSYNTAXGEN=$csyntaxgen
CLINKER=$clinker
CLINKER_OPTIONS=$clinker_options
CPREPRO=$cprepro
Expand Down Expand Up @@ -750,6 +756,9 @@ ASM_SUPPORTS_CFI=false
# Turn on/off compilation of clightgen
CLIGHTGEN=false

# Turn on/off compilation of csyntaxgen
CSYNTAXGEN=false

# Whether the other tools support responsefiles in GNU syntax or Diab syntax
RESPONSEFILE=gnu # diab

Expand All @@ -771,6 +780,7 @@ S cfrontend
S driver
S debug
S exportclight
S exportcsyntax
S cparser
S extraction

Expand All @@ -782,6 +792,7 @@ B cfrontend
B driver
B debug
B exportclight
B exportcsyntax
B cparser
B extraction
EOF
Expand Down
Loading