Permalink
Browse files

Prove postconditions before returning from subprogram.

  • Loading branch information...
xlq committed Sep 2, 2012
1 parent d19daf1 commit 70a726078e3945cf3ce0b6e0a942cfc003a2c36e
Showing with 159 additions and 109 deletions.
  1. +30 −5 icode.ml
  2. +12 −2 icode.mli
  3. +3 −3 symbols.ml
  4. +1 −1 symbols.mli
  5. +70 −80 translation.ml
  6. +43 −18 type_checking.ml
View
@@ -14,8 +14,13 @@ type liveness_origin =
| Used_variable of Lexing.position
| From_parameters
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
| Null_term of loc * (constraint_origin * expr) list
| Assignment_term of loc * expr * expr * iterm
| If_term of loc * expr * iterm * iterm
| Jump_term of jump_info
@@ -46,7 +51,7 @@ and block =
bl_statement : Parse_tree.statement;
mutable bl_body : iterm option;
mutable bl_in : (liveness_origin * symbol_v) Symbols.Maps.t;
mutable bl_preconditions: expr list;
mutable bl_preconditions: (constraint_origin * expr) list;
}
let rec dump_term (f: formatter) = function
@@ -106,7 +111,7 @@ let dump_block (f: formatter) (bl: block) =
break f
) bl.bl_in
end;
List.iter (fun p ->
List.iter (fun (_, p) ->
puts f ("| "
^ string_of_expr p);
break f
@@ -124,6 +129,19 @@ let map_minus_set
=
Symbols.Sets.fold Symbols.Maps.remove b a
let loc_of_constraint_origin = function
| From_postconditions(loc, _)
| From_preconditions(loc, _)
| From_static_assertion(loc) -> loc
let describe_constraint_origin = function
| From_postconditions(_, sub) ->
"a postcondition of " ^ describe_symbol sub
| From_preconditions(_, sub) ->
"a precondition of calling " ^ describe_symbol sub
| From_static_assertion(_) ->
"a static assertion"
let equal_keys a b =
let rec compare = function
| [], [] -> true
@@ -162,7 +180,10 @@ let rec bind_versions_expr context e =
let rec bind_versions context iterm =
match iterm with
| Null_term _ -> iterm
| Null_term(loc, constr) ->
Null_term(loc,
List.map (fun (origin, constr) ->
(origin, bind_versions_expr context constr)) constr)
| Assignment_term(loc, dest, src, tail) ->
let src = bind_versions_expr context src in
let context = bind_versions_lvalue context dest in
@@ -226,7 +247,11 @@ let calculate_free_names (blocks: block list): unit =
(bound: Symbols.Sets.t):
iterm -> (liveness_origin * symbol_v) Symbols.Maps.t
= function
| Null_term _ | Inspect_type_term _ -> free
| Null_term(_,constr) ->
List.fold_left
(fun free (_, constr) -> esearch free bound constr)
free constr
| Inspect_type_term _ -> free
| Assignment_term(_,dest,src,p) ->
let free, bound = esearch_lvalue free bound dest in
search (esearch free bound src) bound p
View
@@ -19,8 +19,15 @@ type liveness_origin =
| Used_variable of Lexing.position
| From_parameters
(* Reason why a constraint must be solved. *)
type constraint_origin =
| From_postconditions of Lexing.position * symbol (* subprogram symbol *)
| From_preconditions of Lexing.position * symbol (* subprogram symbol *)
| From_static_assertion of Lexing.position
type iterm =
| Null_term of loc
(* 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 *)
@@ -73,11 +80,14 @@ and block =
Analogous to the variables that are
live when entering the block. *)
mutable bl_in : (liveness_origin * symbol_v) Symbols.Maps.t;
mutable bl_preconditions: expr list;
mutable bl_preconditions: (constraint_origin * expr) list;
}
val new_block_id: unit -> int
val dump_blocks: formatter -> block list -> unit
val loc_of_constraint_origin : constraint_origin -> Lexing.position
val describe_constraint_origin : constraint_origin -> string
(* Calculate bl_free. This is essentially liveness analysis. *)
val calculate_free_names: block list -> unit
View
@@ -69,11 +69,11 @@ end
module Maps = Map.Make(Ordered)
module Sets = Set.Make(Ordered)
let rec get_loc_of_expression = function
let rec loc_of_expression = function
| Boolean_literal(loc,_) | Integer_literal(loc,_)
| Var(loc,_) | Var_v(loc,_) -> loc
| Negation(e) -> get_loc_of_expression e
| Comparison(_,lhs,_) -> get_loc_of_expression lhs
| Negation(e) -> loc_of_expression e
| Comparison(_,lhs,_) -> loc_of_expression lhs
let root_symbol = {
sym_id = 0;
View
@@ -76,7 +76,7 @@ exception Already_defined of symbol
module Maps : Map.S with type key = symbol
module Sets : Set.S with type elt = symbol
val get_loc_of_expression : expr -> Lexing.position
val loc_of_expression : expr -> Lexing.position
val root_symbol : symbol
val dotted_name : symbol -> string list
val full_name : symbol -> string
Oops, something went wrong.

0 comments on commit 70a7260

Please sign in to comment.