-
Notifications
You must be signed in to change notification settings - Fork 1.1k
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.
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
Cmm invariants #1400
Merged
Merged
Cmm invariants #1400
Changes from 9 commits
Commits
Show all changes
11 commits
Select commit
Hold shift + click to select a range
9b2c634
Add an optional check for invariants on the Cmm representation
lthls d504b58
Add Changes entry
lthls 71fb042
Fix .depend
lthls 1ae91bb
Add cmm-invariants to OCAMLPARAM
lthls 7bac5a9
Add --enable-cmm-invariants configure flag
lthls 94e7474
Enable Cmm invariants on some CI runs
lthls 430c60e
Test file (WIP)
lthls 34fd9d0
Update expected test
lthls 6ff3561
ocamltest: add the codegen_exit_status variable
shindere 49b3574
Changes
lthls ed17834
Add David Allsopp as reviewer
lthls File filter
Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,180 @@ | ||
(**************************************************************************) | ||
(* *) | ||
(* OCaml *) | ||
(* *) | ||
(* Vincent Laviron, OCamlPro *) | ||
(* *) | ||
(* Copyright 2017 OCamlPro SAS *) | ||
(* *) | ||
(* All rights reserved. This file is distributed under the terms of *) | ||
(* the GNU Lesser General Public License version 2.1, with the *) | ||
(* special exception on linking described in the file LICENSE. *) | ||
(* *) | ||
(**************************************************************************) | ||
|
||
[@@@ocaml.warning "-40"] | ||
|
||
module Int = Numbers.Int | ||
|
||
(* Check a number of continuation-related invariants *) | ||
|
||
module Env : sig | ||
type t | ||
|
||
val init : unit -> t | ||
|
||
val handler : t -> cont:int -> arg_num:int -> t | ||
|
||
val jump : t -> cont:int -> arg_num:int -> unit | ||
|
||
val report : Format.formatter -> bool | ||
end = struct | ||
type t = { | ||
bound_handlers : int Int.Map.t; | ||
} | ||
|
||
type error = | ||
| Unbound_handler of { cont: int } | ||
| Multiple_handlers of { cont: int; } | ||
| Wrong_arguments_number of | ||
{ cont: int; handler_args: int; jump_args: int; } | ||
|
||
module Error = struct | ||
type t = error | ||
|
||
let compare = Stdlib.compare | ||
end | ||
|
||
module ErrorSet = Set.Make(Error) | ||
|
||
type persistent_state = { | ||
mutable all_handlers : Int.Set.t; | ||
mutable errors : ErrorSet.t; | ||
} | ||
|
||
let state = { | ||
all_handlers = Int.Set.empty; | ||
errors = ErrorSet.empty; | ||
} | ||
|
||
let record_error error = | ||
state.errors <- ErrorSet.add error state.errors | ||
|
||
let unbound_handler cont = | ||
record_error (Unbound_handler { cont; }) | ||
|
||
let multiple_handler cont = | ||
record_error (Multiple_handlers { cont; }) | ||
|
||
let wrong_arguments cont handler_args jump_args = | ||
record_error (Wrong_arguments_number { cont; handler_args; jump_args; }) | ||
|
||
let init () = | ||
state.all_handlers <- Int.Set.empty; | ||
state.errors <- ErrorSet.empty; | ||
{ | ||
bound_handlers = Int.Map.empty; | ||
} | ||
|
||
let handler t ~cont ~arg_num = | ||
if Int.Set.mem cont state.all_handlers then multiple_handler cont; | ||
state.all_handlers <- Int.Set.add cont state.all_handlers; | ||
let bound_handlers = Int.Map.add cont arg_num t.bound_handlers in | ||
{ bound_handlers; } | ||
|
||
let jump t ~cont ~arg_num = | ||
match Int.Map.find cont t.bound_handlers with | ||
| handler_args -> | ||
if arg_num <> handler_args then | ||
wrong_arguments cont handler_args arg_num | ||
| exception Not_found -> unbound_handler cont | ||
|
||
let print_error ppf error = | ||
match error with | ||
| Unbound_handler { cont } -> | ||
if Int.Set.mem cont state.all_handlers then | ||
Format.fprintf ppf | ||
"Continuation %d was used outside the scope of its handler" | ||
cont | ||
else | ||
Format.fprintf ppf | ||
"Continuation %d was used but never bound" | ||
cont | ||
| Multiple_handlers { cont; } -> | ||
Format.fprintf ppf | ||
"Continuation %d was declared in more than one handler" | ||
cont | ||
| Wrong_arguments_number { cont; handler_args; jump_args } -> | ||
Format.fprintf ppf | ||
"Continuation %d was declared with %d arguments but called with %d" | ||
cont | ||
handler_args | ||
jump_args | ||
|
||
let print_error_newline ppf error = | ||
Format.fprintf ppf "%a@." print_error error | ||
|
||
let report ppf = | ||
if ErrorSet.is_empty state.errors then false | ||
else begin | ||
ErrorSet.iter (fun err -> print_error_newline ppf err) state.errors; | ||
true | ||
end | ||
end | ||
|
||
let rec check env (expr : Cmm.expression) = | ||
match expr with | ||
| Cconst_int _ | Cconst_natint _ | Cconst_float _ | Cconst_symbol _ | ||
| Cvar _ -> | ||
() | ||
| Clet (_, expr, body) | ||
| Clet_mut (_, _, expr, body) -> | ||
check env expr; | ||
check env body | ||
| Cphantom_let (_, _, expr) -> | ||
check env expr | ||
| Cassign (_, expr) -> | ||
check env expr | ||
| Ctuple exprs -> | ||
List.iter (check env) exprs | ||
| Cop (_, args, _) -> | ||
List.iter (check env) args; | ||
| Csequence (expr1, expr2) -> | ||
check env expr1; | ||
check env expr2 | ||
| Cifthenelse (test, _, ifso, _, ifnot, _) -> | ||
check env test; | ||
check env ifso; | ||
check env ifnot | ||
| Cswitch (body, _, branches, _) -> | ||
check env body; | ||
Array.iter (fun (expr, _) -> check env expr) branches | ||
| Ccatch (rec_flag, handlers, body) -> | ||
let env_extended = | ||
List.fold_left | ||
(fun env (cont, args, _, _) -> | ||
Env.handler env ~cont ~arg_num:(List.length args)) | ||
env | ||
handlers | ||
in | ||
check env_extended body; | ||
let env_handler = | ||
match rec_flag with | ||
| Recursive -> env_extended | ||
| Nonrecursive -> env | ||
in | ||
List.iter (fun (_, _, handler, _) -> check env_handler handler) handlers | ||
| Cexit (cont, args) -> | ||
Env.jump env ~cont ~arg_num:(List.length args) | ||
| Ctrywith (body, _, handler, _) -> | ||
(* Jumping from inside a trywith body to outside isn't very nice, | ||
but it's handled correctly by Linearize, as it happens | ||
when compiling match ... with exception ..., for instance, so it is | ||
not reported as an error. *) | ||
check env body; | ||
check env handler | ||
|
||
let run ppf (fundecl : Cmm.fundecl) = | ||
let env = Env.init () in | ||
check env fundecl.fun_body; | ||
Env.report ppf |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,36 @@ | ||
(**************************************************************************) | ||
(* *) | ||
(* OCaml *) | ||
(* *) | ||
(* Vincent Laviron, OCamlPro *) | ||
(* *) | ||
(* Copyright 2017 OCamlPro SAS *) | ||
(* *) | ||
(* All rights reserved. This file is distributed under the terms of *) | ||
(* the GNU Lesser General Public License version 2.1, with the *) | ||
(* special exception on linking described in the file LICENSE. *) | ||
(* *) | ||
(**************************************************************************) | ||
|
||
(* Check a number of continuation-related invariants *) | ||
|
||
(* Currently, this checks that : | ||
- Every use of a continuation occurs within the scope of its handler | ||
- Exit instructions take the same number of arguments as their handler. | ||
- In every function declaration, a given continuation can only be | ||
declared in a single handler. | ||
|
||
This is intended to document what invariants the backend can rely upon. | ||
The first two would trigger errors later, and the last one, while | ||
harmless for now, is not that hard to ensure, could be useful for | ||
future work on the backend, and helped detect a code duplication bug. | ||
|
||
These invariants are not checked by default, but the check can be turned | ||
on with the -dcmm-invariants compilation flag. | ||
*) | ||
|
||
(** [run ppf fundecl] analyses the given function, and returns whether | ||
any errors were encountered (with corresponding error messages printed | ||
on the given formatter). *) | ||
|
||
val run : Format.formatter -> Cmm.fundecl -> bool |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
this shoud probably have more people as reviewers (I guess at least Stephen, probably David and Sébastien as well).