diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-10 18:28:26 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-10 18:28:26 +0200 |
commit | f16fa31ec9cc90da750c8cc10f447023962cd153 (patch) | |
tree | 28eed4d4b5bc964907f20332d1eed470a393d07b /exportclight | |
parent | 485a4c0dd450e65745c83e59acdb40b42058e556 (diff) | |
parent | d703ae1ad5e1fcdc63e07b2a50a3e8576a11e61e (diff) | |
download | compcert-kvx-f16fa31ec9cc90da750c8cc10f447023962cd153.tar.gz compcert-kvx-f16fa31ec9cc90da750c8cc10f447023962cd153.zip |
Merge branch 'kvx-work' into BTL
Diffstat (limited to 'exportclight')
-rw-r--r-- | exportclight/Clightdefs.v | 43 | ||||
-rw-r--r-- | exportclight/Clightgen.ml | 9 | ||||
-rw-r--r-- | exportclight/Clightnorm.ml | 9 | ||||
-rw-r--r-- | exportclight/ExportClight.ml | 17 |
4 files changed, 48 insertions, 30 deletions
diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v index 8af920df..708be1cb 100644 --- a/exportclight/Clightdefs.v +++ b/exportclight/Clightdefs.v @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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. *) (* *) (* *********************************************************************) @@ -18,6 +19,8 @@ From Coq Require Import Ascii String List ZArith. From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop Clight. +(** ** Short names for types *) + Definition tvoid := Tvoid. Definition tschar := Tint I8 Signed noattr. Definition tuchar := Tint I8 Unsigned noattr. @@ -56,6 +59,8 @@ Definition talignas (n: N) (ty: type) := Definition tvolatile_alignas (n: N) (ty: type) := tattr {| attr_volatile := true; attr_alignas := Some n |} ty. +(** ** Constructor for programs and compilation units *) + Definition wf_composites (types: list composite_definition) : Prop := match build_composite_env types with OK _ => True | Error _ => False end. @@ -81,6 +86,8 @@ Definition mkprogram (types: list composite_definition) prog_comp_env := ce; prog_comp_env_eq := EQ |}. +(** ** Encoding character strings as positive numbers *) + (** The following encoding of character strings as positive numbers must be kept consistent with the OCaml function [Camlcoq.pos_of_string]. *) @@ -169,17 +176,6 @@ Fixpoint ident_of_string (s: string) : ident := | String c s => append_char_pos c (ident_of_string s) end. -(** A convenient notation [$ "ident"] to force evaluation of - [ident_of_string "ident"] *) - -Ltac ident_of_string s := - let x := constr:(ident_of_string s) in - let y := eval compute in x in - exact y. - -Notation "$ s" := (ltac:(ident_of_string s)) - (at level 1, only parsing) : string_scope. - (** The inverse conversion, from encoded strings to strings *) Section DECODE_BITS. @@ -289,3 +285,20 @@ Proof. intros. rewrite <- (string_of_ident_of_string s1), <- (string_of_ident_of_string s2). congruence. Qed. + +(** ** Notations *) + +Module ClightNotations. + +(** A convenient notation [$ "ident"] to force evaluation of + [ident_of_string "ident"] *) + +Ltac ident_of_string s := + let x := constr:(ident_of_string s) in + let y := eval compute in x in + exact y. + +Notation "$ s" := (ltac:(ident_of_string s)) + (at level 1, only parsing) : clight_scope. + +End ClightNotations. diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index 5e27370e..44c76cc6 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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. *) (* *) (* *********************************************************************) diff --git a/exportclight/Clightnorm.ml b/exportclight/Clightnorm.ml index a6158b60..88d44c08 100644 --- a/exportclight/Clightnorm.ml +++ b/exportclight/Clightnorm.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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. *) (* *) (* *********************************************************************) diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 4ff901eb..474a1bd8 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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. *) (* *) (* *********************************************************************) @@ -216,8 +217,8 @@ and typlist p = function and callconv p cc = if cc = cc_default then fprintf p "cc_default" - else fprintf p "{|cc_vararg:=%b; cc_unproto:=%b; cc_structret:=%b|}" - cc.cc_vararg cc.cc_unproto cc.cc_structret + else fprintf p "{|cc_vararg:=%a; cc_unproto:=%b; cc_structret:=%b|}" + (print_option coqZ) cc.cc_vararg cc.cc_unproto cc.cc_structret (* External functions *) @@ -455,8 +456,10 @@ let print_composite_definition p (Composite(id, su, m, a)) = let prologue = "\ From Coq Require Import String List ZArith.\n\ From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.\n\ +Import Clightdefs.ClightNotations.\n\ Local Open Scope Z_scope.\n\ -Local Open Scope string_scope.\n" +Local Open Scope string_scope.\n\ +Local Open Scope clight_scope.\n" (* Naming the compiler-generated temporaries occurring in the program *) |