Permalink
Browse files

Check types of out parameters when returning.

  • Loading branch information...
xlq committed Sep 2, 2012
1 parent 6ffebec commit 922bd082d6d64eec749cba1a048d3c8bee670bcb
Showing with 112 additions and 48 deletions.
  1. +3 −1 backend_c.ml
  2. +53 −11 icode.ml
  3. +13 −2 icode.mli
  4. +15 −24 translation.ml
  5. +27 −8 type_checking.ml
  6. +1 −2 type_checking.mli
View
@@ -91,7 +91,9 @@ let translate_lvalue context = function
end
let rec translate_icode context f = function
| Null_term _ -> ()
| Return_term _ ->
puts f "return;";
break f
| Assignment_term(loc, dest, src, tail) ->
puts f (translate_lvalue context dest
^ " = " ^ snd (translate_expr context src) ^ ";");
View
@@ -13,21 +13,33 @@ type loc = Parse_tree.loc
type liveness_origin =
| Used_variable of Lexing.position
| From_parameters
| Returned_parameter of Lexing.position
type constraint_origin =
| From_postconditions of Lexing.position * symbol
| From_preconditions of Lexing.position * symbol
| From_static_assertion of Lexing.position
type iterm =
| Null_term of loc * (constraint_origin * expr) list
| Assignment_term of loc * expr * expr * iterm
| If_term of loc * expr * iterm * iterm
| Return_term of return_info
| Jump_term of jump_info
| Call_term of call_info * iterm
| Inspect_type_term of loc * symbol * iterm
| Static_assert_term of loc * expr * iterm
and return_info =
{
ret_location : loc;
(* Subprogram being returned from. *)
ret_subprogram : symbol;
(* Versions of variables to bind to the out parameters
of the subprogram. This is empty until after
calculate_free_names. *)
ret_versions : symbol_v Symbols.Maps.t;
}
and jump_info =
{
jmp_location : loc;
@@ -55,7 +67,7 @@ and block =
}
let rec dump_term (f: formatter) = function
| Null_term(_) -> puts f "null"
| Return_term(_) -> puts f "return"
| Assignment_term(_,x,m,tail) ->
puts f (string_of_expr x ^ " := "
^ string_of_expr m ^ ";");
@@ -180,10 +192,21 @@ let rec bind_versions_expr context e =
let rec bind_versions context iterm =
match iterm with
| Null_term(loc, constr) ->
Null_term(loc,
List.map (fun (origin, constr) ->
(origin, bind_versions_expr context constr)) constr)
| Return_term(ret) ->
begin match ret.ret_subprogram.sym_info with Subprogram_sym(info) ->
let versions =
List.fold_left (fun versions param ->
match param.sym_info with
| Parameter_sym((Out_parameter|In_out_parameter), _) ->
Symbols.Maps.add param
(Symbols.Maps.find param context)
versions
| Parameter_sym((Const_parameter|In_parameter), _) ->
versions
) Symbols.Maps.empty info.sub_parameters
in
Return_term {ret with ret_versions = versions}
end
| Assignment_term(loc, dest, src, tail) ->
let src = bind_versions_expr context src in
let context = bind_versions_lvalue context dest in
@@ -247,10 +270,23 @@ let calculate_free_names (blocks: block list): unit =
(bound: Symbols.Sets.t):
iterm -> (liveness_origin * symbol_v) Symbols.Maps.t
= function
| Null_term(_,constr) ->
List.fold_left
(fun free (_, constr) -> esearch free bound constr)
free constr
| Return_term(ret) ->
begin match ret.ret_subprogram.sym_info with Subprogram_sym(info) ->
(* All the out parameters not in bound are free in this block. *)
List.fold_left (fun free param ->
match param.sym_info with
| Parameter_sym((Const_parameter | In_parameter),_) ->
free
| Parameter_sym((In_out_parameter | Out_parameter),_) ->
if (Symbols.Sets.mem param bound)
|| (Symbols.Maps.mem param free) then
free
else
Symbols.Maps.add param
(Returned_parameter ret.ret_location, new_version param)
free
) free info.sub_parameters
end
| Inspect_type_term _ -> free
| Assignment_term(_,dest,src,p) ->
let free, bound = esearch_lvalue free bound dest in
@@ -311,6 +347,8 @@ let calculate_free_names (blocks: block list): unit =
if Symbols.Sets.mem x bound then begin
(* x was bound further up. *)
free
end else if Symbols.Maps.mem x free then begin
free
end else begin
(* x is not bound - it was live at the start of this block. *)
Symbols.Maps.add x (Used_variable loc, new_version x) free
@@ -325,7 +363,7 @@ let calculate_free_names (blocks: block list): unit =
| Var_v(loc, x) ->
free, Symbols.Sets.add x.ver_symbol bound
in
block.bl_in <- search Symbols.Maps.empty Symbols.Sets.empty
block.bl_in <- search block.bl_in Symbols.Sets.empty
(unsome block.bl_body)
) blocks;
@@ -355,5 +393,9 @@ let calculate_free_names (blocks: block list): unit =
(* Bind variables to versions. *)
List.iter (fun block ->
let context = Symbols.Maps.map snd block.bl_in in
block.bl_preconditions <- List.map
(fun (origin, constr) ->
(origin, bind_versions_expr context constr))
block.bl_preconditions;
block.bl_body <- Some (bind_versions context (unsome block.bl_body))
) blocks
View
@@ -18,6 +18,7 @@ type loc = Parse_tree.loc
type liveness_origin =
| Used_variable of Lexing.position
| From_parameters
| Returned_parameter of Lexing.position
(* Reason why a constraint must be solved. *)
type constraint_origin =
@@ -26,19 +27,29 @@ type constraint_origin =
| From_static_assertion of Lexing.position
type iterm =
(* XXX: constraint_origin in Null_term contains a lot of redundant information. *)
| Null_term of loc * (constraint_origin * expr) list (* postconditions *)
| Assignment_term of loc * expr (* destination (L-value) *)
* expr (* source *)
* iterm (* continuation *)
| If_term of loc * expr (* condition *)
* iterm (* true part *)
* iterm (* false part *)
| Return_term of return_info
| Jump_term of jump_info
| Call_term of call_info * iterm
| Inspect_type_term of loc * symbol * iterm
| Static_assert_term of loc * expr * iterm
and return_info =
{
ret_location : loc;
(* Subprogram being returned from. *)
ret_subprogram : symbol;
(* Versions of variables to bind to the out parameters
of the subprogram. This is empty until after
calculate_free_names. *)
ret_versions : symbol_v Symbols.Maps.t;
}
and jump_info =
{
(* Source file location. *)
View
@@ -25,7 +25,7 @@ type after =
(* Return_with(sub, constr)
Return from subprogram sub: the postconditions constr
must be met. *)
| Return_with of symbol * expr list
| Return_from of symbol
type state =
{
@@ -158,13 +158,12 @@ let rec translate_statement
match statement with
| Parse_tree.No_statement(loc) | Parse_tree.Null_statement(loc) ->
begin match after with
| Return_with(sub, constraints) ->
Null_term(
loc,
List.map
(fun constr ->
(From_postconditions(loc, sub), constr))
constraints)
| Return_from(sub) ->
Return_term {
ret_location = loc;
ret_subprogram = sub;
ret_versions = Symbols.Maps.empty
}
| Continue_with cont ->
make_jump loc cont
end
@@ -259,18 +258,6 @@ and translate_block
make_block state statement
(fun _ -> translate_statement state scope after statement)
(* Make a sym -> type map of a subprogram's parameters. *)
let parameters_of_subprogram sym =
match sym.sym_info with
| Subprogram_sym(subprogram_info) ->
List.fold_left (fun result param ->
match param.sym_info with
| Parameter_sym(mode, t) ->
Symbols.Maps.add param (mode, t) result
| _ ->
result
) Symbols.Maps.empty subprogram_info.sub_parameters
let translate_subprogram_prototype state scope sub =
match sub.Parse_tree.sub_name with [name] ->
let subprogram_info = {
@@ -333,12 +320,11 @@ let translate_subprogram_body compiler state subprogram_sym sub =
let subprogram_info = match subprogram_sym.sym_info with
| Subprogram_sym(info) -> info
in
let parameters = parameters_of_subprogram subprogram_sym in
let scope = subprogram_sym in
assert (match state.st_blocks with [] -> true | _ -> false);
let entry_point =
translate_block state scope
(Return_with(subprogram_sym, subprogram_info.sub_postconditions))
(Return_from(subprogram_sym))
sub.Parse_tree.sub_body
in
entry_point.bl_preconditions <- List.map
@@ -348,11 +334,16 @@ let translate_subprogram_body compiler state subprogram_sym sub =
subprogram_sym),
precondition))
subprogram_info.sub_preconditions;
entry_point.bl_in <-
List.fold_left
(fun bl_in param ->
Symbols.Maps.add param
(From_parameters, new_version param) bl_in)
Symbols.Maps.empty subprogram_info.sub_parameters;
calculate_free_names state.st_blocks;
Type_checking.type_check_blocks
state.st_blocks
entry_point
parameters;
entry_point;
Backend_c.translate compiler subprogram_sym entry_point state.st_blocks;
state.st_blocks <- []
View
@@ -38,6 +38,10 @@ let report_liveness_origin sym = function
Errors.semantic_error loc
(String.capitalize (describe_symbol sym)
^ " is used here.")
| Returned_parameter loc ->
Errors.semantic_error loc
("Out " ^ describe_symbol sym
^ " is returned here.")
(* Substitute a variable with a term, in the given expression. *)
let rec subst x_sym replacement expr =
@@ -233,11 +237,25 @@ let rec type_check
(context: context)
(iterm: iterm): ttype
= match iterm with
| Null_term(loc, constr) ->
List.iter
(fun (origin, constr) ->
(prove state context origin constr))
constr;
| Return_term(ret) ->
begin match ret.ret_subprogram.sym_info with Subprogram_sym(info) ->
let postconditions = ref info.sub_postconditions in
List.iter (fun param ->
match param.sym_info with
| Parameter_sym((Out_parameter | In_out_parameter), t) ->
let src_version = Symbols.Maps.find param ret.ret_versions in
ignore (coerce context (unsome src_version.ver_type) t);
postconditions :=
List.map (subst param (Var_v(ret.ret_location, src_version)))
!postconditions;
| Parameter_sym((Const_parameter | In_parameter), _) -> ()
) info.sub_parameters;
List.iter (fun constr ->
prove state context
(From_postconditions(ret.ret_location, ret.ret_subprogram))
constr
) !postconditions
end;
got_type context Unit_type
| Assignment_term(loc, dest, src, tail) ->
let src_type =
@@ -287,14 +305,16 @@ let rec type_check
Symbols.Maps.find x jmp.jmp_versions
with Not_found ->
(* XXX: Is this ever reachable? *)
prerr_endline "YES, THIS IS REACHABLE.";
Errors.semantic_error jmp.jmp_location
(String.capitalize (describe_symbol x)
^ " must be initialised by now, but might not be.");
report_liveness_origin x origin;
raise Type_error
in
let t = coerce context (unsome source_version.ver_type) (unsome target.ver_type) in
ignore t;
ignore (coerce context
(unsome source_version.ver_type)
(unsome target.ver_type));
preconditions :=
List.map
(fun (origin, constr) ->
@@ -507,7 +527,6 @@ let resolve_unknowns
let type_check_blocks
(blocks: block list)
(entry_point: block)
(parameters: (param_mode * ttype) Symbols.Maps.t)
=
(* For each block, set unknown types for live variables. *)
List.iter (fun block ->
View
@@ -2,6 +2,5 @@ open Symbols
open Icode
val type_check_blocks : block list
-> block (* entry point *)
-> (param_mode * ttype) Symbols.Maps.t (* parameters *)
-> block (* entry point *)
-> unit

0 comments on commit 922bd08

Please sign in to comment.