[m-rev.] for review: fix assertion failure with promise_equivalent_solutions

Julien Fischer juliensf at csse.unimelb.edu.au
Thu Jan 17 16:46:25 AEDT 2008


For review by anyone.

Estimated hours taken: 1.5
Branches: main

Fix bug #30.  The determinism analysis run as part of partial deduction
was erroneously reporting that the head of a promise_equivalent_solutions
scope contained extra variables, i.e. non-locals that were not further bound
or (potentially) constrained within the scope. 
This violated an assertion that this run of determinism checking should
not produce any errors.

The error was caused because some of the variables in the scope head that
prior to inlining had inst any, had become ground after inlining.
The fix is to ignore such extra variables in determinism analysis passes
that are invoked after inlining.

compiler/det_util.m:
 	Add a field to the det_info structure that indicates whether or not we
 	should report extra variables occurring in the head of a
 	promise_equivalent_solutions scope as an error.

 	Define a new type to represent this.

compiler/det_analysis.m:
 	Check the value of the above field before reporting the
 	presence of extra variables in a promise_equivalent_solutions scope.

compiler/pd_util.m:
compiler/det_report.m:
compiler/simplify.m:
 	Set the value of the det_info di_pess_extra_vars field as necessary.

tests/valid/Mercury.options:
tests/valid/Mmakefile:
tests/valid/equiv_solns_ia.m:
 	Regression test for the above.

Julien.

Index: compiler/det_analysis.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/det_analysis.m,v
retrieving revision 1.210
diff -u -r1.210 det_analysis.m
--- compiler/det_analysis.m	30 Dec 2007 08:23:36 -0000	1.210
+++ compiler/det_analysis.m	17 Jan 2008 05:40:27 -0000
@@ -284,7 +284,8 @@
      proc_info_get_goal(Proc0, Goal0),
      proc_info_get_initial_instmap(Proc0, !.ModuleInfo, InstMap0),
      proc_info_get_vartypes(Proc0, VarTypes),
-    det_info_init(!.ModuleInfo, VarTypes, PredId, ProcId, DetInfo0),
+    det_info_init(!.ModuleInfo, VarTypes, PredId, ProcId,
+        pess_extra_vars_report, DetInfo0),
      det_infer_goal(Goal0, Goal, InstMap0, SolnContext, [], no,
          InferDetism, _,  DetInfo0, DetInfo, [], !:Specs),
      det_info_get_module_info(DetInfo, !:ModuleInfo),
@@ -1490,7 +1491,12 @@
          % Which vars were listed in the promise_equivalent_solutions
          % but not bound inside the scope?
          set.difference(set.list_to_set(Vars), BoundVars, ExtraVars),
-        ( set.empty(ExtraVars) ->
+        det_info_get_pess_extra_vars(!.DetInfo, IgnoreExtraVars),
+        ( 
+            ( set.empty(ExtraVars)
+            ; IgnoreExtraVars = pess_extra_vars_ignore
+            )
+        ->
              true
          ;
              ExtraVarNames = list.map(lookup_var_name_in_varset(VarSet),
Index: compiler/det_report.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/det_report.m,v
retrieving revision 1.141
diff -u -r1.141 det_report.m
--- compiler/det_report.m	30 Dec 2007 08:23:36 -0000	1.141
+++ compiler/det_report.m	17 Jan 2008 05:40:27 -0000
@@ -255,7 +255,8 @@
              proc_info_get_goal(ProcInfo0, Goal),
              proc_info_get_vartypes(ProcInfo0, VarTypes),
              proc_info_get_initial_instmap(ProcInfo0, !.ModuleInfo, InstMap0),
-            det_info_init(!.ModuleInfo, VarTypes, PredId, ProcId, DetInfo0),
+            det_info_init(!.ModuleInfo, VarTypes, PredId, ProcId, 
+                pess_extra_vars_report, DetInfo0),
              det_diagnose_goal(Goal, InstMap0, DeclaredDetism, [],
                  DetInfo0, DetInfo, GoalMsgs0),
              det_info_get_module_info(DetInfo, !:ModuleInfo),
Index: compiler/det_util.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/det_util.m,v
retrieving revision 1.45
diff -u -r1.45 det_util.m
--- compiler/det_util.m	30 Dec 2007 08:23:36 -0000	1.45
+++ compiler/det_util.m	17 Jan 2008 05:40:27 -0000
@@ -37,6 +37,26 @@
      --->    changed
      ;       unchanged.

+    % Should we emit an error message about extra variables in the head
+    % of a promise_equivalent_solutions scope?  Extra variables are
+    % those non-locals that are not further bound or (potentially) constrained
+    % by the goal inside the scope.
+    %
+    % We ignore such extra variables when re-running determinism
+    % analysis after optimisations such as inlining have been performed
+    % because not doing so results in spurious error messages.
+    % (Inlining can cause variables that had inst any to become ground.)
+    %
+:- type report_pess_extra_vars
+    --->    pess_extra_vars_report
+            % Emit an error message if the head of a
+            % promise_equivalent_solutions scope contains variables that
+            % are not further bound or (potentially) further constrained
+            % by the goal inside the scope.
+
+    ;       pess_extra_vars_ignore.
+            % Do not emit an error message if the above occurs.
+
  :- type det_info.

      % Given a list of cases, and a list of the possible cons_ids
@@ -66,7 +86,7 @@
      det_info::in) is semidet.

  :- pred det_info_init(module_info::in, vartypes::in, pred_id::in, proc_id::in,
-    det_info::out) is det.
+    report_pess_extra_vars::in, det_info::out) is det.

  :- pred det_info_get_module_info(det_info::in, module_info::out) is det.
  :- pred det_info_get_pred_id(det_info::in, pred_id::out) is det.
@@ -75,6 +95,8 @@
  :- pred det_info_get_reorder_disj(det_info::in, bool::out) is det.
  :- pred det_info_get_fully_strict(det_info::in, bool::out) is det.
  :- pred det_info_get_vartypes(det_info::in, vartypes::out) is det.
+:- pred det_info_get_pess_extra_vars(det_info::in,
+    report_pess_extra_vars::out) is det.

  :- pred det_info_set_module_info(module_info::in, det_info::in, det_info::out)
      is det.
@@ -184,16 +206,18 @@
                  di_proc_id         :: proc_id,     % currently processed
                  di_reorder_conj    :: bool,        % --reorder-conj
                  di_reorder_disj    :: bool,        % --reorder-disj
-                di_fully_strict    :: bool         % --fully-strict
+                di_fully_strict    :: bool,        % --fully-strict
+                di_pess_extra_vars :: report_pess_extra_vars
              ).

-det_info_init(ModuleInfo, VarTypes, PredId, ProcId, DetInfo) :-
+det_info_init(ModuleInfo, VarTypes, PredId, ProcId, PessExtraVars,
+        DetInfo) :-
      module_info_get_globals(ModuleInfo, Globals),
      globals.lookup_bool_option(Globals, reorder_conj, ReorderConj),
      globals.lookup_bool_option(Globals, reorder_disj, ReorderDisj),
      globals.lookup_bool_option(Globals, fully_strict, FullyStrict),
      DetInfo = det_info(ModuleInfo, VarTypes, PredId, ProcId,
-        ReorderConj, ReorderDisj, FullyStrict).
+        ReorderConj, ReorderDisj, FullyStrict, PessExtraVars).

  det_info_get_module_info(DI, DI ^ di_module_info).
  det_info_get_pred_id(DI, DI ^ di_pred_id).
@@ -202,6 +226,7 @@
  det_info_get_reorder_disj(DI, DI ^ di_reorder_disj).
  det_info_get_fully_strict(DI, DI ^ di_fully_strict).
  det_info_get_vartypes(DI, DI ^ di_vartypes).
+det_info_get_pess_extra_vars(DI, DI ^ di_pess_extra_vars).

  det_info_set_module_info(ModuleInfo, DI, DI ^ di_module_info := ModuleInfo).
  det_info_set_vartypes(VarTypes, DI, DI ^ di_vartypes := VarTypes).
Index: compiler/pd_util.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/pd_util.m,v
retrieving revision 1.65
diff -u -r1.65 pd_util.m
--- compiler/pd_util.m	30 Dec 2007 08:23:53 -0000	1.65
+++ compiler/pd_util.m	17 Jan 2008 05:40:27 -0000
@@ -244,7 +244,8 @@
      pd_info_get_module_info(!.PDInfo, ModuleInfo0),
      pd_info_get_pred_proc_id(!.PDInfo, proc(PredId, ProcId)),
      proc_info_get_vartypes(ProcInfo0, VarTypes0),
-    det_info_init(ModuleInfo0, VarTypes0, PredId, ProcId, DetInfo0),
+    det_info_init(ModuleInfo0, VarTypes0, PredId, ProcId, 
+        pess_extra_vars_ignore, DetInfo0),
      pd_info_get_instmap(!.PDInfo, InstMap0),
      pd_info_get_proc_info(!.PDInfo, ProcInfo0),
      simplify_info_init(DetInfo0, Simplifications, InstMap0, ProcInfo0,
@@ -374,7 +375,8 @@
          ModuleInfo0, ModuleInfo1),

      proc_info_get_vartypes(ProcInfo, VarTypes),
-    det_info_init(ModuleInfo1, VarTypes, PredId, ProcId, DetInfo0),
+    det_info_init(ModuleInfo1, VarTypes, PredId, ProcId,
+        pess_extra_vars_ignore, DetInfo0),
      pd_info_get_instmap(!.PDInfo, InstMap),
      det_infer_goal(Goal0, Goal, InstMap, SolnContext, [], no, _, _,
          DetInfo0, DetInfo, [], Specs),
Index: compiler/simplify.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/simplify.m,v
retrieving revision 1.222
diff -u -r1.222 simplify.m
--- compiler/simplify.m	30 Dec 2007 08:23:56 -0000	1.222
+++ compiler/simplify.m	17 Jan 2008 05:40:28 -0000
@@ -380,7 +380,8 @@
      ;
          Simplifications = Simplifications0
      ),
-    det_info_init(!.ModuleInfo, VarTypes0, PredId, ProcId, DetInfo0),
+    det_info_init(!.ModuleInfo, VarTypes0, PredId, ProcId,
+        pess_extra_vars_report, DetInfo0),
      proc_info_get_initial_instmap(!.ProcInfo, !.ModuleInfo, InstMap0),
      simplify_info_init(DetInfo0, Simplifications, InstMap0, !.ProcInfo, Info0),
      proc_info_get_goal(!.ProcInfo, Goal0),
Index: tests/valid/Mercury.options
===================================================================
RCS file: /home/mercury/mercury1/repository/tests/valid/Mercury.options,v
retrieving revision 1.42
diff -u -r1.42 Mercury.options
--- tests/valid/Mercury.options	3 Dec 2007 09:52:14 -0000	1.42
+++ tests/valid/Mercury.options	17 Jan 2008 05:40:28 -0000
@@ -35,6 +35,7 @@
  MCFLAGS-deforest_loop		= -O3 --intermodule-optimization
  MCFLAGS-deforest_rerun_det	= -O3 --check-termination
  MCFLAGS-double_vn		= -O4
+MCFLAGS-equiv_solns_ia		= --inlining --local-constraint-propagation
  MCFLAGS-exists_cast_bug		= --trace rep -O0 --optimize-saved-vars-const
  MCFLAGS-explicit_quant		= --halt-at-warn
  MCFLAGS-func_class		= --no-warn-nothing-exported
Index: tests/valid/Mmakefile
===================================================================
RCS file: /home/mercury/mercury1/repository/tests/valid/Mmakefile,v
retrieving revision 1.203
diff -u -r1.203 Mmakefile
--- tests/valid/Mmakefile	3 Dec 2007 09:52:14 -0000	1.203
+++ tests/valid/Mmakefile	17 Jan 2008 05:40:28 -0000
@@ -85,6 +85,7 @@
  	empty_switch \
  	erl_ite_vars \
  	error \
+	equiv_solns_ia \
  	eval \
  	existential_cons \
  	explicit_quant \
Index: tests/valid/equiv_solns_ia.m
===================================================================
RCS file: tests/valid/equiv_solns_ia.m
diff -N tests/valid/equiv_solns_ia.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/valid/equiv_solns_ia.m	17 Jan 2008 05:40:28 -0000
@@ -0,0 +1,65 @@
+% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
+%
+% rotd-2007-11-27 emits the following error message for this program:
+%
+% equiv_solns_ia.m:051: Error: the `promise_equivalent_solutions' goal lists
+% equiv_solns_ia.m:051:   some extra variables: V_3, V_4 and V_5.
+% Uncaught Mercury exception:
+% Software Error: pd_util.m: Unexpected: rerun_det_analysis: determinism errors
+%
+% Compile with: -C -O0 --inlining --local-constraint-propagation
+%
+% The problem was caused by the fact that inst any non-locals in a promise
+% equivalent_solutions scope must be listed in the scope head but optimizations
+% such as inlining can cause the inst of these non-locals to become ground.
+% Since only variables that become further bound/constrained should be listed
+% in the scope head this means that determinism analysis reruns after
+% inlining reported extra variables in the scope head.
+% 
+:- module equiv_solns_ia.
+:- interface.
+
+:- import_module list.
+
+:- typeclass flatzinc_solver(Solver, Var) <= (Solver -> Var) where [
+
+    pred solve_for_vars(Solver::in, solve_spec(Var)::ia,
+        solver_annotations(Var)::ia, list(Var)::ia) is nondet
+].
+
+:- type solve_spec(Var)
+    --->    satisfy
+    ;       minimize(Var)
+    ;       maximize(Var).
+
+:- type solver_annotations(Var) == list(solver_annotation(Var)).
+
+:- type solver_annotation(Var)
+    --->    solver_annotation(list(Var)).
+
+:- type env(Var) == list({int, Var}).
+
+:- implementation.
+:- import_module exception.
+
+:- pred interpret(Solver::in) is det <= flatzinc_solver(Solver, Var).
+
+interpret(Solver) :-
+    interpret_2(Solver, satisfy, [], []).
+
+:- pragma inline(interpret_2/4).
+:- pred interpret_2(Solver::in, solve_spec(Var)::ia,
+    solver_annotations(Var)::ia,
+    list(Var)::ia) is det <= flatzinc_solver(Solver, Var).
+
+interpret_2(Solver, SolveSpec, SolverAnns, AllVars) :-
+    promise_pure
+    ( if
+        promise_equivalent_solutions [SolveSpec, SolverAnns, AllVars] (
+            solve_for_vars(Solver, SolveSpec, SolverAnns, AllVars)
+        )
+      then
+        true
+      else
+        throw("")
+    ).

--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------



More information about the reviews mailing list