Skip to content

Adding a switch for normalising types at elaboration time #805

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

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Adding a switch for normalising types at elaboration time #805

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
2 changes: 1 addition & 1 deletion backend/cn/bin/main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ let frontend ~macros ~incl_dirs ~incl_files astprints ~filename ~magic_comment_c
~ignore_bitfields:false;
Ocaml_implementation.set Ocaml_implementation.HafniumImpl.impl;
Switches.set
([ "inner_arg_temps"; "at_magic_comments" ]
([ "inner_arg_temps"; "at_magic_comments"; "elaboration_normalises_types" ]
(* TODO (DCM, VIP) figure out how to support liveness checks for read-only
resources and then switch on "strict_pointer_arith" to elaborate array
shift to the effectful version. "strict_pointer_relationals" is also
Expand Down
2 changes: 2 additions & 0 deletions frontend/model/global.lem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,7 @@ type cerb_switch =
| SW_permissive_printf
| SW_no_integer_provenance
| SW_CHERI
| SW_elaboration_normalises_types

declare ocaml target_rep function SW_strict_reads = `Switches.SW_strict_reads`
declare ocaml target_rep function SW_forbid_nullptr_free = `Switches.SW_forbid_nullptr_free`
Expand All @@ -59,6 +60,7 @@ declare ocaml target_rep function SW_inner_arg_temps = `Switches.SW_inner_arg_te
declare ocaml target_rep function SW_permissive_printf = `Switches.SW_permissive_printf`
declare ocaml target_rep function SW_no_integer_provenance = `Switches.SW_no_integer_provenance`
declare ocaml target_rep function SW_CHERI = `Switches.SW_CHERI`
declare ocaml target_rep function SW_elaboration_normalises_types = `Switches.SW_elaboration_normalises_types`


val is_CHERI: unit -> bool
Expand Down
6 changes: 6 additions & 0 deletions frontend/model/translation.lem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1410,6 +1410,12 @@ let rec translate_expression is_used ctx variadic_env stdlib tagDefs a_expr =
(* STD §6.3.1.8#1, bullet 4 *)
match (AilTypesAux.promotion (Implementation.integerImpl ()) ty1, AilTypesAux.promotion (Implementation.integerImpl ()) ty2) with
| (Just (Ctype.Ctype _ (Ctype.Basic (Ctype.Integer ity1')) as ty1'), Just (Ctype.Ctype _ (Ctype.Basic (Ctype.Integer ity2')) as ty2')) ->
let (ity1', ity2') =
if Global.has_switch Global.SW_elaboration_normalises_types then
( Implementation.normalise_integerType ity1'
, Implementation.normalise_integerType ity2' )
else
(ity1', ity2') in
(* "If both operants have the same type, then no further conversion is needed." *)
if ty1' = ty2' then
(mk_conv_int ity1' e1, mk_conv_int ity2' e2)
Expand Down
12 changes: 10 additions & 2 deletions frontend/model/translation_aux.lem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -207,8 +207,16 @@ let ctype_of a_expr =
match ErrorMonad.runErrorMonad
(GenTypesAux.interpret_genTypeCategory (Loc.locOf a_expr) (Implementation.integerImpl ())
(GenTypes.genTypeCategoryOf a_expr)) with
| Right (GenTypes.LValueType _ ty _) -> ty
| Right (GenTypes.RValueType ty) -> ty
| Right (GenTypes.LValueType _ ty _) ->
if Global.has_switch Global.SW_elaboration_normalises_types then
Implementation.normalise_ctype ty
else
ty
| Right (GenTypes.RValueType ty) ->
if Global.has_switch Global.SW_elaboration_normalises_types then
Implementation.normalise_ctype ty
else
ty
| Left (loc, TypingError.TError_MiscError (TypingError.UntypableIntegerConstant n)) ->
error $ Loc.stringFromLocation loc ^ ": untypable integer constant '" ^ show n ^ "'\n"
| _ -> error "[Translation_aux.ctype_of] impossible case: TODO move to Exception.t"
Expand Down
8 changes: 7 additions & 1 deletion ocaml_frontend/switches.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,9 @@ type cerb_switch =
(* set magic comment syntax to "/*$ ... $*/" *)
| SW_magic_comment_char_dollar

(* type aliases (e.g. size_t) are normalised during the elaboration to Core.
As a result the generated Core has fixed their implementation. *)
| SW_elaboration_normalises_types

let internal_ref =
ref []
Expand Down Expand Up @@ -94,6 +97,8 @@ let set strs =
Some SW_at_magic_comments
| "magic_comment_char_dollar" ->
Some (SW_magic_comment_char_dollar)
| "elaboration_normalises_types" ->
Some SW_elaboration_normalises_types
| _ ->
None in
let pred x = function
Expand Down Expand Up @@ -122,7 +127,8 @@ let set strs =
| SW_permissive_printf
| SW_zero_initialised
| SW_at_magic_comments
| SW_magic_comment_char_dollar as y ->
| SW_magic_comment_char_dollar
| SW_elaboration_normalises_types as y ->
x = y in
List.iter (fun str ->
match read_switch str with
Expand Down
4 changes: 4 additions & 0 deletions ocaml_frontend/switches.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,10 @@ type cerb_switch =
(* set magic comment syntax to "/*$ ... $*/" *)
| SW_magic_comment_char_dollar

(* type aliases (e.g. size_t) are normalised during the elaboration to Core.
As a result the generated Core has fixed their implementation. *)
| SW_elaboration_normalises_types

val get_switches: unit -> cerb_switch list
val has_switch: cerb_switch -> bool
val has_switch_pred: (cerb_switch -> bool) -> cerb_switch option
Expand Down
Loading