Commit 471a8363 authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

Merge branch 'kvx-work' into aarch64-peephole

parents a71ed694 a644da35
......@@ -21,6 +21,7 @@
# Emacs saves
*~
# Executables and configuration
/tools/compiler_expand
/ccomp
/ccomp.byte
/ccomp.prof
......@@ -31,10 +32,12 @@
/Makefile.config
/.merlin
/_CoqProject
/compile.pl
# Generated files
/.depend
/.depend.extr
/compcert.ini
/compcert.config
/x86/ConstpropOp.v
/x86/SelectOp.v
/x86/SelectLong.v
......
......@@ -3,7 +3,7 @@ stages:
check-admitted:
stage: build
image: coqorg/coq:8.11.2-ocaml-4.11.1-flambda
image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda
before_script:
- eval `opam config env`
- opam update
......@@ -22,7 +22,7 @@ check-admitted:
build_x86_64:
stage: build
image: coqorg/coq:8.12-ocaml-4.11-flambda
image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda
before_script:
- eval `opam config env`
- opam update
......@@ -43,7 +43,7 @@ build_x86_64:
build_ia32:
stage: build
image: coqorg/coq:8.11.2-ocaml-4.11.1-flambda
image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda
before_script:
- sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
- sudo apt-get -y install gcc-multilib
......@@ -66,7 +66,7 @@ build_ia32:
build_aarch64:
stage: build
image: coqorg/coq:8.11.2-ocaml-4.11.1-flambda
image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda
before_script:
- sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
- sudo apt-get -y install gcc-aarch64-linux-gnu qemu-user
......@@ -89,7 +89,7 @@ build_aarch64:
build_arm:
stage: build
image: coqorg/coq:8.11.2-ocaml-4.11.1-flambda
image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda
before_script:
- sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
- sudo apt-get -y install gcc-arm-linux-gnueabi qemu-user
......@@ -113,7 +113,7 @@ build_arm:
build_armhf:
stage: build
image: coqorg/coq:8.11.2-ocaml-4.11.1-flambda
image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda
before_script:
- sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
- sudo apt-get -y install gcc-arm-linux-gnueabihf qemu-user
......@@ -136,7 +136,7 @@ build_armhf:
build_ppc:
stage: build
image: coqorg/coq:8.11.2-ocaml-4.11.1-flambda
image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda
before_script:
- sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
- sudo apt-get -y install gcc-powerpc-linux-gnu qemu-user
......@@ -157,7 +157,7 @@ build_ppc:
build_ppc64:
stage: build
image: coqorg/coq:8.11.2-ocaml-4.11.1-flambda
image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda
before_script:
- sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
- sudo apt-get -y install gcc-powerpc64-linux-gnu
......@@ -178,7 +178,7 @@ build_ppc64:
build_rv64:
stage: build
image: coqorg/coq:8.11.2-ocaml-4.11.1-flambda
image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda
before_script:
- sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
- sudo apt-get -y install gcc-riscv64-linux-gnu qemu-user
......@@ -201,7 +201,7 @@ build_rv64:
build_rv32:
stage: build
image: coqorg/coq:8.11.2-ocaml-4.11.1-flambda
image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda
before_script:
- sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
- sudo apt-get -y install gcc-riscv64-linux-gnu qemu-user
......@@ -222,7 +222,7 @@ build_rv32:
build_kvx:
stage: build
image: coqorg/coq:8.11.2-ocaml-4.11.1-flambda
image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda
before_script:
- sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
- sudo apt-get -y install sshpass openssh-client libzip4 lttng-tools liblttng-ctl-dev liblttng-ust-dev babeltrace
......@@ -249,12 +249,12 @@ build_kvx:
pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "build_kvx" above ?)
stage: build
image: coqorg/coq:8.11.2-ocaml-4.11.1-flambda
image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda
before_script:
- sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
- sudo apt-get -y install sshpass openssh-client libzip4 lttng-tools liblttng-ctl-dev liblttng-ust-dev babeltrace
- ./.download_from_Kalray.sh
- rm -f download/*dkms*.deb download/*eclipse*.deb download/*llvm*.deb download/*board-mgmt* download/*oce-host* download/*pocl*
- rm -f download/*dkms*.deb download/*eclipse*.deb download/*llvm*.deb download/*board-mgmt* download/*oce-host* download/*pocl* download/*flash-util* download/*barebox*
- sudo dpkg -i download/*.deb
- rm -rf download
- eval `opam config env`
......
Release 3.8, 2020-11-16
=======================
New features:
- Support `_Static_assert` from ISO C11.
- Support `__builtin_constant_p` from GCC and Clang.
- New port: x86 64 bits Windows with the Cygwin 64 environment.
(configure with target `x86_64-cygwin`).
- The following built-in functions are now available for all ports:
`__builtin_sqrt`, `__builtin_fabsf`, and all variants of
`__builtin_clz` and `__builtin_ctz`.
- Added `__builtin_fmin` and `__builtin_fmax` for AArch64.
Removed features:
- The x86 32 bits port is no longer supported under macOS.
Compiler internals:
- Simpler translation of CompCert C casts used for their effects but
not for their values.
- Known builtins whose results are unused are eliminated earlier.
- Improved error reporting for `++` and `--` applied to pointers to
incomplete types.
- Improved error reporting for redefinitions and implicit definitions
of built-in functions.
- Added formal semantics for some PowerPC built-ins.
The clightgen tool:
- New `-canonical-idents` mode, selected by default, to change the way
C identifiers are encoded as CompCert idents (positive numbers).
In `-canonical-idents` mode, a fixed one-to-one encoding is used
so that the same identifier occurring in different compilation units
encodes to the same number.
- The `-short-idents` flag restores the previous encoding where
C identifiers are consecutively numbered in order of appearance,
causing the same identifier to have different numbers in different
compilation units.
- Removed the automatic translation of annotation builtins to Coq
logical assertions, which was never used and possibly confusing.
Coq and OCaml development:
- Compatibility with Coq 8.12.1, 8.12.0, 8.11.2, 8.11.1.
- Can use already-installed Flocq and MenhirLib libraries instead of their
local copies (options `-use-external-Flocq` and `-use-external-MenhirLib`
to the `configure` script).
- Automatically build to OCaml bytecode on platforms where OCaml
native-code compilation is not available.
- Install the `compcert.config` summary of configuration choices
in the same directory as the Coq development.
- Updated the list of dual-licensed source files.
Release 3.7, 2020-03-31
=======================
......
......@@ -46,8 +46,8 @@ option) any later version:
all files in the exportclight/ directory
the Archi.v, CBuiltins.ml, and extractionMachdep.v files
in directories arm, powerpc, riscV, x86, x86_32, x86_64
the Archi.v, Builtins1.v, CBuiltins.ml, and extractionMachdep.v files
in directories aarch64, arm, powerpc, riscV, x86, x86_32, x86_64
extraction/extraction.v
......
......@@ -14,6 +14,12 @@
#######################################################################
include Makefile.config
include VERSION
BUILDVERSION ?= $(version)
BUILDNR ?= $(buildnr)
TAG ?= $(tag)
BRANCH ?= $(branch)
ifeq ($(wildcard $(ARCH)_$(BITSIZE)),)
ARCHDIRS?=$(ARCH)
......@@ -23,16 +29,27 @@ endif
BACKENDLIB?=Asmgenproof0.v Asmgenproof1.v
DIRS=lib lib/Impure common $(ARCHDIRS) scheduling backend cfrontend driver \
flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 \
exportclight MenhirLib cparser
DIRS := lib lib/Impure common $(ARCHDIRS) scheduling backend cfrontend driver \
exportclight cparser
RECDIRS:=lib common $(ARCHDIRS) scheduling backend cfrontend driver flocq exportclight \
cparser
RECDIRS=lib common $(ARCHDIRS) scheduling backend cfrontend driver flocq exportclight \
MenhirLib cparser
COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(subst /,.,$d))
COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) $(subst /,.,compcert.$(d)))
ifeq ($(LIBRARY_FLOCQ),local)
DIRS += flocq/Core flocq/Prop flocq/Calc flocq/IEEE754
RECDIRS += flocq
COQINCLUDES += -R flocq Flocq
endif
COQCOPTS ?= -w -undeclared-scope
ifeq ($(LIBRARY_MENHIRLIB),local)
DIRS += MenhirLib
RECDIRS += MenhirLib
COQINCLUDES += -R MenhirLib MenhirLib
endif
COQCOPTS ?= -w -undeclared-scope -w -omega-is-deprecated
COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
COQDOC="$(COQBIN)coqdoc"
......@@ -46,6 +63,7 @@ GPATH=$(DIRS)
# Flocq
ifeq ($(LIBRARY_FLOCQ),local)
FLOCQ=\
Raux.v Zaux.v Defs.v Digits.v Float_prop.v FIX.v FLT.v FLX.v FTZ.v \
Generic_fmt.v Round_pred.v Round_NE.v Ulp.v Core.v \
......@@ -53,6 +71,9 @@ FLOCQ=\
Div_sqrt_error.v Mult_error.v Plus_error.v \
Relative.v Sterbenz.v Round_odd.v Double_rounding.v \
Binary.v Bits.v
else
FLOCQ=
endif
# General-purpose libraries (in lib/)
......@@ -136,9 +157,13 @@ PARSER=Cabs.v Parser.v
# MenhirLib
ifeq ($(LIBRARY_MENHIRLIB),local)
MENHIRLIB=Alphabet.v Automaton.v Grammar.v Interpreter_complete.v \
Interpreter_correct.v Interpreter.v Main.v Validator_complete.v \
Validator_safe.v Validator_classes.v
else
MENHIRLIB=
endif
# Putting everything together (in driver/)
......@@ -168,6 +193,9 @@ endif
ifeq ($(CLIGHTGEN),true)
$(MAKE) clightgen
endif
ifeq ($(INSTALL_COQDEV),true)
$(MAKE) compcert.config
endif
proof: $(FILES:.v=.vo)
......@@ -212,11 +240,25 @@ documentation: $(FILES)
$(filter-out doc/coq2html cparser/Parser.v, $^)
tools/ndfun: tools/ndfun.ml
ifeq ($(OCAML_NATIVE_COMP),true)
ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml
tools/modorder: tools/modorder.ml
ocamlopt -o tools/modorder str.cmxa tools/modorder.ml
else
ocamlc -o tools/ndfun str.cma tools/ndfun.ml
endif
tools/compiler_expand: tools/compiler_expand.ml
ifeq ($(OCAML_NATIVE_COMP),true)
ocamlopt -o $@ $+
ocamlc -o $@ $+
else
endif
tools/modorder: tools/modorder.ml
ifeq ($(OCAML_NATIVE_COMP),true)
ocamlopt -o tools/modorder str.cmxa tools/modorder.ml
else
ocamlc -o tools/modorder str.cma tools/modorder.ml
endif
latexdoc:
cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES)
......@@ -254,14 +296,29 @@ compcert.ini: Makefile.config
echo "response_file_style=$(RESPONSEFILE)";) \
> compcert.ini
compcert.config: Makefile.config
(echo "# CompCert configuration parameters"; \
echo "COMPCERT_ARCH=$(ARCH)"; \
echo "COMPCERT_MODEL=$(MODEL)"; \
echo "COMPCERT_ABI=$(ABI)"; \
echo "COMPCERT_ENDIANNESS=$(ENDIANNESS)"; \
echo "COMPCERT_BITSIZE=$(BITSIZE)"; \
echo "COMPCERT_SYSTEM=$(SYSTEM)"; \
echo "COMPCERT_VERSION=$(BUILDVERSION)"; \
echo "COMPCERT_BUILDNR=$(BUILDNR)"; \
echo "COMPCERT_TAG=$(TAG)"; \
echo "COMPCERT_BRANCH=$(BRANCH)" \
) > compcert.config
driver/Version.ml: VERSION
cat VERSION \
| sed -e 's|\(.*\)=\(.*\)|let \1 = \"\2\"|g' \
>driver/Version.ml
(echo 'let version = "$(BUILDVERSION)"'; \
echo 'let buildnr = "$(BUILDNR)"'; \
echo 'let tag = "$(TAG)"'; \
echo 'let branch = "$(BRANCH)"') > driver/Version.ml
cparser/Parser.v: cparser/Parser.vy
@rm -f $@
$(MENHIR) --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check cparser/Parser.vy
$(MENHIR) --coq --coq-no-version-check cparser/Parser.vy
@chmod a-w $@
depend: $(GENERATED) depend1
......@@ -288,6 +345,7 @@ ifeq ($(INSTALL_COQDEV),true)
install -m 0644 $$d/*.vo $(DESTDIR)$(COQDEVDIR)/$$d/; \
done
install -m 0644 ./VERSION $(DESTDIR)$(COQDEVDIR)
install -m 0644 ./compcert.config $(DESTDIR)$(COQDEVDIR)
@(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(DESTDIR)$(COQDEVDIR)/README
endif
......@@ -297,7 +355,7 @@ clean:
rm -f $(patsubst %, %/.*.aux, $(DIRS))
rm -rf doc/html doc/*.glob
rm -f driver/Version.ml
rm -f compcert.ini
rm -f compcert.ini compcert.config
rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr
rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o
rm -f $(GENERATED) .depend
......@@ -319,6 +377,9 @@ check-proof: $(FILES)
print-includes:
@echo $(COQINCLUDES)
CoqProject:
@echo $(COQINCLUDES) > _CoqProject
-include .depend
FORCE:
......@@ -19,7 +19,8 @@ include Makefile.config
#
# Variables from Makefile.config:
# -OCAML_OPT_COMP: can we use the native version
# -OCAML_NATIVE_COMP: native-code compilation is supported
# -OCAML_OPT_COMP: can we use the natively-compiled compilers
# -COMPFLAGS: compile options
# -LINK_OPT: additional linker flags for the native binary
#
......@@ -49,13 +50,22 @@ INCLUDES=$(patsubst %,-I %, $(DIRS))
# Control of warnings:
WARNINGS=-w +a-4-9-27-42 -strict-sequence -safe-string -warn-error +a #Deprication returns with ocaml 4.03
# WARNINGS=-w +a-4-9-27-42 -strict-sequence -safe-string -warn-error +a #Deprication returns with ocaml 4.03
WARNINGS=-w +a-4-9-27-42
extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45-60-67
extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45-60-67
cparser/pre_parser.cmx: WARNINGS += -w -41
cparser/pre_parser.cmo: WARNINGS += -w -41
COMPFLAGS+=-g $(INCLUDES) -I "$(MENHIR_DIR)" $(WARNINGS)
# Turn warnings into errors, but not for released tarballs
ifeq ($(wildcard .git),.git)
WARN_ERRORS=-warn-error +a
else
WARN_ERRORS=
endif
COMPFLAGS+=-g -strict-sequence -safe-string $(INCLUDES) -I "$(MENHIR_DIR)" $(WARNINGS) $(WARN_ERRORS)
# Using .opt compilers if available
......@@ -71,6 +81,7 @@ OCAMLDEP=ocamldep$(DOTOPT) -slash $(INCLUDES)
OCAMLLEX=ocamllex -q
MODORDER=tools/modorder .depend.extr
COPY=cp
PARSERS=cparser/pre_parser.mly
LEXERS=cparser/Lexer.mll lib/Tokenize.mll \
......@@ -88,9 +99,15 @@ ifeq ($(wildcard .depend.extr),.depend.extr)
CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx)
ifeq ($(OCAML_NATIVE_COMP),true)
ccomp: $(CCOMP_OBJS)
@echo "Linking $@"
@$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+
else
ccomp: ccomp.byte
@echo "Copying to $@"
@$(COPY) $+ $@
endif
# DM force compilation without checking dependencies
ccomp.force:
......@@ -102,9 +119,15 @@ ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo)
CLIGHTGEN_OBJS:=$(shell $(MODORDER) exportclight/Clightgen.cmx)
ifeq ($(OCAML_NATIVE_COMP),true)
clightgen: $(CLIGHTGEN_OBJS)
@echo "Linking $@"
@$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+
else
clightgen: clightgen.byte
@echo "Copying to $@"
@$(COPY) $+ $@
endif
clightgen.byte: $(CLIGHTGEN_OBJS:.cmx=.cmo)
@echo "Linking $@"
......
......@@ -11,7 +11,8 @@
(* *)
(****************************************************************************)
From Coq Require Import Omega List Syntax Relations RelationClasses.
From Coq Require Import Omega List Relations RelationClasses.
Import ListNotations.
Local Obligation Tactic := intros.
......
......@@ -11,7 +11,8 @@
(* *)
(****************************************************************************)
From Coq Require Import List Syntax Orders.
From Coq Require Import List Orders.
Import ListNotations.
Require Import Alphabet.
(** The terminal non-terminal alphabets of the grammar. **)
......
......@@ -12,6 +12,7 @@
(****************************************************************************)
From Coq Require Import List Syntax.
Import ListNotations.
From Coq.ssr Require Import ssreflect.
Require Automaton.
Require Import Alphabet Grammar Validator_safe.
......
......@@ -11,7 +11,8 @@
(* *)
(****************************************************************************)
From Coq Require Import List Syntax Arith.
From Coq Require Import List Arith.
Import ListNotations.
From Coq.ssr Require Import ssreflect.
Require Import Alphabet Grammar.
Require Automaton Interpreter Validator_complete.
......
......@@ -11,7 +11,8 @@
(* *)
(****************************************************************************)
From Coq Require Import List Syntax.
From Coq Require Import List.
Import ListNotations.
Require Import Alphabet.
Require Grammar Automaton Interpreter.
From Coq.ssr Require Import ssreflect.
......
......@@ -13,6 +13,7 @@
From Coq Require Import List Syntax Derive.
From Coq.ssr Require Import ssreflect.
Import ListNotations.
Require Automaton.
Require Import Alphabet Validator_classes.
......
......@@ -12,6 +12,7 @@
(****************************************************************************)
From Coq Require Import List Syntax Derive.
Import ListNotations.
From Coq.ssr Require Import ssreflect.
Require Automaton.
Require Import Alphabet Validator_classes.
......
# CompCert
The verified C compiler.
The formally-verified C compiler.
## Overview
The CompCert C verified compiler is a compiler for a large subset of the
......@@ -13,8 +13,8 @@ source C code.
For more information on CompCert (supported platforms, supported C
features, installation instructions, using the compiler, etc), please
refer to the [Web site](http://compcert.inria.fr/) and especially
the [user's manual](http://compcert.inria.fr/man/).
refer to the [Web site](https://compcert.org/) and especially
the [user's manual](https://compcert.org/man/).
## Verimag-Kalray version
This is a special version with additions from Verimag and Kalray :
......@@ -40,7 +40,7 @@ The people responsible for this version are
CompCert is not free software. This non-commercial release can only
be used for evaluation, research, educational and personal purposes.
A commercial version of CompCert, without this restriction and with
professional support, can be purchased from
professional support and extra features, can be purchased from
[AbsInt](https://www.absint.com). See the file `LICENSE` for more
information.
......
version=3.7
version=3.8
buildnr=
tag=
branch=
......@@ -6,15 +6,17 @@
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(** Architecture-dependent parameters for AArch64 *)
From Flocq Require Import Binary Bits.
Require Import ZArith List.
(*From Flocq*)
Require Import Binary Bits.
Definition ptr64 := true.
......
......@@ -255,6 +255,7 @@ Inductive instruction: Type :=
| Pclz (sz: isize) (rd r1: ireg) (**r count leading zero bits *)
| Prev (sz: isize) (rd r1: ireg) (**r reverse bytes *)
| Prev16 (sz: isize) (rd r1: ireg) (**r reverse bytes in each 16-bit word *)
| Prbit (sz: isize) (rd r1: ireg) (**r reverse bits *)
(** Conditional data processing *)
| Pcsel (rd: ireg) (r1 r2: ireg) (c: testcond) (**r int conditional move *)
| Pcset (rd: ireg) (c: testcond) (**r set to 1/0 if cond is true/false *)
......@@ -300,6 +301,8 @@ Inductive instruction: Type :=
| Pfmsub (sz: fsize) (rd r1 r2 r3: freg) (**r [rd = r3 - r1 * r2] *)
| Pfnmadd (sz: fsize) (rd r1 r2 r3: freg) (**r [rd = - r3 - r1 * r2] *)
| Pfnmsub (sz: fsize) (rd r1 r2 r3: freg) (**r [rd = - r3 + r1 * r2] *)
| Pfmax (sz: fsize) (rd r1 r2: freg) (**r maximum *)
| Pfmin (sz: fsize) (rd r1 r2: freg) (**r minimum *)
(** Floating-point comparison *)
| Pfcmp (sz: fsize) (r1 r2: freg) (**r compare [r1] and [r2] *)
| Pfcmp0 (sz: fsize) (r1: freg) (**r compare [r1] and [+0.0] *)
......@@ -1304,7 +1307,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| Vint n =>
match list_nth_z tbl (Int.unsigned n) with
| None => Stuck
| Some lbl => goto_label f lbl (rs#X16 <- Vundef #X17 <- Vundef) m
| Some lbl => goto_label f lbl (rs#X16 <- Vundef) m
end
| _ => Stuck
end
......@@ -1324,11 +1327,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| Pclz _ _ _
| Prev _ _ _
| Prev16 _ _ _
| Prbit _ _ _
| Pfsqrt _ _ _
| Pfmadd _ _ _ _ _
| Pfmsub _ _ _ _ _
| Pfnmadd _ _ _ _ _
| Pfnmsub _ _ _ _ _
| Pfmax _ _ _ _
| Pfmin _ _ _ _
| Pcfi_adjust _
| Pcfi_rel_offset _ =>
Stuck
......@@ -1351,7 +1357,7 @@ Inductive step: state -> trace -> state -> Prop :=
external_call ef ge vargs m t vres m' ->
rs' = nextinstr
(set_res res vres
(undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
(undef_regs (DR X16 :: DR X30 :: map preg_of (destroyed_by_builtin ef)) rs)) ->
step (State rs m) t (State rs' m')
| exec_step_external:
forall b ef args res rs m t rs' m',
......
......@@ -39,8 +39,10 @@ Require Import Events.
Require Import Lia.
Open Scope impure.
Import ListNotations.
Local Open Scope list_scope.
Open Scope impure.
(** auxiliary treatments of builtins *)
Definition is_builtin(ex: option control): bool :=
......
......@@ -337,7 +337,7 @@ let expand_builtin_inline name args res =
| "__builtin_bswap16", [BA(DR(IR(RR1 a1)))], BR(DR(IR(RR1 res))) ->
emit (Prev16(W, res, a1));
emit (Pandimm(W, res, RR0 res, Z.of_uint 0xFFFF))
(* Count leading zeros and leading sign bits *)
(* Count leading zeros, leading sign bits, trailing zeros *)
| "__builtin_clz", [BA(DR(IR(RR1 a1)))], BR(DR(IR(RR1 res))) ->
emit (Pclz(W, res, a1))
| ("__builtin_clzl" | "__builtin_clzll"), [BA(DR(IR(RR1 a1)))], BR(DR(IR(RR1 res))) ->