Permalink
Browse files

Add subprogram's preconditions to bl_preconditions.

I.e. when constraint-checking a subprogram, assume the subprogram's
preconditions at its entry point.
  • Loading branch information...
xlq committed Sep 16, 2012
1 parent ae8308a commit 5e7fd46babcbf0bc6a000d262835c1cdf0678950
Showing with 28 additions and 18 deletions.
  1. +0 −10 icode.ml
  2. +0 −3 icode.mli
  3. +10 −0 symbols.ml
  4. +3 −0 symbols.mli
  5. +15 −5 translation.ml
View
@@ -322,13 +322,3 @@ let calculate_versions (blocks: block list): unit =
block.bl_body <- Some
(finish_iterm (unsome block.bl_body))
) blocks
let rec bind_versions f e =
match e with
| Boolean_literal _ -> e
| Integer_literal _ -> e
| Var(loc, x) -> Var_v(loc, f x)
| Var_v _ -> e
| Negation(e) -> Negation(bind_versions f e)
| Comparison(op, lhs, rhs) ->
Comparison(op, bind_versions f lhs, bind_versions f rhs)
View
@@ -91,6 +91,3 @@ val describe_constraint_origin : constraint_origin -> string
(* Calculate bl_in. This is essentially liveness analysis. *)
val calculate_versions: block list -> unit
(* Change all Var to Var_v in an expression. *)
val bind_versions : (symbol -> symbol_v) -> expr -> expr
View
@@ -205,3 +205,13 @@ let free_variables e =
| Comparison(_,lhs,rhs) ->
search (search vars lhs) rhs
in search [] e
let rec bind_versions f e =
match e with
| Boolean_literal _ -> e
| Integer_literal _ -> e
| Var(loc, x) -> Var_v(loc, f x)
| Var_v _ -> e
| Negation(e) -> Negation(bind_versions f e)
| Comparison(op, lhs, rhs) ->
Comparison(op, bind_versions f lhs, bind_versions f rhs)
View
@@ -114,3 +114,6 @@ val dump_symbols : unit -> unit
(* Return a list of all the free variables in an expression. *)
val free_variables : expr -> symbol_v list
(* Change all Var to Var_v in an expression. *)
val bind_versions : (symbol -> symbol_v) -> expr -> expr
View
@@ -353,6 +353,7 @@ let translate_subprogram_body compiler state subprogram_sym sub =
sub.Parse_tree.sub_body
in
(* Add parameters to bl_in (calculate_versions doesn't do this). *)
assert (Symbols.Maps.is_empty entry_point.bl_in);
entry_point.bl_in <-
List.fold_left (fun bl_in param ->
match param.sym_info with
@@ -367,11 +368,20 @@ let translate_subprogram_body compiler state subprogram_sym sub =
Symbols.Maps.add param paramv bl_in
) Symbols.Maps.empty subprogram_info.sub_parameters;
calculate_versions state.st_blocks;
(*let f = new_formatter () in
puts f "Dumping blocks before type checking...";
break f;
dump_blocks f state.st_blocks;
prerr_endline (get_fmt_str f);*)
(* Add preconditions to bl_preconditions
(constraint_check_blocks doesn't do this). *)
assert (match entry_point.bl_preconditions with [] -> true | _ -> false);
entry_point.bl_preconditions <-
List.map
(fun e ->
(* NOTE: This constraint_origin should never get used anyway,
because there is never a Jump_term to the entry point. *)
(From_preconditions(
unsome subprogram_sym.sym_declared,
unsome subprogram_sym.sym_declared,
subprogram_sym),
bind_versions (fun x -> Symbols.Maps.find x entry_point.bl_in) e))
subprogram_info.sub_preconditions;
Type_checking.type_check_blocks state.st_blocks;
Constraint_checking.constraint_check_blocks state.st_blocks entry_point;
(*Backend_c.translate compiler subprogram_sym entry_point state.st_blocks;*)

0 comments on commit 5e7fd46

Please sign in to comment.