Propagate constraints between blocks.

constraint_checking.ml

@@ -161,7 +161,9 @@ let rec check_iterm context iterm =
          List.iter (fun postcondition ->
             prove context
                (From_postconditions(
-                  ret.ret_location, ret.ret_subprogram))
+                  loc_of_expression postcondition,
+                  ret.ret_location,
+                  ret.ret_subprogram))
                (bind_versions
                   (fun x -> Symbols.Maps.find x ret.ret_versions)
                   postcondition)
@@ -176,13 +178,18 @@ let rec check_iterm context iterm =
          [{sym_info=Subprogram_sym(info)} as subprogram]
       } as call, tail)
    ->
-      let preconditions = ref info.sub_preconditions in
+      let preconditions = ref
+         (List.map (fun e -> (loc_of_expression e, e))
+            info.sub_preconditions)
+      in
       let postconditions = ref info.sub_postconditions in
       let invariants = ref [] in
       List.iter2
          (fun ({sym_info=Parameter_sym(mode,_)} as param)
               (arg_in, arg_out) ->
-            preconditions := List.map (subst param arg_in) !preconditions;
+            preconditions := List.map
+               (fun (loc, e) -> (loc, subst param arg_in e))
+               !preconditions;
             postconditions := List.map
                (subst param
                   (match mode, arg_out with
@@ -195,9 +202,9 @@ let rec check_iterm context iterm =
                         arg_out))
                !postconditions
          ) info.sub_parameters call.call_bound_arguments;
-      List.iter (fun constr ->
+      List.iter (fun (loc, constr) ->
          prove context
-            (From_preconditions(call.call_location, subprogram))
+            (From_preconditions(loc, call.call_location, subprogram))
             constr
       ) !preconditions;
       check_iterm
@@ -207,7 +214,7 @@ let rec check_iterm context iterm =
                   (List.rev_append !invariants context.cc_facts)}
          tail
 
-let constraint_check_blocks blocks =
+let constraint_check_blocks blocks entry_point =
    let changed = ref true in
    while !changed do
       changed := false;
@@ -217,8 +224,33 @@ let constraint_check_blocks blocks =
             cc_facts = List.map snd block.bl_preconditions;
          } in
          check_iterm context (unsome block.bl_body);
-         prerr_endline (string_of_int (List.length !(context.cc_unsolved))
-            ^ " unsolved constraints.")
+         List.iter (fun (origin, constr) ->
+            (* Add this unsolved constraint to this block's
+               preconditions iff the constraint doesn't contain
+               versions not in bl_in. *)
+            if (block != entry_point) (* cannot add preconditions to entry point *)
+            && (List.for_all
+               (fun xv ->
+                  (Symbols.Maps.find xv.ver_symbol block.bl_in) == xv)
+               (free_variables constr))
+            then begin
+               block.bl_preconditions <- (origin, constr)
+                  :: block.bl_preconditions;
+               changed := true
+            end else begin
+               Errors.semantic_error
+                  (loc_of_constraint_origin origin)
+                  ("Cannot prove `"
+                     ^ string_of_expr constr ^ "', "
+                     ^ describe_constraint_origin origin ^ ".");
+               begin match origin with
+                  | From_postconditions(loc,_,_)
+                  | From_preconditions(loc,_,_) ->
+                     Errors.semantic_error loc
+                        ("Original constraint was here.")
+                  | From_static_assertion _ -> ()
+               end
+            end
+        ) !(context.cc_unsolved)
       ) blocks
    done
-

constraint_checking.mli

@@ -1,3 +1,5 @@
 open Icode
 
-val constraint_check_blocks : block list -> unit
+val constraint_check_blocks : block list
+                           -> block (* entry point *)
+                           -> unit

icode.ml

@@ -11,10 +11,11 @@ let new_block_id () =
 type loc = Parse_tree.loc
 
 type constraint_origin =
-   | From_postconditions of Lexing.position * symbol
-   | From_preconditions of Lexing.position * symbol
+   | From_postconditions of Lexing.position * Lexing.position * symbol
+   | From_preconditions of Lexing.position * Lexing.position * symbol
    | From_static_assertion of Lexing.position
 
+
 type iterm =
    | Assignment_term of loc * expr * expr * iterm
    | If_term of loc * expr * iterm * iterm
@@ -124,14 +125,14 @@ let dump_blocks (f: formatter) (blocks: block list) =
    List.iter (dump_block f) blocks
 
 let loc_of_constraint_origin = function
-   | From_postconditions(loc, _)
-   | From_preconditions(loc, _)
+   | From_postconditions(_, loc, _)
+   | From_preconditions(_, loc, _)
    | From_static_assertion(loc) -> loc
 
 let describe_constraint_origin = function
-   | From_postconditions(_, sub) ->
+   | From_postconditions(_, _, sub) ->
       "a post-condition of " ^ describe_symbol sub
-   | From_preconditions(_, sub) ->
+   | From_preconditions(_, _, sub) ->
       "a pre-condition of calling " ^ describe_symbol sub
    | From_static_assertion(_) ->
       "a static assertion"

icode.mli

@@ -15,8 +15,12 @@ type loc = Parse_tree.loc
 
 (* 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_postconditions of Lexing.position (* original location *)
+                          * Lexing.position (* Return_term location *)
+                          * symbol (* subprogram symbol *)
+   | From_preconditions of Lexing.position (* original location *)
+                         * Lexing.position (* call location *)
+                         * symbol (* subprogram symbol *)
    | From_static_assertion of Lexing.position
 
 type iterm =
@@ -80,6 +84,8 @@ and block =
 val new_block_id: unit -> int
 val dump_blocks: formatter -> block list -> unit
 
+(* Get the location in the source that produced a constraint.
+   E.g. for a precondition of a call, this returns the location of the call. *)
 val loc_of_constraint_origin : constraint_origin -> Lexing.position
 val describe_constraint_origin : constraint_origin -> string
 

symbols.ml

@@ -195,3 +195,13 @@ let dump_symbols () =
       prerr_endline ("Symbol " ^ full_name sym);
       List.iter dump_sym sym.sym_children
    in dump_sym root_symbol
+
+let free_variables e =
+   let rec search vars = function
+      | Boolean_literal _ -> vars
+      | Integer_literal _ -> vars
+      | Var_v(_,xv) -> xv::vars
+      | Negation(e) -> search vars e
+      | Comparison(_,lhs,rhs) ->
+         search (search vars lhs) rhs
+   in search [] e

symbols.mli

@@ -111,3 +111,6 @@ val new_overloaded_symbol : symbol
                          -> symbol
 val new_version : symbol -> symbol_v
 val dump_symbols : unit -> unit
+
+(* Return a list of all the free variables in an expression. *)
+val free_variables : expr -> symbol_v list

translation.ml

@@ -352,14 +352,7 @@ let translate_subprogram_body compiler state subprogram_sym sub =
          (Return_from(subprogram_sym))
          sub.Parse_tree.sub_body
    in
-   entry_point.bl_preconditions <- List.map
-      (fun precondition ->
-         (From_preconditions(
-            Symbols.loc_of_expression precondition,
-            subprogram_sym),
-          precondition))
-      subprogram_info.sub_preconditions;
-   (* Add parameters to bl_in (needed by calculate_versions). *)
+   (* Add parameters to bl_in (calculate_versions doesn't do this). *)
    entry_point.bl_in <-
       List.fold_left (fun bl_in param ->
          match param.sym_info with
@@ -380,7 +373,7 @@ let translate_subprogram_body compiler state subprogram_sym sub =
    dump_blocks f state.st_blocks;
    prerr_endline (get_fmt_str f);*)
    Type_checking.type_check_blocks state.st_blocks;
-   Constraint_checking.constraint_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;*)
    state.st_blocks <- []