From 6137b6b5b788138dd02503cb1e88242a618a3677 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 14 Mar 2019 23:39:11 +0000 Subject: C: Wrap Jib identifiers Avoids duplication between l-expressions and expressions. Also means that special variables like current_exception and have_exception are treated normally by functions such as instr_reads and instr_writes etc. Furthermore we can now easily annotate Jib identifiers in ways that were not previously possible with plain sail ids. --- language/jib.ott | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) (limited to 'language') diff --git a/language/jib.ott b/language/jib.ott index e54e2ea5..5a0e3eba 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -47,15 +47,19 @@ open import Value2 grammar +name :: '' ::= + | id nat :: :: name + | have_exception nat :: :: have_exception + | current_exception nat :: :: current_exception + | return nat :: :: return + % Fragments are small pure snippets of (abstract) C code, mostly -% expressions, used by the aval and cval types. +% expressions, used by the aval (ANF) and cval (Jib) types. fragment :: 'F_' ::= - | id :: :: id - | '&' id :: :: ref + | name :: :: id + | '&' name :: :: ref | value :: :: lit - | have_exception :: :: have_exception - | current_exception :: :: current_exception | fragment op fragment' :: :: op | op fragment :: :: unary | string ( fragment0 , ... , fragmentn ) :: :: call @@ -129,13 +133,10 @@ cval :: 'CV_' ::= {{ lem fragment * ctyp }} clexp :: 'CL_' ::= - | id : ctyp :: :: id + | name : ctyp :: :: id | clexp . string :: :: field | * clexp :: :: addr | clexp . nat :: :: tuple - | current_exception : ctyp :: :: current_exception - | have_exception :: :: have_exception - | return : ctyp :: :: return | void :: :: void ctype_def :: 'CTD_' ::= @@ -152,14 +153,14 @@ instr :: 'I_' ::= {{ aux _ iannot }} % The following are the minimal set of instructions output by % Jib_compile.ml. - | ctyp id :: :: decl - | ctyp id = cval :: :: init + | ctyp name :: :: decl + | ctyp name = cval :: :: init | jump ( cval ) string :: :: jump | goto string :: :: goto | string : :: :: label | clexp = bool id ( cval0 , ... , cvaln ) :: :: funcall | clexp = cval :: :: copy - | clear ctyp id :: :: clear + | clear ctyp name :: :: clear | undefined ctyp :: :: undefined | match_failure :: :: match_failure | end :: :: end @@ -187,8 +188,8 @@ instr :: 'I_' ::= | return cval :: :: return % For optimising away allocations and copying. - | reset ctyp id :: :: reset - | ctyp id = cval :: :: reinit + | reset ctyp name :: :: reset + | ctyp name = cval :: :: reinit | alias clexp = cval :: :: alias cdef :: 'CDEF_' ::= -- cgit v1.2.3 From c7e5eae97e75036d700ba437a5c295c6fb3874a4 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 19 Mar 2019 17:06:48 +0000 Subject: C: Some simplification Remove unused experimental optimizations --- language/jib.ott | 1 - 1 file changed, 1 deletion(-) (limited to 'language') diff --git a/language/jib.ott b/language/jib.ott index 5a0e3eba..f0173660 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -190,7 +190,6 @@ instr :: 'I_' ::= % For optimising away allocations and copying. | reset ctyp name :: :: reset | ctyp name = cval :: :: reinit - | alias clexp = cval :: :: alias cdef :: 'CDEF_' ::= | register id : ctyp = { -- cgit v1.2.3 From bee510755ecd32c600a27b9741c18cce1bd2ea4d Mon Sep 17 00:00:00 2001 From: Alasdair Date: Mon, 18 Mar 2019 21:40:34 +0000 Subject: C: Add identifier to end instruction Allows us to track the last version of the return variable when the AST in in SSA form. --- language/jib.ott | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'language') diff --git a/language/jib.ott b/language/jib.ott index f0173660..4f8eeacc 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -163,7 +163,7 @@ instr :: 'I_' ::= | clear ctyp name :: :: clear | undefined ctyp :: :: undefined | match_failure :: :: match_failure - | end :: :: end + | end name :: :: end % All instructions containing nested instructions can be flattened % away. try and throw only exist for internal use within -- cgit v1.2.3 From 21a26461caf237783d93dacfad933fc6ef0fe0c0 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 5 Apr 2019 17:03:33 +0100 Subject: Fix: Don't remove uncalled polymorphic constructors if they are matched upon Previously the specialization would remove any polymorphic union constructor that was never created anywhere in the specification. While this wasn't usually problematic, it does leave an edge case where such a constructor could be matched upon in a pattern, and then the resulting match would fail to compile as it would be matching on a constructor kind that doesn't exists. This should fix that issue by chaging the V_ctor_kind value into an F_ctor_kind fragment. Previously a polymorphic constructor-kind would have been represented by its mangled name, e.g. V_ctor_kind "zSome_unit" would now be represented as V_ctor_kind ("Some", unifiers, ty) where ty is a monomorphic version of the original constructor's type such that ctyp_unify original_ty ty = unifiers and the mangled name we generate is zencode_string ("Some_" ^ string_of_list "_" string_of_ctyp unifiers) --- language/jib.ott | 1 + 1 file changed, 1 insertion(+) (limited to 'language') diff --git a/language/jib.ott b/language/jib.ott index 4f8eeacc..e26389ce 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -60,6 +60,7 @@ fragment :: 'F_' ::= | name :: :: id | '&' name :: :: ref | value :: :: lit + | kind id ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_kind | fragment op fragment' :: :: op | op fragment :: :: unary | string ( fragment0 , ... , fragmentn ) :: :: call -- cgit v1.2.3 From 76bf4a3853e547ae2e0327b20e4f4b89d16820b7 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Sat, 6 Apr 2019 00:07:11 +0100 Subject: Various bugfixes and improvements - Rename DeIid to Operator. It corresponds to operator in the syntax. The previous name is from when it was called deinfix in sail1. - Removed things that weren't actually common from pretty_print_common.ml, e.g. printing identifiers is backend specific. The doc_id function here was only used for a very specific use case in pretty_print_lem, so I simplified it and renamed it to doc_sia_id, as it is always used for a SIA.Id whatever that is. - There is some support for anonymous records in constructors, e.g. union Foo ('a : Type) = { MkFoo : { field1 : 'a, field2 : int } } somewhat similar to the enum syntax in Rust. I'm not sure when this was added, but there were a few odd things about it. It was desugared in the preprocessor, rather than initial_check, and the desugaring generated incorrect code for polymorphic anonymous records as above. I moved the code to initial_check, so the pre-processor now just deals with pre-processor things and not generating types, and I fixed the code to work with polymorphic types. This revealed some issues in the C backend w.r.t. polymorphic structs, which is the bulk of this commit. I also added some tests for this feature. - OCaml backend can now generate a valid string_of function for polymorphic structs, previously this would cause the ocaml to fail to compile. - Some cleanup in the Sail ott definition - Add support for E_var in interpreter previously this would just cause the interpreter to fail --- language/jib.ott | 21 +++++++++--------- language/sail.ott | 64 ++++++++++++++++--------------------------------------- 2 files changed, 29 insertions(+), 56 deletions(-) (limited to 'language') diff --git a/language/jib.ott b/language/jib.ott index e26389ce..5f800fcd 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -57,16 +57,17 @@ name :: '' ::= % expressions, used by the aval (ANF) and cval (Jib) types. fragment :: 'F_' ::= - | name :: :: id - | '&' name :: :: ref - | value :: :: lit - | kind id ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_kind - | fragment op fragment' :: :: op - | op fragment :: :: unary - | string ( fragment0 , ... , fragmentn ) :: :: call - | fragment . string :: :: field - | string :: :: raw - | poly fragment :: :: poly + | name :: :: id + | '&' name :: :: ref + | value :: :: lit + | fragment != kind id ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_kind + | unwrap id ( ctyp0 , ... , ctypn ) fragment :: :: ctor_unwrap + | fragment op fragment' :: :: op + | op fragment :: :: unary + | string ( fragment0 , ... , fragmentn ) :: :: call + | fragment . string :: :: field + | string :: :: raw + | poly fragment :: :: poly % Note that init / clear are sometimes refered to as create / kill diff --git a/language/sail.ott b/language/sail.ott index a47f3f9f..1a3148d0 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -119,44 +119,16 @@ l :: '' ::= {{ phantom }} {{ hol () }} annot :: '' ::= - {{ phantom }} - {{ ocaml 'a annot }} - {{ lem annot 'a }} - {{ hol unit }} + {{ phantom }} + {{ ocaml 'a annot }} + {{ lem annot 'a }} + {{ hol unit }} id :: '' ::= {{ com Identifier }} {{ aux _ l }} - | x :: :: id - | ( deinfix x ) :: D :: deIid {{ com remove infix status }} - | bool :: M :: bool {{ com built in type identifiers }} {{ ichlo (Id "bool") }} - | bit :: M :: bit {{ ichlo (Id "bit") }} - | unit :: M :: unit {{ ichlo (Id "unit") }} - | nat :: M :: nat {{ ichlo (Id "nat") }} - | int :: M :: int {{ ichlo (Id "int") }} - | string :: M :: string {{ tex \ottkw{string} }} {{ ichlo (Id "string") }} - | range :: M :: range {{ ichlo (Id "range") }} - | atom :: M :: atom {{ ichlo (Id "atom") }} - | vector :: M :: vector {{ ichlo (Id "vector") }} - | list :: M :: list {{ ichlo (Id "list") }} -% | set :: M :: set {{ ichlo (Id "set") }} - | reg :: M :: reg {{ ichlo (Id "reg") }} - | to_num :: M :: tonum {{ com built-in function identifiers }} {{ ichlo (Id "to_num") }} - | to_vec :: M :: tovec {{ ichlo (Id "to_vec") }} - | msb :: M :: msb {{ ichlo (Id "msb") }} -% Note: we have just a single namespace. We don't want the same -% identifier to be reused as a type name or variable, expression -% variable, and field name. We don't enforce any lexical convention -% on type variables (or variables of other kinds) -% We don't enforce a lexical convention on infix operators, as some of the -% targets use alphabetical infix operators. - -% Vector builtins - | vector_access :: M :: vector_access {{ ichlo (Id "vector_access") }} - | vector_update :: M :: vector_update {{ ichlo (Id "vector_update") }} - | vector_update_subrange :: M :: vector_update_subrange {{ ichlo (Id "vector_update_subrange") }} - | vector_subrange :: M :: vector_subrange {{ ichlo (Id "vector_subrange") }} - | vector_append :: M :: vector_append {{ ichlo (Id "vector_append") }} + | x :: :: id + | ( operator x ) :: D :: operator {{ com remove infix status }} kid :: '' ::= {{ com kinded IDs: Type, Int, and Order variables }} @@ -180,23 +152,23 @@ kind :: 'K_' ::= nexp :: 'Nexp_' ::= {{ com numeric expression, of kind Int }} {{ aux _ l }} - | id :: :: id {{ com abbreviation identifier }} - | kid :: :: var {{ com variable }} - | num :: :: constant {{ com constant }} - | id ( nexp1 , ... , nexpn ) :: :: app {{ com app }} - | nexp1 * nexp2 :: :: times {{ com product }} - | nexp1 + nexp2 :: :: sum {{ com sum }} - | nexp1 - nexp2 :: :: minus {{ com subtraction }} - | 2** nexp :: :: exp {{ com exponential }} - | neg nexp :: I :: neg {{ com for internal use only}} - | ( nexp ) :: S :: paren {{ ichlo [[nexp]] }} + | id :: :: id {{ com abbreviation identifier }} + | kid :: :: var {{ com variable }} + | num :: :: constant {{ com constant }} + | id ( nexp1 , ... , nexpn ) :: :: app {{ com app }} + | nexp1 * nexp2 :: :: times {{ com product }} + | nexp1 + nexp2 :: :: sum {{ com sum }} + | nexp1 - nexp2 :: :: minus {{ com subtraction }} + | 2 ^ nexp :: :: exp {{ com exponential }} + | - nexp :: :: neg {{ com unary negation}} + | ( nexp ) :: S :: paren {{ ichlo [[nexp]] }} order :: 'Ord_' ::= {{ com vector order specifications, of kind Order }} {{ aux _ l }} | kid :: :: var {{ com variable }} - | inc :: :: inc {{ com increasing }} - | dec :: :: dec {{ com decreasing }} + | inc :: :: inc {{ com increasing }} + | dec :: :: dec {{ com decreasing }} | ( order ) :: S :: paren {{ ichlo [[order]] }} base_effect :: 'BE_' ::= -- cgit v1.2.3