Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 9b2c634

Browse files
lthlslthls
committedApr 19, 2021
Add an optional check for invariants on the Cmm representation
1 parent d12738a commit 9b2c634

9 files changed

+275
-10
lines changed
 

‎.depend

+36-10
Original file line numberDiff line numberDiff line change
@@ -2027,8 +2027,10 @@ bytecomp/printinstr.cmx : \
20272027
bytecomp/printinstr.cmi
20282028
bytecomp/printinstr.cmi : \
20292029
bytecomp/instruct.cmi
2030+
bytecomp/runtimedef.cmo :
2031+
bytecomp/runtimedef.cmx :
20302032
bytecomp/symtable.cmo : \
2031-
lambda/runtimedef.cmi \
2033+
bytecomp/runtimedef.cmo \
20322034
typing/predef.cmi \
20332035
utils/misc.cmi \
20342036
bytecomp/meta.cmi \
@@ -2043,7 +2045,7 @@ bytecomp/symtable.cmo : \
20432045
parsing/asttypes.cmi \
20442046
bytecomp/symtable.cmi
20452047
bytecomp/symtable.cmx : \
2046-
lambda/runtimedef.cmx \
2048+
bytecomp/runtimedef.cmx \
20472049
typing/predef.cmx \
20482050
utils/misc.cmx \
20492051
bytecomp/meta.cmx \
@@ -2141,6 +2143,7 @@ asmcomp/asmgen.cmo : \
21412143
asmcomp/comballoc.cmi \
21422144
asmcomp/coloring.cmi \
21432145
asmcomp/cmmgen.cmi \
2146+
asmcomp/cmm_invariants.cmi \
21442147
asmcomp/cmm_helpers.cmi \
21452148
asmcomp/cmm.cmi \
21462149
utils/clflags.cmi \
@@ -2183,6 +2186,7 @@ asmcomp/asmgen.cmx : \
21832186
asmcomp/comballoc.cmx \
21842187
asmcomp/coloring.cmx \
21852188
asmcomp/cmmgen.cmx \
2189+
asmcomp/cmm_invariants.cmx \
21862190
asmcomp/cmm_helpers.cmx \
21872191
asmcomp/cmm.cmx \
21882192
utils/clflags.cmx \
@@ -2225,7 +2229,7 @@ asmcomp/asmlibrarian.cmx : \
22252229
asmcomp/asmlibrarian.cmi
22262230
asmcomp/asmlibrarian.cmi :
22272231
asmcomp/asmlink.cmo : \
2228-
lambda/runtimedef.cmi \
2232+
bytecomp/runtimedef.cmo \
22292233
utils/profile.cmi \
22302234
utils/misc.cmi \
22312235
parsing/location.cmi \
@@ -2243,7 +2247,7 @@ asmcomp/asmlink.cmo : \
22432247
asmcomp/asmgen.cmi \
22442248
asmcomp/asmlink.cmi
22452249
asmcomp/asmlink.cmx : \
2246-
lambda/runtimedef.cmx \
2250+
bytecomp/runtimedef.cmx \
22472251
utils/profile.cmx \
22482252
utils/misc.cmx \
22492253
parsing/location.cmx \
@@ -2420,6 +2424,16 @@ asmcomp/cmm_helpers.cmi : \
24202424
middle_end/clambda_primitives.cmi \
24212425
middle_end/clambda.cmi \
24222426
parsing/asttypes.cmi
2427+
asmcomp/cmm_invariants.cmo : \
2428+
utils/numbers.cmi \
2429+
asmcomp/cmm.cmi \
2430+
asmcomp/cmm_invariants.cmi
2431+
asmcomp/cmm_invariants.cmx : \
2432+
utils/numbers.cmx \
2433+
asmcomp/cmm.cmx \
2434+
asmcomp/cmm_invariants.cmi
2435+
asmcomp/cmm_invariants.cmi : \
2436+
asmcomp/cmm.cmi
24232437
asmcomp/cmmgen.cmo : \
24242438
typing/types.cmi \
24252439
middle_end/printclambda_primitives.cmi \
@@ -5777,6 +5791,7 @@ asmcomp/debug/reg_with_debug_info.cmx : \
57775791
asmcomp/debug/reg_with_debug_info.cmi : \
57785792
asmcomp/reg.cmi \
57795793
middle_end/backend_var.cmi
5794+
driver/compdynlink.cmi :
57805795
driver/compenv.cmo : \
57815796
utils/warnings.cmi \
57825797
utils/profile.cmi \
@@ -6111,13 +6126,13 @@ driver/pparse.cmi : \
61116126
parsing/parsetree.cmi
61126127
toplevel/expunge.cmo : \
61136128
bytecomp/symtable.cmi \
6114-
lambda/runtimedef.cmi \
6129+
bytecomp/runtimedef.cmo \
61156130
utils/misc.cmi \
61166131
typing/ident.cmi \
61176132
bytecomp/bytesections.cmi
61186133
toplevel/expunge.cmx : \
61196134
bytecomp/symtable.cmx \
6120-
lambda/runtimedef.cmx \
6135+
bytecomp/runtimedef.cmx \
61216136
utils/misc.cmx \
61226137
typing/ident.cmx \
61236138
bytecomp/bytesections.cmx
@@ -6327,6 +6342,8 @@ toplevel/trace.cmi : \
63276342
typing/path.cmi \
63286343
parsing/longident.cmi \
63296344
typing/env.cmi
6345+
toplevel/byte/topdirs.cmi : \
6346+
parsing/longident.cmi
63306347
toplevel/byte/topeval.cmo : \
63316348
utils/warnings.cmi \
63326349
typing/types.cmi \
@@ -6400,11 +6417,20 @@ toplevel/byte/topeval.cmx : \
64006417
toplevel/byte/topeval.cmi : \
64016418
toplevel/topcommon.cmi \
64026419
parsing/parsetree.cmi
6420+
toplevel/byte/toploop.cmi : \
6421+
utils/warnings.cmi \
6422+
typing/types.cmi \
6423+
typing/path.cmi \
6424+
parsing/parsetree.cmi \
6425+
typing/outcometree.cmi \
6426+
parsing/longident.cmi \
6427+
parsing/location.cmi \
6428+
typing/env.cmi
64036429
toplevel/byte/topmain.cmo : \
64046430
toplevel/byte/trace.cmi \
6405-
toplevel/toploop.cmi \
6431+
toplevel/byte/toploop.cmi \
64066432
toplevel/byte/topeval.cmi \
6407-
toplevel/topdirs.cmi \
6433+
toplevel/byte/topdirs.cmi \
64086434
toplevel/topcommon.cmi \
64096435
typing/printtyp.cmi \
64106436
typing/path.cmi \
@@ -6419,9 +6445,9 @@ toplevel/byte/topmain.cmo : \
64196445
toplevel/byte/topmain.cmi
64206446
toplevel/byte/topmain.cmx : \
64216447
toplevel/byte/trace.cmx \
6422-
toplevel/toploop.cmx \
6448+
toplevel/byte/toploop.cmi \
64236449
toplevel/byte/topeval.cmx \
6424-
toplevel/topdirs.cmx \
6450+
toplevel/byte/topdirs.cmi \
64256451
toplevel/topcommon.cmx \
64266452
typing/printtyp.cmx \
64276453
typing/path.cmx \

‎asmcomp/asmgen.ml

+11
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,16 @@ type error =
3030

3131
exception Error of error
3232

33+
let cmm_invariants ppf fd_cmm =
34+
let print_fundecl =
35+
if !Clflags.dump_cmm then Printcmm.fundecl
36+
else fun ppf fdecl -> Format.fprintf ppf "%s" fdecl.fun_name
37+
in
38+
if !Clflags.cmm_invariants && Cmm_invariants.run ppf fd_cmm then
39+
Misc.fatal_errorf "Cmm invariants failed on following fundecl:@.%a@."
40+
print_fundecl fd_cmm;
41+
fd_cmm
42+
3343
let liveness phrase = Liveness.fundecl phrase; phrase
3444

3545
let dump_if ppf flag message phrase =
@@ -127,6 +137,7 @@ let compile_fundecl ~ppf_dump fd_cmm =
127137
Proc.init ();
128138
Reg.reset();
129139
fd_cmm
140+
++ Profile.record ~accumulate:true "cmm_invariants" (cmm_invariants ppf_dump)
130141
++ Profile.record ~accumulate:true "selection" Selection.fundecl
131142
++ pass_dump_if ppf_dump dump_selection "After instruction selection"
132143
++ Profile.record ~accumulate:true "comballoc" Comballoc.fundecl

‎asmcomp/cmm_invariants.ml

+180
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,180 @@
1+
(**************************************************************************)
2+
(* *)
3+
(* OCaml *)
4+
(* *)
5+
(* Vincent Laviron, OCamlPro *)
6+
(* *)
7+
(* Copyright 2017 OCamlPro SAS *)
8+
(* *)
9+
(* All rights reserved. This file is distributed under the terms of *)
10+
(* the GNU Lesser General Public License version 2.1, with the *)
11+
(* special exception on linking described in the file LICENSE. *)
12+
(* *)
13+
(**************************************************************************)
14+
15+
[@@@ocaml.warning "-40"]
16+
17+
module Int = Numbers.Int
18+
19+
(* Check a number of continuation-related invariants *)
20+
21+
module Env : sig
22+
type t
23+
24+
val init : unit -> t
25+
26+
val handler : t -> cont:int -> arg_num:int -> t
27+
28+
val jump : t -> cont:int -> arg_num:int -> unit
29+
30+
val report : Format.formatter -> bool
31+
end = struct
32+
type t = {
33+
bound_handlers : int Int.Map.t;
34+
}
35+
36+
type error =
37+
| Unbound_handler of { cont: int }
38+
| Multiple_handlers of { cont: int; }
39+
| Wrong_arguments_number of
40+
{ cont: int; handler_args: int; jump_args: int; }
41+
42+
module Error = struct
43+
type t = error
44+
45+
let compare = Stdlib.compare
46+
end
47+
48+
module ErrorSet = Set.Make(Error)
49+
50+
type persistent_state = {
51+
mutable all_handlers : Int.Set.t;
52+
mutable errors : ErrorSet.t;
53+
}
54+
55+
let state = {
56+
all_handlers = Int.Set.empty;
57+
errors = ErrorSet.empty;
58+
}
59+
60+
let record_error error =
61+
state.errors <- ErrorSet.add error state.errors
62+
63+
let unbound_handler cont =
64+
record_error (Unbound_handler { cont; })
65+
66+
let multiple_handler cont =
67+
record_error (Multiple_handlers { cont; })
68+
69+
let wrong_arguments cont handler_args jump_args =
70+
record_error (Wrong_arguments_number { cont; handler_args; jump_args; })
71+
72+
let init () =
73+
state.all_handlers <- Int.Set.empty;
74+
state.errors <- ErrorSet.empty;
75+
{
76+
bound_handlers = Int.Map.empty;
77+
}
78+
79+
let handler t ~cont ~arg_num =
80+
if Int.Set.mem cont state.all_handlers then multiple_handler cont;
81+
state.all_handlers <- Int.Set.add cont state.all_handlers;
82+
let bound_handlers = Int.Map.add cont arg_num t.bound_handlers in
83+
{ bound_handlers; }
84+
85+
let jump t ~cont ~arg_num =
86+
match Int.Map.find cont t.bound_handlers with
87+
| handler_args ->
88+
if arg_num <> handler_args then
89+
wrong_arguments cont handler_args arg_num
90+
| exception Not_found -> unbound_handler cont
91+
92+
let print_error ppf error =
93+
match error with
94+
| Unbound_handler { cont } ->
95+
if Int.Set.mem cont state.all_handlers then
96+
Format.fprintf ppf
97+
"Continuation %d was used outside the scope of its handler"
98+
cont
99+
else
100+
Format.fprintf ppf
101+
"Continuation %d was used but never bound"
102+
cont
103+
| Multiple_handlers { cont; } ->
104+
Format.fprintf ppf
105+
"Continuation %d was declared in more than one handler"
106+
cont
107+
| Wrong_arguments_number { cont; handler_args; jump_args } ->
108+
Format.fprintf ppf
109+
"Continuation %d was declared with %d arguments but called with %d"
110+
cont
111+
handler_args
112+
jump_args
113+
114+
let print_error_newline ppf error =
115+
Format.fprintf ppf "%a@." print_error error
116+
117+
let report ppf =
118+
if ErrorSet.is_empty state.errors then false
119+
else begin
120+
ErrorSet.iter (fun err -> print_error_newline ppf err) state.errors;
121+
true
122+
end
123+
end
124+
125+
let rec check env (expr : Cmm.expression) =
126+
match expr with
127+
| Cconst_int _ | Cconst_natint _ | Cconst_float _ | Cconst_symbol _
128+
| Cvar _ ->
129+
()
130+
| Clet (_, expr, body)
131+
| Clet_mut (_, _, expr, body) ->
132+
check env expr;
133+
check env body
134+
| Cphantom_let (_, _, expr) ->
135+
check env expr
136+
| Cassign (_, expr) ->
137+
check env expr
138+
| Ctuple exprs ->
139+
List.iter (check env) exprs
140+
| Cop (_, args, _) ->
141+
List.iter (check env) args;
142+
| Csequence (expr1, expr2) ->
143+
check env expr1;
144+
check env expr2
145+
| Cifthenelse (test, _, ifso, _, ifnot, _) ->
146+
check env test;
147+
check env ifso;
148+
check env ifnot
149+
| Cswitch (body, _, branches, _) ->
150+
check env body;
151+
Array.iter (fun (expr, _) -> check env expr) branches
152+
| Ccatch (rec_flag, handlers, body) ->
153+
let env_extended =
154+
List.fold_left
155+
(fun env (cont, args, _, _) ->
156+
Env.handler env ~cont ~arg_num:(List.length args))
157+
env
158+
handlers
159+
in
160+
check env_extended body;
161+
let env_handler =
162+
match rec_flag with
163+
| Recursive -> env_extended
164+
| Nonrecursive -> env
165+
in
166+
List.iter (fun (_, _, handler, _) -> check env_handler handler) handlers
167+
| Cexit (cont, args) ->
168+
Env.jump env ~cont ~arg_num:(List.length args)
169+
| Ctrywith (body, _, handler, _) ->
170+
(* Jumping from inside a trywith body to outside isn't very nice,
171+
but it's handled correctly by Linearize, as it happens
172+
when compiling match ... with exception ..., for instance, so it is
173+
not reported as an error. *)
174+
check env body;
175+
check env handler
176+
177+
let run ppf (fundecl : Cmm.fundecl) =
178+
let env = Env.init () in
179+
check env fundecl.fun_body;
180+
Env.report ppf

‎asmcomp/cmm_invariants.mli

+36
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
(**************************************************************************)
2+
(* *)
3+
(* OCaml *)
4+
(* *)
5+
(* Vincent Laviron, OCamlPro *)
6+
(* *)
7+
(* Copyright 2017 OCamlPro SAS *)
8+
(* *)
9+
(* All rights reserved. This file is distributed under the terms of *)
10+
(* the GNU Lesser General Public License version 2.1, with the *)
11+
(* special exception on linking described in the file LICENSE. *)
12+
(* *)
13+
(**************************************************************************)
14+
15+
(* Check a number of continuation-related invariants *)
16+
17+
(* Currently, this checks that :
18+
- Every use of a continuation occurs within the scope of its handler
19+
- Exit instructions take the same number of arguments as their handler.
20+
- In every function declaration, a given continuation can only be
21+
declared in a single handler.
22+
23+
This is intended to document what invariants the backend can rely upon.
24+
The first two would trigger errors later, and the last one, while
25+
harmless for now, is not that hard to ensure, could be useful for
26+
future work on the backend, and helped detect a code duplication bug.
27+
28+
These invariants are not checked by default, but the check can be turned
29+
on with the -dcmm-invariants compilation flag.
30+
*)
31+
32+
(** [run ppf fundecl] analyses the given function, and returns whether
33+
any errors were encountered (with corresponding error messages printed
34+
on the given formatter). *)
35+
36+
val run : Format.formatter -> Cmm.fundecl -> bool

‎compilerlibs/Makefile.compilerlibs

+1
Original file line numberDiff line numberDiff line change
@@ -136,6 +136,7 @@ ASMCOMP=\
136136
asmcomp/cmmgen_state.cmo \
137137
asmcomp/cmm_helpers.cmo \
138138
asmcomp/cmmgen.cmo \
139+
asmcomp/cmm_invariants.cmo \
139140
asmcomp/interval.cmo \
140141
asmcomp/printmach.cmo asmcomp/selectgen.cmo \
141142
asmcomp/selection.cmo \
There was a problem loading the remainder of the diff.

0 commit comments

Comments
 (0)
Please sign in to comment.