[m-rev.] for review: Conform to memory alignment requirements on doubles.

Peter Wang novalazy at gmail.com
Mon Oct 7 15:45:49 AEDT 2013


If desired, I could try doing the nondet stack change mentioned below.

Also, note that if we reorder constructor arguments then floats can be
placed so they won't appear at unaligned offsets within a cell.

---

Conform to memory alignment requirements on doubles.

On some 32-bit architectures, we were violating memory alignment
requirements for double-precision floats, in cell fields and on det and
nondet stacks.  Bug #299.

We now only take the address of a double field when it occurs on an
aligned memory address, i.e. when it starts at an even word offset from
the start of the cell (this assumption is incompatible with term-size
profiling which adds a hidden word before the start of the cell).

For the det stack, we can round up allocations to keep the stack pointer
double-aligned, then allocate slots for doubles at even word offsets
from the stack pointer.

It would be trickier for the nondet stack.  Multiple frame types exist
on the nondet stack, and the different frame types are identified by
their sizes: 3-word and 4-word temporary frames, and 5/6+ word ordinary
frames. Rather than rounding up frame sizes to even numbers of words,
we would probably want to dynamically pad ordinary frame allocations,
such that any doubles in the frame will be at aligned addresses.

However, in this change, we simply store box floats on the nondet stack.

compiler/globals.m:
	Add predicate which returns whether double-width floats
	should be stored on the det stack.

compiler/handle_options.m:
	Disable double-word fields in term-size profiling grades.

compiler/code_info.m:
	Add a predicate to round up det stack frame sizes.

	Remember det_stack_float_width in exprn_opts.

compiler/hlds_llds.m:
compiler/llds.m:
compiler/stack_layout.m:
	Delete the possibility of double-width slots on the nondet
	stack.

	Remember det_stack_float_width in exprn_opts.

compiler/llds_out_data.m:
	Add wrapper macro `MR_dword_ptr' when taking the address of a
	double.

	Only take the address of doubles when aligned.

compiler/llds_out_instr.m:
compiler/llds_out_util.m:
	Only assign a double field in a single C statement when it is
	aligned.

	Assert that the stack pointer is incremented by an even number,
	if necessary.

compiler/mlds_to_c.m:
	Only take the address of doubles when aligned.

compiler/middle_rec.m:
compiler/proc_gen.m:
	Round up det stack frame allocations to even numbers of words
	when necessary.

compiler/stack_alloc.m:
	Add padding as required so that double-word variables will
	be allocated at even-word offsets from the stack pointer.

compiler/opt_debug.m:
compiler/par_conj_gen.m:
	Conform to changes.

runtime/mercury_conf_param.h:
runtime/mercury_float.h:
	Add macro `MR_dword_ptr' to be wrapped around instances where
	the address of a double is taken. When `MR_DEBUG_DWORD_ALIGNMENT'
	is defined (and using gcc or clang) the address is checked to be
	properly aligned.  Almost all our development is done on x86 or
	x86-64 architecture which do not have strict memory alignment
	requirements, making violations hard to check otherwise.

tests/debugger/nondet_stack.exp5:
	Add new expected output. This is the same as nondet_stack.exp
	except that det stack frames have been rounded up.

diff --git a/compiler/code_info.m b/compiler/code_info.m
index 59f8eee..19b5398 100644
--- a/compiler/code_info.m
+++ b/compiler/code_info.m
@@ -689,6 +689,14 @@ init_exprn_opts(Globals) = ExprnOpts :-
         OptFloatRegs = no,
         UseFloatRegs = do_not_use_float_registers
     ),
+    double_width_floats_on_det_stack(Globals, FloatDwords),
+    (
+        FloatDwords = yes,
+        DetStackFloatWidth = double_width
+    ;
+        FloatDwords = no,
+        DetStackFloatWidth = single_width
+    ),
     globals.lookup_bool_option(Globals, static_ground_floats, OptSGFloat),
     (
         OptSGFloat = yes,
@@ -706,8 +714,8 @@ init_exprn_opts(Globals) = ExprnOpts :-
         OptStaticCodeAddr = no,
         StaticCodeAddrs = do_not_have_static_code_addresses
     ),
-    ExprnOpts = exprn_opts(NLG, ASM, UBF, UseFloatRegs, SGCell, SGFloat,
-        StaticCodeAddrs).
+    ExprnOpts = exprn_opts(NLG, ASM, UBF, UseFloatRegs, DetStackFloatWidth,
+        SGCell, SGFloat, StaticCodeAddrs).
 
 :- pred init_maybe_trace_info(trace_level::in, globals::in,
     module_info::in, pred_info::in, proc_info::in, trace_slot_info::out,
@@ -4101,7 +4109,7 @@ record_highest_used_reg(_, AbsLocn, !HighestUsedRegR, !HighestUsedRegF) :-
     ;
         AbsLocn = abs_parent_stackvar(_, _)
     ;
-        AbsLocn = abs_framevar(_, _)
+        AbsLocn = abs_framevar(_)
     ).
 
 acquire_reg(Type, Lval, !CI) :-
@@ -4457,11 +4465,16 @@ generate_resume_layout(Label, ResumeMap, !CI) :-
 :- interface.
 
     % Returns the total stackslot count, but not including space for
-    % succip. This total can change in the future if this call is
-    % followed by further allocations of temp slots.
+    % succip, and without padding for alignment. This total can change in the
+    % future if this call is followed by further allocations of temp slots.
     %
 :- pred get_total_stackslot_count(code_info::in, int::out) is det.
 
+    % If necessary, round up a det stack frame allocation so that the stack
+    % pointer remains on an even word boundary.
+    %
+:- func round_det_stack_frame_size(code_info, int) = int.
+
     % If a stack slot is persistent, then the stack slot is not implicitly
     % released when the code generator resets its location-dependent state,
     % usually when entering the next arm of a disjunction, switch, etc.
@@ -4725,6 +4738,17 @@ get_total_stackslot_count(CI, NumSlots) :-
     get_max_temp_slot_count(CI, SlotsForTemps),
     NumSlots = SlotsForVars + SlotsForTemps.
 
+round_det_stack_frame_size(CI, NumSlots) = NumSlotsRoundup :-
+    (
+        odd(NumSlots),
+        get_exprn_opts(CI, ExprnOpts),
+        get_det_stack_float_width(ExprnOpts) = double_width
+    ->
+        NumSlotsRoundup = NumSlots + 1
+    ;
+        NumSlotsRoundup = NumSlots
+    ).
+
 :- pred max_var_slot(stack_slots::in, int::out) is det.
 
 max_var_slot(StackSlots, SlotCount) :-
@@ -4740,7 +4764,8 @@ max_var_slot_2([L | Ls], !Max) :-
     ;
         L = parent_det_slot(N, Width)
     ;
-        L = nondet_slot(N, Width)
+        L = nondet_slot(N),
+        Width = single_width
     ),
     (
         Width = single_width,
diff --git a/compiler/globals.m b/compiler/globals.m
index 723942b..4a1e6aa 100644
--- a/compiler/globals.m
+++ b/compiler/globals.m
@@ -315,6 +315,10 @@
 
 :- pred get_any_intermod(globals::in, bool::out) is det.
 
+    % Check if we may store double-width floats on the det stack.
+    %
+:- pred double_width_floats_on_det_stack(globals::in, bool::out) is det.
+
 %-----------------------------------------------------------------------------%
 
 :- pred globals_init_mutables(globals::in, io::di, io::uo) is det.
@@ -796,6 +800,23 @@ get_any_intermod(Globals, AnyIntermod) :-
     lookup_bool_option(Globals, intermodule_analysis, IntermodAnalysis),
     AnyIntermod = bool.or(IntermodOpt, IntermodAnalysis).
 
+double_width_floats_on_det_stack(Globals, FloatDwords) :-
+    globals.lookup_int_option(Globals, bits_per_word, TargetWordBits),
+    globals.lookup_bool_option(Globals, single_prec_float, SinglePrecFloat),
+    ( TargetWordBits = 64 ->
+        FloatDwords = no
+    ; TargetWordBits = 32 ->
+        (
+            SinglePrecFloat = yes,
+            FloatDwords = no
+        ;
+            SinglePrecFloat = no,
+            FloatDwords = yes
+        )
+    ;
+        unexpected($module, $pred, "bits_per_word not 32 or 64")
+    ).
+
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
 
diff --git a/compiler/handle_options.m b/compiler/handle_options.m
index 5f80ae1..4761e7d 100644
--- a/compiler/handle_options.m
+++ b/compiler/handle_options.m
@@ -1705,6 +1705,10 @@ convert_options_to_globals(OptionTable0, Target, GC_Method, TagsMethod0,
     ->
         globals.set_option(optimize_constructor_last_call, bool(no),
             !Globals),
+        % Term size profiling breaks the assumption that even word offsets from
+        % the start of the cell are double-word aligned memory addresses.
+        globals.set_option(allow_double_word_fields, bool(no),
+            !Globals),
         (
             HighLevelCode = yes,
             add_error("term size profiling is incompatible "
diff --git a/compiler/hlds_llds.m b/compiler/hlds_llds.m
index a30843d..7f8f6e6 100644
--- a/compiler/hlds_llds.m
+++ b/compiler/hlds_llds.m
@@ -39,7 +39,7 @@
 :- type stack_slot
     --->    det_slot(int, stack_slot_width)
     ;       parent_det_slot(int, stack_slot_width)
-    ;       nondet_slot(int, stack_slot_width).
+    ;       nondet_slot(int).
 
 :- type stack_slot_width
     --->    single_width
@@ -56,7 +56,7 @@
     ;       abs_reg(reg_type, int)
     ;       abs_stackvar(int, stack_slot_width)
     ;       abs_parent_stackvar(int, stack_slot_width)
-    ;       abs_framevar(int, stack_slot_width).
+    ;       abs_framevar(int).
 
 :- type abs_follow_vars_map ==  map(prog_var, abs_locn).
 
@@ -332,7 +332,8 @@ explain_stack_slots_2([Var - Slot | Rest], VarSet, !Explanation) :-
         Slot = parent_det_slot(SlotNum, Width),
         StackStr = "parent_sv"
     ;
-        Slot = nondet_slot(SlotNum, Width),
+        Slot = nondet_slot(SlotNum),
+        Width = single_width,
         StackStr = "fv"
     ),
     int_to_string(SlotNum, SlotStr),
@@ -793,7 +794,8 @@ stack_slot_num(StackSlot) = N :-
     ;
         StackSlot = parent_det_slot(N, Width)
     ;
-        StackSlot = nondet_slot(N, Width)
+        StackSlot = nondet_slot(N),
+        Width = single_width
     ),
     (
         Width = single_width
@@ -810,8 +812,8 @@ stack_slot_to_abs_locn(StackSlot) = AbsLocn :-
         StackSlot = parent_det_slot(N, Width),
         AbsLocn = abs_parent_stackvar(N, Width)
     ;
-        StackSlot = nondet_slot(N, Width),
-        AbsLocn = abs_framevar(N, Width)
+        StackSlot = nondet_slot(N),
+        AbsLocn = abs_framevar(N)
     ).
 
 key_stack_slot_to_abs_locn(_, Slot) =
@@ -839,9 +841,9 @@ abs_locn_to_string(Locn, Str, MaybeWidth) :-
         Str = "parent_stackvar" ++ int_to_string(N),
         MaybeWidth = stack_slot_width_to_string(Width)
     ;
-        Locn = abs_framevar(N, Width),
+        Locn = abs_framevar(N),
         Str = "framevar" ++ int_to_string(N),
-        MaybeWidth = stack_slot_width_to_string(Width)
+        MaybeWidth = no
     ).
 
 :- func stack_slot_width_to_string(stack_slot_width) = maybe(string).
diff --git a/compiler/llds.m b/compiler/llds.m
index 6026600..4a9c0c2 100644
--- a/compiler/llds.m
+++ b/compiler/llds.m
@@ -1102,10 +1102,14 @@
             % numbers start at 1.
 
     ;       double_stackvar(double_stack_type, int)
-            % Two consecutive stack slots for storing a double-precision float:
+            % Two consecutive stack slots for storing a double-precision float.
+            % The number is the offset relative to one of the stack pointers
+            % and represents the lower-numbered of two consecutive slots.
+            % As our stacks grow downward, the higher-number slot has the
+            % lower address, and must be aligned for the target architecture.
+            %
             % - stackvar(Slot), stackvar(Slot + 1)
             % - parent_stackvar(Slot), parent_stackvar(Slot + 1)
-            % - framevar(Slot), framevar(Slot + 1)
 
     ;       succip_slot(rval)
             % The succip slot of the specified nondet stack frame; holds the
@@ -1160,8 +1164,7 @@
 
 :- type double_stack_type
     --->    double_stackvar
-    ;       double_parent_stackvar
-    ;       double_framevar.
+    ;       double_parent_stackvar.
 
     % An rval is an expression that represents a value.
     %
@@ -1498,6 +1501,7 @@
                 asm_labels              :: have_asm_labels,
                 unboxed_floats          :: have_unboxed_floats,
                 float_registers         :: use_float_registers,
+                det_stack_float_width   :: stack_slot_width,
                 static_ground_cells     :: have_static_ground_cells,
                 static_ground_floats    :: have_static_ground_floats,
                 static_code_addresses   :: have_static_code_addresses
@@ -1507,6 +1511,7 @@
 :- func get_asm_labels(exprn_opts) = have_asm_labels.
 :- func get_unboxed_floats(exprn_opts) = have_unboxed_floats.
 :- func get_float_registers(exprn_opts) = use_float_registers.
+:- func get_det_stack_float_width(exprn_opts) = stack_slot_width.
 :- func get_static_ground_cells(exprn_opts) = have_static_ground_cells.
 :- func get_static_ground_floats(exprn_opts) = have_static_ground_floats.
 :- func get_static_code_addresses(exprn_opts) = have_static_code_addresses.
@@ -1569,14 +1574,8 @@ stack_slot_to_lval(Slot) = Lval :-
             Lval = double_stackvar(double_parent_stackvar, N)
         )
     ;
-        Slot = nondet_slot(N, Width),
-        (
-            Width = single_width,
-            Lval = framevar(N)
-        ;
-            Width = double_width,
-            Lval = double_stackvar(double_framevar, N)
-        )
+        Slot = nondet_slot(N),
+        Lval = framevar(N)
     ).
 
 key_stack_slot_to_lval(_, Slot) =
@@ -1588,8 +1587,8 @@ abs_locn_to_lval_or_any_reg(abs_stackvar(N, Width)) =
     loa_lval(stack_slot_to_lval(det_slot(N, Width))).
 abs_locn_to_lval_or_any_reg(abs_parent_stackvar(N, Width)) =
     loa_lval(stack_slot_to_lval(parent_det_slot(N, Width))).
-abs_locn_to_lval_or_any_reg(abs_framevar(N, Width)) =
-    loa_lval(stack_slot_to_lval(nondet_slot(N, Width))).
+abs_locn_to_lval_or_any_reg(abs_framevar(N)) =
+    loa_lval(stack_slot_to_lval(nondet_slot(N))).
 
 abs_locn_to_lval(any_reg) = _ :-
     unexpected($module, $pred, "any_reg").
@@ -1598,8 +1597,8 @@ abs_locn_to_lval(abs_stackvar(N, Width)) =
     stack_slot_to_lval(det_slot(N, Width)).
 abs_locn_to_lval(abs_parent_stackvar(N, Width)) =
     stack_slot_to_lval(parent_det_slot(N, Width)).
-abs_locn_to_lval(abs_framevar(N, Width)) =
-    stack_slot_to_lval(nondet_slot(N, Width)).
+abs_locn_to_lval(abs_framevar(N)) =
+    stack_slot_to_lval(nondet_slot(N)).
 
 key_abs_locn_to_lval(_, AbsLocn) =
     abs_locn_to_lval(AbsLocn).
@@ -1771,6 +1770,7 @@ get_asm_labels(ExprnOpts) = ExprnOpts ^ asm_labels.
 get_static_ground_cells(ExprnOpts) = ExprnOpts ^ static_ground_cells.
 get_unboxed_floats(ExprnOpts) = ExprnOpts ^ unboxed_floats.
 get_float_registers(ExprnOpts) = ExprnOpts ^ float_registers.
+get_det_stack_float_width(ExprnOpts) = ExprnOpts ^ det_stack_float_width.
 get_static_ground_floats(ExprnOpts) = ExprnOpts ^ static_ground_floats.
 get_static_code_addresses(ExprnOpts) = ExprnOpts ^ static_code_addresses.
 
diff --git a/compiler/llds_out_data.m b/compiler/llds_out_data.m
index 07b31c3..76c9964 100644
--- a/compiler/llds_out_data.m
+++ b/compiler/llds_out_data.m
@@ -523,20 +523,18 @@ output_lval_as_word(Info, Lval, !IO) :-
     double_stack_type::in, int::in, io::di, io::uo) is det.
 
 output_double_stackvar_ptr(Info, StackType, SlotNum, !IO) :-
-    % We take the address of the second slot because our stacks grow downwards,
-    % i.e. &MR_sv(n + 1) < &MR_sv(n).
+    % The higher-numbered slot has the lower address because our stacks grow
+    % downwards.
     (
         StackType = double_stackvar,
         Lval = stackvar(SlotNum + 1)
     ;
         StackType = double_parent_stackvar,
         Lval = parent_stackvar(SlotNum + 1)
-    ;
-        StackType = double_framevar,
-        Lval = framevar(SlotNum + 1)
     ),
-    io.write_string("&", !IO),
-    output_lval(Info, Lval, !IO).
+    io.write_string("MR_dword_ptr(&(", !IO),
+    output_lval(Info, Lval, !IO),
+    io.write_string("))", !IO).
 
     % llds_types_match(DesiredType, ActualType) is true iff
     % a value of type ActualType can be used as a value of
@@ -602,9 +600,6 @@ lval_to_string(double_stackvar(Type, N)) = String :-
     ;
         Type = double_parent_stackvar,
         Macro = "MR_parent_sv"
-    ;
-        Type = double_framevar,
-        Macro = "MR_fv"
     ),
     string.format("%s(%d,%d)", [s(Macro), i(N), i(N + 1)], String).
 
@@ -984,12 +979,19 @@ output_rval(Info, Rval, !IO) :-
                 output_rval_as_type(Info, SubRvalB, lt_integer, !IO),
                 io.write_string(")", !IO)
             ;
-                Op = float_from_dword,
-                consecutive_field_offsets(SubRvalA, SubRvalB, MemRef)
+                Op = float_from_dword
             ->
-                io.write_string("MR_float_from_dword_ptr(", !IO),
-                output_rval(Info, mem_addr(MemRef), !IO),
-                io.write_string(")", !IO)
+                ( is_aligned_dword_ptr(SubRvalA, SubRvalB, MemRef) ->
+                    io.write_string("MR_float_from_dword_ptr(", !IO),
+                    output_rval(Info, mem_addr(MemRef), !IO),
+                    io.write_string(")", !IO)
+                ;
+                    io.write_string("MR_float_from_dword(", !IO),
+                    output_rval(Info, SubRvalA, !IO),
+                    io.write_string(", ", !IO),
+                    output_rval(Info, SubRvalB, !IO),
+                    io.write_string(")", !IO)
+                )
             ;
                 sorry($module, $pred, "unknown float_macro_binop")
             )
@@ -1102,23 +1104,6 @@ output_rval(Info, Rval, !IO) :-
         )
     ).
 
-:- pred consecutive_field_offsets(rval::in, rval::in, mem_ref::out) is semidet.
-
-consecutive_field_offsets(lval(LvalA), lval(LvalB), MemRef) :-
-    (
-        LvalA = field(MaybeTag, Address, const(llconst_int(N))),
-        LvalB = field(MaybeTag, Address, const(llconst_int(N + 1))),
-        MemRef = heap_ref(Address, MaybeTag, const(llconst_int(N)))
-    ;
-        LvalA = stackvar(N),
-        LvalB = stackvar(N + 1),
-        MemRef = stackvar_ref(const(llconst_int(N)))
-    ;
-        LvalA = framevar(N),
-        LvalB = framevar(N + 1),
-        MemRef = framevar_ref(const(llconst_int(N)))
-    ).
-
 :- pred output_rval_const(llds_out_info::in, rval_const::in,
     io::di, io::uo) is det.
 
@@ -1365,6 +1350,25 @@ output_float_rval(Info, Rval, IsPtr, !IO) :-
         io.write_string(")", !IO)
     ).
 
+:- pred is_aligned_dword_ptr(rval::in, rval::in, mem_ref::out) is semidet.
+
+is_aligned_dword_ptr(lval(LvalA), lval(LvalB), MemRef) :-
+    (
+        LvalA = field(MaybeTag, Address, const(llconst_int(N))),
+        LvalB = field(MaybeTag, Address, const(llconst_int(N + 1))),
+        % Only output an aligned memory reference to a double-word,
+        % i.e. fields at even word offsets from the start of the cell.
+        int.even(N),
+        MemRef = heap_ref(Address, MaybeTag, const(llconst_int(N)))
+    ;
+        LvalA = stackvar(N),
+        LvalB = stackvar(N + 1),
+        % Double-width variables on the det stack should have been aligned
+        % by the allocator. In a downwards-growing stack the higher slot
+        % number has the lower address.
+        MemRef = stackvar_ref(const(llconst_int(N + 1)))
+    ).
+
 output_test_rval(Info, Test, !IO) :-
     (
         is_int_cmp(Test, Left, RightConst, OpStr, _)
diff --git a/compiler/llds_out_instr.m b/compiler/llds_out_instr.m
index 7a78280..5abf77d 100644
--- a/compiler/llds_out_instr.m
+++ b/compiler/llds_out_instr.m
@@ -291,7 +291,7 @@ output_instruction_list(Info, [Instr | Instrs], ProfInfo, WhileSet,
     ;
         Instrs = [Instr1 | Instrs1],
         Instr1 = llds_instr(Uinstr1, _),
-        is_float_dword_assignment(Uinstr, Uinstr1, Lval, Rval)
+        is_aligned_float_dword_assignment(Uinstr, Uinstr1, Lval, Rval)
     ->
         output_float_dword_assignment(Info, Lval, Rval, !IO),
         AfterLayoutLabel = not_after_layout_label,
@@ -393,24 +393,26 @@ output_instruction_list_while_block(Info, [Instr | Instrs], Label, ProfInfo,
             ProfInfo, !IO)
     ).
 
-:- pred is_float_dword_assignment(instr::in, instr::in, lval::out, rval::out)
-    is semidet.
+:- pred is_aligned_float_dword_assignment(instr::in, instr::in, lval::out,
+    rval::out) is semidet.
 
-is_float_dword_assignment(InstrA, InstrB, LvalA, Rval) :-
+is_aligned_float_dword_assignment(InstrA, InstrB, LvalA, Rval) :-
     InstrA = assign(LvalA, RvalA),
     InstrB = assign(LvalB, RvalB),
     RvalA = binop(float_word_bits, Rval, const(llconst_int(0))),
     RvalB = binop(float_word_bits, Rval, const(llconst_int(1))),
     LvalA = field(MaybeTag, Address, const(llconst_int(Offset))),
-    LvalB = field(MaybeTag, Address, const(llconst_int(Offset + 1))).
+    LvalB = field(MaybeTag, Address, const(llconst_int(Offset + 1))),
+    % Only output an aligned memory reference to a double-word,
+    % i.e. fields at even word offsets from the start of the cell.
+    int.even(Offset).
 
 :- pred output_float_dword_assignment(llds_out_info::in, lval::in, rval::in,
     io::di, io::uo) is det.
 
 output_float_dword_assignment(Info, Lval, Rval, !IO) :-
     % This looks neater than two statements to assign a double precision float,
-    % but makes no real difference to the code generated by gcc. It might
-    % improve the code generated by other C compilers.
+    % but can only be if the address is aligned for the target architecture.
 
     io.write_string("\t* (MR_Float *) &(", !IO),
     output_lval_for_assign(Info, Lval, Type, !IO),
@@ -523,14 +525,11 @@ output_instruction(Info, Instr, ProfInfo, !IO) :-
             not_after_layout_label, !IO),
         output_block_end(!IO)
     ;
-        Instr = assign(Lval, Rval),
-        io.write_string("\t", !IO),
-        output_lval_for_assign(Info, Lval, Type, !IO),
-        io.write_string(" = ", !IO),
-        output_rval_as_type(Info, Rval, Type, !IO),
-        io.write_string(";\n", !IO)
-    ;
-        Instr = keep_assign(Lval, Rval),
+        (
+            Instr = assign(Lval, Rval)
+        ;
+            Instr = keep_assign(Lval, Rval)
+        ),
         io.write_string("\t", !IO),
         output_lval_for_assign(Info, Lval, Type, !IO),
         io.write_string(" = ", !IO),
@@ -844,6 +843,13 @@ output_instruction(Info, Instr, ProfInfo, !IO) :-
         io.write_string(");\n", !IO)
     ;
         Instr = incr_sp(N, _Msg, Kind),
+        DwordAlignment = Info ^ lout_det_stack_dword_alignment,
+        (
+            DwordAlignment = yes,
+            expect(int.even(N), $module, $pred, "odd sp increment")
+        ;
+            DwordAlignment = no
+        ),
         (
             Kind = stack_incr_leaf,
             ( N < max_leaf_stack_frame_size ->
diff --git a/compiler/llds_out_util.m b/compiler/llds_out_util.m
index 471685a..2d2e5f1 100644
--- a/compiler/llds_out_util.m
+++ b/compiler/llds_out_util.m
@@ -51,6 +51,7 @@
                 lout_profile_memory             :: bool,
                 lout_profile_deep               :: bool,
                 lout_unboxed_float              :: bool,
+                lout_det_stack_dword_alignment  :: bool,
                 lout_static_ground_floats       :: bool,
                 lout_use_macro_for_redo_fail    :: bool,
                 lout_trace_level                :: trace_level,
@@ -127,6 +128,7 @@ init_llds_out_info(ModuleName, Globals,
     globals.lookup_bool_option(Globals, profile_memory, ProfileMemory),
     globals.lookup_bool_option(Globals, profile_deep, ProfileDeep),
     globals.lookup_bool_option(Globals, unboxed_float, UnboxedFloat),
+    double_width_floats_on_det_stack(Globals, DetStackDwordAligment),
     globals.lookup_bool_option(Globals, static_ground_floats,
         StaticGroundFloats),
     globals.lookup_bool_option(Globals, use_macro_for_redo_fail,
@@ -138,8 +140,8 @@ init_llds_out_info(ModuleName, Globals,
         AutoComments, LineNumbers,
         EmitCLoops, GenerateBytecode, LocalThreadEngineBase,
         ProfileCalls, ProfileTime, ProfileMemory, ProfileDeep,
-        UnboxedFloat, StaticGroundFloats, UseMacroForRedoFail,
-        TraceLevel, Globals).
+        UnboxedFloat, DetStackDwordAligment, StaticGroundFloats,
+        UseMacroForRedoFail, TraceLevel, Globals).
 
 output_set_line_num(Info, Context, !IO) :-
     LineNumbers = Info ^ lout_line_numbers,
diff --git a/compiler/middle_rec.m b/compiler/middle_rec.m
index 81bfd7b..88a5881 100644
--- a/compiler/middle_rec.m
+++ b/compiler/middle_rec.m
@@ -298,7 +298,8 @@ middle_rec_generate_switch(Var, BaseConsId, Base, Recursive, SwitchGoalInfo,
 
     get_next_label(Loop1Label, !CI),
     get_next_label(Loop2Label, !CI),
-    get_total_stackslot_count(!.CI, FrameSize),
+    get_total_stackslot_count(!.CI, FrameSize0),
+    FrameSize = round_det_stack_frame_size(!.CI, FrameSize0),
 
     generate_downloop_test(EntryTestInstrs, Loop1Label, Loop1Test),
 
diff --git a/compiler/mlds_to_c.m b/compiler/mlds_to_c.m
index bb02cd2..8fa8d8a 100644
--- a/compiler/mlds_to_c.m
+++ b/compiler/mlds_to_c.m
@@ -1575,7 +1575,7 @@ mlds_output_scalar_cell_group_struct_field(Opts, Indent, FieldType,
         Num, Num + 1, !IO) :-
     mlds_indent(Indent, !IO),
     ( FieldType = mlds_native_float_type ->
-        % Ensure float structure members are word-aligned.
+        % Ensure float structure members are word-aligned (not double-aligned).
         io.write_string("MR_Float_Aligned", !IO)
     ;
         mlds_output_type_prefix(Opts, FieldType, !IO)
@@ -4507,12 +4507,11 @@ mlds_output_binop(Opts, Op, X, Y, !IO) :-
         ),
         (
             Op = float_from_dword,
-            consecutive_field_offsets(X, Y)
+            is_aligned_dword_field(X, Y, PtrRval)
         ->
             % gcc produces faster code in this case.
-            io.write_string("MR_float_from_dword_ptr", !IO),
-            io.write_string("(&(", !IO),
-            mlds_output_rval(Opts, X, !IO),
+            io.write_string("MR_float_from_dword_ptr(MR_dword_ptr(", !IO),
+            mlds_output_rval(Opts, PtrRval, !IO),
             io.write_string("))", !IO)
         ;
             io.write_string(OpStr, !IO),
@@ -4524,14 +4523,6 @@ mlds_output_binop(Opts, Op, X, Y, !IO) :-
         )
     ).
 
-:- pred consecutive_field_offsets(mlds_rval::in, mlds_rval::in) is semidet.
-
-consecutive_field_offsets(X, Y) :-
-    X = ml_lval(ml_field(Tag, Addr, FieldIdX, Type, PtrType)),
-    Y = ml_lval(ml_field(Tag, Addr, FieldIdY, Type, PtrType)),
-    FieldIdX = ml_field_offset(ml_const(mlconst_int(Offset))),
-    FieldIdY = ml_field_offset(ml_const(mlconst_int(Offset + 1))).
-
 :- pred mlds_output_rval_const(mlds_to_c_opts::in, mlds_rval_const::in,
     io::di, io::uo) is det.
 
@@ -4626,6 +4617,16 @@ mlds_output_float_bits(Opts, Float, !IO) :-
     ),
     io.format("%s /* float-bits: %g */", [s(String), f(Float)], !IO).
 
+:- pred is_aligned_dword_field(mlds_rval::in, mlds_rval::in, mlds_rval::out)
+    is semidet.
+
+is_aligned_dword_field(X, Y, ml_mem_addr(Lval)) :-
+    X = ml_lval(ml_field(Tag, Addr, FieldIdX, Type, PtrType) @ Lval),
+    Y = ml_lval(ml_field(Tag, Addr, FieldIdY, Type, PtrType)),
+    FieldIdX = ml_field_offset(ml_const(mlconst_int(Offset))),
+    FieldIdY = ml_field_offset(ml_const(mlconst_int(Offset + 1))),
+    int.even(Offset).
+
 %-----------------------------------------------------------------------------%
 
 :- pred mlds_output_tag(mlds_tag::in, io::di, io::uo) is det.
diff --git a/compiler/opt_debug.m b/compiler/opt_debug.m
index fffda73..426e296 100644
--- a/compiler/opt_debug.m
+++ b/compiler/opt_debug.m
@@ -282,9 +282,6 @@ dump_lval(_, double_stackvar(Type, N)) = Str :-
     ;
         Type = double_parent_stackvar,
         Macro = "parent_sv"
-    ;
-        Type= double_framevar,
-        Macro = "fv"
     ),
     string.format("%s%d,%s%d", [s(Macro), i(N), s(Macro), i(N + 1)], Str).
 dump_lval(_, succip) = "succip".
diff --git a/compiler/par_conj_gen.m b/compiler/par_conj_gen.m
index 21f5a5e..af8cd13 100644
--- a/compiler/par_conj_gen.m
+++ b/compiler/par_conj_gen.m
@@ -535,9 +535,6 @@ replace_stack_vars_by_parent_sv_lval(Lval0, Lval, !Acc) :-
         ;
             Type = double_parent_stackvar,
             Lval = Lval0
-        ;
-            Type = double_framevar,
-            Lval = Lval0
         )
     ;
         ( Lval0 = reg(_Type, _RegNum)
diff --git a/compiler/proc_gen.m b/compiler/proc_gen.m
index 1424224..71144d8 100644
--- a/compiler/proc_gen.m
+++ b/compiler/proc_gen.m
@@ -916,7 +916,7 @@ generate_entry(CI, CodeModel, Goal, OutsideResumePoint, FrameInfo,
         % Do we need to use a general slot for storing succip?
         CodeModel \= model_non
     ->
-        SuccipSlot = MainSlots + 1,
+        SuccipSlot = maybe_round_frame_size(CI, CodeModel, MainSlots + 1),
         SaveSuccipCode = singleton(
             llds_instr(assign(stackvar(SuccipSlot), lval(succip)),
                 "Save the success ip")
@@ -925,7 +925,7 @@ generate_entry(CI, CodeModel, Goal, OutsideResumePoint, FrameInfo,
         MaybeSuccipSlot = yes(SuccipSlot)
     ;
         SaveSuccipCode = empty,
-        TotalSlots = MainSlots,
+        TotalSlots = maybe_round_frame_size(CI, CodeModel, MainSlots),
         MaybeSuccipSlot = no
     ),
     get_maybe_trace_info(CI, MaybeTraceInfo),
@@ -976,6 +976,19 @@ generate_entry(CI, CodeModel, Goal, OutsideResumePoint, FrameInfo,
     EntryCode = StartComment ++ LabelCode ++ AllocCode ++
         SaveSuccipCode ++ TraceFillCode ++ EndComment.
 
+:- func maybe_round_frame_size(code_info, code_model, int) = int.
+
+maybe_round_frame_size(CI, CodeModel, NumSlots0) = NumSlots :-
+    (
+        ( CodeModel = model_det
+        ; CodeModel = model_semi
+        ),
+        NumSlots = round_det_stack_frame_size(CI, NumSlots0)
+    ;
+        CodeModel = model_non,
+        NumSlots = NumSlots0
+    ).
+
 %---------------------------------------------------------------------------%
 
     % Generate the success epilogue for a procedure.
diff --git a/compiler/stack_alloc.m b/compiler/stack_alloc.m
index 6d83390..3e4949e 100644
--- a/compiler/stack_alloc.m
+++ b/compiler/stack_alloc.m
@@ -111,33 +111,12 @@ allocate_stack_slots_in_proc(ModuleInfo, proc(PredId, ProcId), !ProcInfo) :-
 
     CodeModel = proc_info_interface_code_model(!.ProcInfo),
     MainStack = code_model_to_main_stack(CodeModel),
-    FloatWidth = get_float_width(Globals),
-    allocate_stack_slots(ColourList, MainStack, VarTypes, FloatWidth,
+    allocate_stack_slots(ColourList, Globals, MainStack, VarTypes,
         NumReservedSlots, MaybeReservedVarInfo, StackSlots1),
     allocate_dummy_stack_slots(DummyVars, MainStack, -1,
         StackSlots1, StackSlots),
     proc_info_set_stack_slots(StackSlots, !ProcInfo).
 
-:- func get_float_width(globals) = stack_slot_width.
-
-get_float_width(Globals) = FloatWidth :-
-    globals.lookup_int_option(Globals, bits_per_word, TargetWordBits),
-    ( TargetWordBits = 64 ->
-        FloatWidth = single_width
-    ; TargetWordBits = 32 ->
-        globals.lookup_bool_option(Globals, single_prec_float,
-            SinglePrecFloat),
-        (
-            SinglePrecFloat = yes,
-            FloatWidth = single_width
-        ;
-            SinglePrecFloat = no,
-            FloatWidth = double_width
-        )
-    ;
-        unexpected($module, $pred, "bits_per_word not 32 or 64")
-    ).
-
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
 
@@ -230,33 +209,31 @@ var_is_not_dummy(DummyVarArray, Var) :-
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
 
-:- pred allocate_stack_slots(list(set_of_progvar)::in, main_stack::in,
-    vartypes::in, stack_slot_width::in, int::in,
-    maybe(pair(prog_var, int))::in, stack_slots::out) is det.
+:- pred allocate_stack_slots(list(set_of_progvar)::in, globals::in,
+    main_stack::in, vartypes::in, int::in, maybe(pair(prog_var, int))::in,
+    stack_slots::out) is det.
 
-allocate_stack_slots(ColourList, MainStack, VarTypes, FloatWidth,
+allocate_stack_slots(ColourList, Globals, MainStack, VarTypes,
         NumReservedSlots, MaybeReservedVarInfo, StackSlots) :-
     % The reserved slots are referred to by fixed number
     % (e.g. framevar(1)) in trace.setup.
     FirstVarSlot = NumReservedSlots + 1,
-    allocate_stack_slots_2(ColourList, MainStack, VarTypes, FloatWidth,
+    allocate_stack_slots_2(ColourList, Globals, MainStack, VarTypes,
         MaybeReservedVarInfo, FirstVarSlot, map.init, StackSlots).
 
-:- pred allocate_stack_slots_2(list(set_of_progvar)::in, main_stack::in,
-    vartypes::in, stack_slot_width::in, maybe(pair(prog_var, int))::in,
+:- pred allocate_stack_slots_2(list(set_of_progvar)::in, globals::in,
+    main_stack::in, vartypes::in, maybe(pair(prog_var, int))::in,
     int::in, stack_slots::in, stack_slots::out) is det.
 
 allocate_stack_slots_2([], _, _, _, _, _, !StackSlots).
-allocate_stack_slots_2([Vars | VarSets], MainStack, VarTypes, FloatWidth,
+allocate_stack_slots_2([Vars | VarSets], Globals, MainStack, VarTypes,
         MaybeReservedVarInfo, N0, !StackSlots) :-
-    (
-        FloatWidth = single_width,
-        SingleWidthVars = Vars,
-        DoubleWidthVars = set_of_var.init
-    ;
-        FloatWidth = double_width,
+    ( float_width_on_stack(Globals, MainStack) = double_width ->
         set_of_var.divide(var_is_float(VarTypes), Vars,
             DoubleWidthVars, SingleWidthVars)
+    ;
+        SingleWidthVars = Vars,
+        DoubleWidthVars = set_of_var.init
     ),
     ( set_of_var.is_non_empty(SingleWidthVars) ->
         allocate_stack_slots_3(SingleWidthVars, MainStack, single_width,
@@ -269,14 +246,53 @@ allocate_stack_slots_2([Vars | VarSets], MainStack, VarTypes, FloatWidth,
         % double-width vars. The code generator does not understand that
         % clobbering one of the pair of slots is equivalent to clobbering
         % both of them.
+        align_double_width_slots(N1, N2),
         allocate_stack_slots_3(DoubleWidthVars, MainStack, double_width,
-            MaybeReservedVarInfo, N1, N, !StackSlots)
+            MaybeReservedVarInfo, N2, N, !StackSlots)
     ;
         N = N1
     ),
-    allocate_stack_slots_2(VarSets, MainStack, VarTypes, FloatWidth,
+    allocate_stack_slots_2(VarSets, Globals, MainStack, VarTypes,
         MaybeReservedVarInfo, N, !StackSlots).
 
+:- func float_width_on_stack(globals, main_stack) = stack_slot_width.
+
+float_width_on_stack(Globals, Stack) = FloatWidth :-
+    % We only store unboxed double-width floats on the det stack.
+    % It would be possible to do on the nondet stack but we would probably
+    % need to pad the frame allocation at run time to ensure that any double
+    % variables in the frame will be at aligned memory addresses.
+    (
+        Stack = det_stack,
+        double_width_floats_on_det_stack(Globals, yes)
+    ->
+        FloatWidth = double_width
+    ;
+        FloatWidth = single_width
+    ).
+
+    % Conform to memory alignment requirements for double-word values.
+    % We maintain the invariant that the stack pointer is double-aligned.
+    % The first stack variable is numbered 1 so all odd-numbered stack slots
+    % are aligned. In a downwards-growing stack a higher slot number has a
+    % lower address. When allocating two consecutive slots, we therefore want
+    % the highered-numbered slot to be ODD. [N, N+1] shall be the next slots
+    % to be allocated, therefore N must be EVEN and N+1 must be ODD.
+    %
+:- pred align_double_width_slots(int::in, int::out) is det.
+
+align_double_width_slots(N0, N) :-
+    ( int.even(N0) ->
+        N = N0
+    ;
+        N = N0 + 1
+    ).
+
+:- pred var_is_float(vartypes::in, prog_var::in) is semidet.
+
+var_is_float(VarTypes, Var) :-
+    lookup_var_type(VarTypes, Var, float_type).
+
 :- pred allocate_stack_slots_3(set_of_progvar::in, main_stack::in,
     stack_slot_width::in, maybe(pair(prog_var, int))::in, int::in, int::out,
     stack_slots::in, stack_slots::out) is det.
@@ -292,28 +308,22 @@ allocate_stack_slots_3(Vars, MainStack, StackSlotWidth, MaybeReservedVarInfo,
         SlotNum = ResSlotNum
     ;
         SlotNum = !.N,
-        (
-            StackSlotWidth = single_width,
-            !:N = !.N + 1
-        ;
-            StackSlotWidth = double_width,
-            !:N = !.N + 2
-        )
+        next_slot(StackSlotWidth, !N)
     ),
     (
         MainStack = det_stack,
         Locn = det_slot(SlotNum, StackSlotWidth)
     ;
         MainStack = nondet_stack,
-        Locn = nondet_slot(SlotNum, StackSlotWidth)
+        Locn = nondet_slot(SlotNum)
     ),
     VarList = set_of_var.to_sorted_list(Vars),
     allocate_same_stack_slot(VarList, Locn, !StackSlots).
 
-:- pred var_is_float(vartypes::in, prog_var::in) is semidet.
+:- pred next_slot(stack_slot_width::in, int::in, int::out) is det.
 
-var_is_float(VarTypes, Var) :-
-    lookup_var_type(VarTypes, Var, float_type).
+next_slot(single_width, N, N + 1).
+next_slot(double_width, N, N + 2).
 
 :- pred allocate_same_stack_slot(list(prog_var)::in, stack_slot::in,
     stack_slots::in, stack_slots::out) is det.
@@ -344,7 +354,7 @@ allocate_dummy_stack_slots([Var | Vars], MainStack, N0, !StackSlots) :-
         Locn = det_slot(N0, single_width)
     ;
         MainStack = nondet_stack,
-        Locn = nondet_slot(N0, single_width)
+        Locn = nondet_slot(N0)
     ),
     allocate_same_stack_slot([Var], Locn, !StackSlots),
     allocate_dummy_stack_slots(Vars, MainStack, N0 - 1, !StackSlots).
diff --git a/compiler/stack_layout.m b/compiler/stack_layout.m
index ea36927..84830af 100644
--- a/compiler/stack_layout.m
+++ b/compiler/stack_layout.m
@@ -1697,8 +1697,6 @@ select_trace_return(LocnInfo) :-
         Lval = framevar(_)
     ;
         Lval = double_stackvar(double_stackvar, _)
-    ;
-        Lval = double_stackvar(double_framevar, _)
     ).
 
     % Given a list of layout_var_infos, put the ones that tracing can be
@@ -2269,9 +2267,6 @@ represent_lval(double_stackvar(StackType, Num), Word) :-
     ;
         StackType = double_parent_stackvar,
         make_tagged_word(lval_double_parent_stackvar, Num, Word)
-    ;
-        StackType = double_framevar,
-        make_tagged_word(lval_double_framevar, Num, Word)
     ).
 represent_lval(succip, Word) :-
     make_tagged_word(lval_succip, 0, Word).
@@ -2361,7 +2356,7 @@ locn_type_code(lval_sp,              11).
 locn_type_code(lval_parent_sp,       11).    % XXX placeholder only
 locn_type_code(lval_double_stackvar, 13).
 locn_type_code(lval_double_parent_stackvar, 13). % XXX placeholder only
-locn_type_code(lval_double_framevar, 14).
+locn_type_code(lval_double_framevar, 14).    % unused now
 locn_type_code(lval_indirect,        15).
 
     % This number of tag bits must be able to encode all values of
diff --git a/runtime/mercury_conf_param.h b/runtime/mercury_conf_param.h
index 9f4c14a..ba89750 100644
--- a/runtime/mercury_conf_param.h
+++ b/runtime/mercury_conf_param.h
@@ -433,6 +433,9 @@
 ** MR_STM_DEBUG
 **	Enables low-level debugging messages from the code that implements
 **	transactions used by software transactional memory.
+**
+** MR_DEBUG_DWORD_ALIGNMENT
+**	Enables runtime tests for misaligned double-word pointers.
 */
 
 #ifdef MR_DEEP_PROFILING_DETAIL_DEBUG
diff --git a/runtime/mercury_float.h b/runtime/mercury_float.h
index f9856f4..b302f80 100644
--- a/runtime/mercury_float.h
+++ b/runtime/mercury_float.h
@@ -113,6 +113,18 @@
     }
   #endif
 
+  #if defined(MR_DEBUG_DWORD_ALIGNMENT) && \
+	(defined(MR_GNUC) || defined(MR_CLANG))
+    #define MR_dword_ptr(ptr)                                               \
+      ({                                                                    \
+          MR_Word __addr = (MR_Word) (ptr);                                 \
+          assert((__addr % 8) == 0);                                        \
+          /* return */ (void *) __addr;                                     \
+      })
+  #else
+    #define MR_dword_ptr(ptr)   ((void *) (ptr))
+  #endif
+
   #define MR_float_from_dword_ptr(ptr)                                      \
         (((union MR_Float_Dword *) (ptr))->f)
 
diff --git a/tests/debugger/nondet_stack.exp5 b/tests/debugger/nondet_stack.exp5
new file mode 100644
index 0000000..02c2559
--- /dev/null
+++ b/tests/debugger/nondet_stack.exp5
@@ -0,0 +1,861 @@
+      E1:     C1 CALL pred nondet_stack.main/2-0 (cc_multi) nondet_stack.m:NNNN
+mdb> echo on
+Command echo enabled.
+mdb> context none
+Contexts will not be printed.
+mdb> register --quiet
+mdb> goto 22
+      E2:     C2 SWTC pred nondet_stack.qperm/2-0 (nondet) s2-2;
+mdb> nondet_stack -f 3
+non 135: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 135
+ succip: unnamed label
+ succfr: non 103
+non 122: temp
+ redoip: label UNKNOWN
+ redofr: non 116
+non 119: temp
+ redoip: unnamed label
+ redofr: non 116
+<more stack frames snipped>
+mdb> nondet_stack
+non 135: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 135
+ succip: unnamed label
+ succfr: non 103
+non 122: temp
+ redoip: label UNKNOWN
+ redofr: non 116
+non 119: temp
+ redoip: unnamed label
+ redofr: non 116
+non 116: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 116
+ succip: unnamed label
+ succfr: non 103
+non 103: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 103
+ succip: unnamed label
+ succfr: non  71
+non  90: temp
+ redoip: label UNKNOWN
+ redofr: non  84
+non  87: temp
+ redoip: unnamed label
+ redofr: non  84
+non  84: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  84
+ succip: unnamed label
+ succfr: non  71
+non  71: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  71
+ succip: unnamed label
+ succfr: non  39
+non  58: temp
+ redoip: label UNKNOWN
+ redofr: non  52
+non  55: temp
+ redoip: unnamed label
+ redofr: non  52
+non  52: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  52
+ succip: unnamed label
+ succfr: non  39
+non  39: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  39
+ succip: unnamed label
+ succfr: non  26
+non  26: ordinary, 12 words
+ redoip: unnamed label
+ redofr: non  26
+ succip: unnamed label
+ succfr: non  10
+non  14: temp
+ redoip: label UNKNOWN
+ redofr: non  10
+ detfr:  det  14
+non  10: ordinary, 6 words
+ redoip: label global_fail
+ redofr: non  10
+ succip: label wrapper_not_reached
+ succfr: non   4
+mdb> stack_regs
+sp = det  14
+curfr = non 135
+maxfr = non 135
+mdb> nondet_stack -d
+non 135: ordinary, 13 words, pred nondet_stack.qperm/2-0 (nondet) <s2-2;>
+ redoip: unnamed label
+ redofr: non 135
+ succip: unnamed label
+ succfr: non 103
+ on main nondet branch non 135
+       HeadVar__1             [4, 5]
+       TypeInfo_for_T         int
+non 122: temp
+ redoip: label UNKNOWN
+ redofr: non 116
+non 119: temp
+ redoip: unnamed label
+ redofr: non 116
+non 116: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 116
+ succip: unnamed label
+ succfr: non 103
+ top frame of a nondet side branch non 116
+       HeadVar__2             [3, 4, 5]
+       TypeInfo_for_T         int
+non 103: ordinary, 13 words, pred nondet_stack.qperm/2-0 (nondet) <s2-2;c2;>
+ redoip: unnamed label
+ redofr: non 103
+ succip: unnamed label
+ succfr: non  71
+ on main nondet branch non 135
+       HeadVar__1             [3, 4, 5]
+       TypeInfo_for_T         int
+       U                      3
+       Z                      [4, 5]
+non  90: temp
+ redoip: label UNKNOWN
+ redofr: non  84
+non  87: temp
+ redoip: unnamed label
+ redofr: non  84
+non  84: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  84
+ succip: unnamed label
+ succfr: non  71
+ top frame of a nondet side branch non  84
+       HeadVar__2             [2, 3, 4, 5]
+       TypeInfo_for_T         int
+non  71: ordinary, 13 words, pred nondet_stack.qperm/2-0 (nondet) <s2-2;c2;>
+ redoip: unnamed label
+ redofr: non  71
+ succip: unnamed label
+ succfr: non  39
+ on main nondet branch non 135
+       HeadVar__1             [2, 3, 4, 5]
+       TypeInfo_for_T         int
+       U                      2
+       Z                      [3, 4, 5]
+non  58: temp
+ redoip: label UNKNOWN
+ redofr: non  52
+non  55: temp
+ redoip: unnamed label
+ redofr: non  52
+non  52: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  52
+ succip: unnamed label
+ succfr: non  39
+ top frame of a nondet side branch non  52
+       HeadVar__2             [1, 2, 3, 4, 5]
+       TypeInfo_for_T         int
+non  39: ordinary, 13 words, pred nondet_stack.qperm/2-0 (nondet) <s2-2;c2;>
+ redoip: unnamed label
+ redofr: non  39
+ succip: unnamed label
+ succfr: non  26
+ on main nondet branch non 135
+       HeadVar__1             [1, 2, 3, 4, 5]
+       TypeInfo_for_T         int
+       U                      1
+       Z                      [2, 3, 4, 5]
+non  26: ordinary, 12 words, pred nondet_stack.queen/2-0 (nondet) <c2;>
+ redoip: unnamed label
+ redofr: non  26
+ succip: unnamed label
+ succfr: non  10
+ on main nondet branch non 135
+       Data (arg 1)           [1, 2, 3, 4, 5]
+       TypeCtorInfo_5         int
+non  14: temp
+ redoip: label UNKNOWN
+ redofr: non  10
+ detfr:  det  14
+non  10: ordinary, 6 words
+ redoip: label global_fail
+ redofr: non  10
+ succip: label wrapper_not_reached
+ succfr: non   4
+mdb> goto 39
+      E3:     C3 CALL pred nondet_stack.safe/1-0 (semidet)
+mdb> nondet_stack
+non 217: temp
+ redoip: label UNKNOWN
+ redofr: non  39
+non 214: temp
+ redoip: label UNKNOWN
+ redofr: non  71
+non 211: temp
+ redoip: label UNKNOWN
+ redofr: non 103
+non 208: temp
+ redoip: label UNKNOWN
+ redofr: non 135
+non 205: temp
+ redoip: label UNKNOWN
+ redofr: non 167
+non 202: temp
+ redoip: label UNKNOWN
+ redofr: non 199
+non 199: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 199
+ succip: unnamed label
+ succfr: non 167
+non 186: temp
+ redoip: label UNKNOWN
+ redofr: non 180
+non 183: temp
+ redoip: unnamed label
+ redofr: non 180
+non 180: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 180
+ succip: unnamed label
+ succfr: non 167
+non 167: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 167
+ succip: unnamed label
+ succfr: non 135
+non 154: temp
+ redoip: label UNKNOWN
+ redofr: non 148
+non 151: temp
+ redoip: unnamed label
+ redofr: non 148
+non 148: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 148
+ succip: unnamed label
+ succfr: non 135
+non 135: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 135
+ succip: unnamed label
+ succfr: non 103
+non 122: temp
+ redoip: label UNKNOWN
+ redofr: non 116
+non 119: temp
+ redoip: unnamed label
+ redofr: non 116
+non 116: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 116
+ succip: unnamed label
+ succfr: non 103
+non 103: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 103
+ succip: unnamed label
+ succfr: non  71
+non  90: temp
+ redoip: label UNKNOWN
+ redofr: non  84
+non  87: temp
+ redoip: unnamed label
+ redofr: non  84
+non  84: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  84
+ succip: unnamed label
+ succfr: non  71
+non  71: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  71
+ succip: unnamed label
+ succfr: non  39
+non  58: temp
+ redoip: label UNKNOWN
+ redofr: non  52
+non  55: temp
+ redoip: unnamed label
+ redofr: non  52
+non  52: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  52
+ succip: unnamed label
+ succfr: non  39
+non  39: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  39
+ succip: unnamed label
+ succfr: non  26
+non  26: ordinary, 12 words
+ redoip: unnamed label
+ redofr: non  26
+ succip: unnamed label
+ succfr: non  10
+non  14: temp
+ redoip: label UNKNOWN
+ redofr: non  10
+ detfr:  det  14
+non  10: ordinary, 6 words
+ redoip: label global_fail
+ redofr: non  10
+ succip: label wrapper_not_reached
+ succfr: non   4
+mdb> stack_regs
+sp = det  22
+curfr = non  26
+maxfr = non 217
+mdb> nondet_stack -d
+non 217: temp
+ redoip: label UNKNOWN
+ redofr: non  39
+non 214: temp
+ redoip: label UNKNOWN
+ redofr: non  71
+non 211: temp
+ redoip: label UNKNOWN
+ redofr: non 103
+non 208: temp
+ redoip: label UNKNOWN
+ redofr: non 135
+non 205: temp
+ redoip: label UNKNOWN
+ redofr: non 167
+non 202: temp
+ redoip: label UNKNOWN
+ redofr: non 199
+non 199: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 199
+ succip: unnamed label
+ succfr: non 167
+ top frame of a nondet side branch non 199
+       HeadVar__1             []
+       TypeInfo_for_T         int
+non 186: temp
+ redoip: label UNKNOWN
+ redofr: non 180
+non 183: temp
+ redoip: unnamed label
+ redofr: non 180
+non 180: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 180
+ succip: unnamed label
+ succfr: non 167
+ top frame of a nondet side branch non 180
+       HeadVar__2             [5]
+       TypeInfo_for_T         int
+non 167: ordinary, 13 words, pred nondet_stack.qperm/2-0 (nondet) <s2-2;c2;>
+ redoip: unnamed label
+ redofr: non 167
+ succip: unnamed label
+ succfr: non 135
+ internal frame on nondet side branch non 199
+       HeadVar__1             [5]
+       TypeInfo_for_T         int
+       U                      5
+       Z                      []
+non 154: temp
+ redoip: label UNKNOWN
+ redofr: non 148
+non 151: temp
+ redoip: unnamed label
+ redofr: non 148
+non 148: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 148
+ succip: unnamed label
+ succfr: non 135
+ top frame of a nondet side branch non 148
+       HeadVar__2             [4, 5]
+       TypeInfo_for_T         int
+non 135: ordinary, 13 words, pred nondet_stack.qperm/2-0 (nondet) <s2-2;c2;>
+ redoip: unnamed label
+ redofr: non 135
+ succip: unnamed label
+ succfr: non 103
+ internal frame on nondet side branch non 199
+       HeadVar__1             [4, 5]
+       TypeInfo_for_T         int
+       U                      4
+       Z                      [5]
+non 122: temp
+ redoip: label UNKNOWN
+ redofr: non 116
+non 119: temp
+ redoip: unnamed label
+ redofr: non 116
+non 116: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 116
+ succip: unnamed label
+ succfr: non 103
+ top frame of a nondet side branch non 116
+       HeadVar__2             [3, 4, 5]
+       TypeInfo_for_T         int
+non 103: ordinary, 13 words, pred nondet_stack.qperm/2-0 (nondet) <s2-2;c2;>
+ redoip: unnamed label
+ redofr: non 103
+ succip: unnamed label
+ succfr: non  71
+ internal frame on nondet side branch non 199
+       HeadVar__1             [3, 4, 5]
+       TypeInfo_for_T         int
+       U                      3
+       Z                      [4, 5]
+non  90: temp
+ redoip: label UNKNOWN
+ redofr: non  84
+non  87: temp
+ redoip: unnamed label
+ redofr: non  84
+non  84: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  84
+ succip: unnamed label
+ succfr: non  71
+ top frame of a nondet side branch non  84
+       HeadVar__2             [2, 3, 4, 5]
+       TypeInfo_for_T         int
+non  71: ordinary, 13 words, pred nondet_stack.qperm/2-0 (nondet) <s2-2;c2;>
+ redoip: unnamed label
+ redofr: non  71
+ succip: unnamed label
+ succfr: non  39
+ internal frame on nondet side branch non 199
+       HeadVar__1             [2, 3, 4, 5]
+       TypeInfo_for_T         int
+       U                      2
+       Z                      [3, 4, 5]
+non  58: temp
+ redoip: label UNKNOWN
+ redofr: non  52
+non  55: temp
+ redoip: unnamed label
+ redofr: non  52
+non  52: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  52
+ succip: unnamed label
+ succfr: non  39
+ top frame of a nondet side branch non  52
+       HeadVar__2             [1, 2, 3, 4, 5]
+       TypeInfo_for_T         int
+non  39: ordinary, 13 words, pred nondet_stack.qperm/2-0 (nondet) <s2-2;c2;>
+ redoip: unnamed label
+ redofr: non  39
+ succip: unnamed label
+ succfr: non  26
+ internal frame on nondet side branch non 199
+       HeadVar__1             [1, 2, 3, 4, 5]
+       TypeInfo_for_T         int
+       U                      1
+       Z                      [2, 3, 4, 5]
+non  26: ordinary, 12 words, pred nondet_stack.queen/2-0 (nondet) <c3;>
+ redoip: unnamed label
+ redofr: non  26
+ succip: unnamed label
+ succfr: non  10
+ on main nondet branch non  26
+       Data (arg 1)           [1, 2, 3, 4, 5]
+       Out (arg 2)            [1, 2, 3, 4, 5]
+       TypeCtorInfo_5         int
+non  14: temp
+ redoip: label UNKNOWN
+ redofr: non  10
+ detfr:  det  14
+non  10: ordinary, 6 words
+ redoip: label global_fail
+ redofr: non  10
+ succip: label wrapper_not_reached
+ succfr: non   4
+mdb> break nondet_stack__test
+ 0: + stop  interface pred nondet_stack.test/2-0 (nondet)
+mdb> continue
+      E4:     C4 CALL pred nondet_stack.test/2-0 (nondet)
+mdb> nondet_stack
+non 284: ordinary, 12 words
+ redoip: unnamed label
+ redofr: non 284
+ succip: unnamed label
+ succfr: non  10
+non 272: temp
+ redoip: label UNKNOWN
+ redofr: non  10
+ detfr:  det  14
+non 268: temp
+ redoip: label UNKNOWN
+ redofr: non  26
+non 265: temp
+ redoip: label UNKNOWN
+ redofr: non  39
+non 262: temp
+ redoip: label UNKNOWN
+ redofr: non  71
+non 259: temp
+ redoip: label UNKNOWN
+ redofr: non 119
+non 256: temp
+ redoip: label UNKNOWN
+ redofr: non 183
+non 253: temp
+ redoip: label UNKNOWN
+ redofr: non 215
+non 250: temp
+ redoip: label UNKNOWN
+ redofr: non 247
+non 247: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 247
+ succip: unnamed label
+ succfr: non 215
+non 234: temp
+ redoip: label UNKNOWN
+ redofr: non 228
+non 231: temp
+ redoip: unnamed label
+ redofr: non 228
+non 228: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 228
+ succip: unnamed label
+ succfr: non 215
+non 215: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 215
+ succip: unnamed label
+ succfr: non 183
+non 202: temp
+ redoip: label UNKNOWN
+ redofr: non 196
+non 199: temp
+ redoip: unnamed label
+ redofr: non 196
+non 196: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 196
+ succip: unnamed label
+ succfr: non 183
+non 183: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 183
+ succip: unnamed label
+ succfr: non 119
+non 170: temp
+ redoip: label UNKNOWN
+ redofr: non 132
+non 167: temp
+ redoip: label UNKNOWN
+ redofr: non 145
+non 164: temp
+ redoip: label UNKNOWN
+ redofr: non 158
+non 161: temp
+ redoip: unnamed label
+ redofr: non 158
+non 158: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 158
+ succip: unnamed label
+ succfr: non 145
+non 145: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 145
+ succip: unnamed label
+ succfr: non 132
+non 132: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 132
+ succip: unnamed label
+ succfr: non 119
+non 119: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 119
+ succip: unnamed label
+ succfr: non  71
+non 106: temp
+ redoip: label UNKNOWN
+ redofr: non  84
+non 103: temp
+ redoip: label UNKNOWN
+ redofr: non  97
+non 100: temp
+ redoip: unnamed label
+ redofr: non  97
+non  97: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  97
+ succip: unnamed label
+ succfr: non  84
+non  84: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  84
+ succip: unnamed label
+ succfr: non  71
+non  71: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  71
+ succip: unnamed label
+ succfr: non  39
+non  58: temp
+ redoip: label UNKNOWN
+ redofr: non  52
+non  55: temp
+ redoip: unnamed label
+ redofr: non  52
+non  52: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  52
+ succip: unnamed label
+ succfr: non  39
+non  39: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  39
+ succip: unnamed label
+ succfr: non  26
+non  26: ordinary, 12 words
+ redoip: unnamed label
+ redofr: non  26
+ succip: unnamed label
+ succfr: non  10
+non  14: temp
+ redoip: label UNKNOWN
+ redofr: non  10
+ detfr:  det  14
+non  10: ordinary, 6 words
+ redoip: label global_fail
+ redofr: non  10
+ succip: label wrapper_not_reached
+ succfr: non   4
+mdb> stack_regs
+sp = det  14
+curfr = non 284
+maxfr = non 284
+mdb> nondet_stack -d
+non 284: ordinary, 12 words, pred nondet_stack.test/2-0 (nondet) <>
+ redoip: unnamed label
+ redofr: non 284
+ succip: unnamed label
+ succfr: non  10
+ on main nondet branch non 284
+       HeadVar__1             [1, 3, 5, 2, 4]
+non 272: temp
+ redoip: label UNKNOWN
+ redofr: non  10
+ detfr:  det  14
+non 268: temp
+ redoip: label UNKNOWN
+ redofr: non  26
+non 265: temp
+ redoip: label UNKNOWN
+ redofr: non  39
+non 262: temp
+ redoip: label UNKNOWN
+ redofr: non  71
+non 259: temp
+ redoip: label UNKNOWN
+ redofr: non 119
+non 256: temp
+ redoip: label UNKNOWN
+ redofr: non 183
+non 253: temp
+ redoip: label UNKNOWN
+ redofr: non 215
+non 250: temp
+ redoip: label UNKNOWN
+ redofr: non 247
+non 247: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 247
+ succip: unnamed label
+ succfr: non 215
+ top frame of a nondet side branch non 247
+       HeadVar__1             []
+       TypeInfo_for_T         int
+non 234: temp
+ redoip: label UNKNOWN
+ redofr: non 228
+non 231: temp
+ redoip: unnamed label
+ redofr: non 228
+non 228: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 228
+ succip: unnamed label
+ succfr: non 215
+ top frame of a nondet side branch non 228
+       HeadVar__2             [4]
+       TypeInfo_for_T         int
+non 215: ordinary, 13 words, pred nondet_stack.qperm/2-0 (nondet) <s2-2;c2;>
+ redoip: unnamed label
+ redofr: non 215
+ succip: unnamed label
+ succfr: non 183
+ internal frame on nondet side branch non 247
+       HeadVar__1             [4]
+       TypeInfo_for_T         int
+       U                      4
+       Z                      []
+non 202: temp
+ redoip: label UNKNOWN
+ redofr: non 196
+non 199: temp
+ redoip: unnamed label
+ redofr: non 196
+non 196: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 196
+ succip: unnamed label
+ succfr: non 183
+ top frame of a nondet side branch non 196
+       HeadVar__2             [2, 4]
+       TypeInfo_for_T         int
+non 183: ordinary, 13 words, pred nondet_stack.qperm/2-0 (nondet) <s2-2;c2;>
+ redoip: unnamed label
+ redofr: non 183
+ succip: unnamed label
+ succfr: non 119
+ internal frame on nondet side branch non 247
+       HeadVar__1             [2, 4]
+       TypeInfo_for_T         int
+       U                      2
+       Z                      [4]
+non 170: temp
+ redoip: label UNKNOWN
+ redofr: non 132
+non 167: temp
+ redoip: label UNKNOWN
+ redofr: non 145
+non 164: temp
+ redoip: label UNKNOWN
+ redofr: non 158
+non 161: temp
+ redoip: unnamed label
+ redofr: non 158
+non 158: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non 158
+ succip: unnamed label
+ succfr: non 145
+ top frame of a nondet side branch non 158
+       HeadVar__2             [5]
+       TypeInfo_for_T         int
+non 145: ordinary, 13 words, pred nondet_stack.qdelete/3-0 (nondet) <c2;d2;c3;>
+ redoip: unnamed label
+ redofr: non 145
+ succip: unnamed label
+ succfr: non 132
+ internal frame on nondet side branch non 158
+       HeadVar__2             [4, 5]
+       A                      4
+       TypeInfo_for_T         int
+       Z                      [5]
+non 132: ordinary, 13 words, pred nondet_stack.qdelete/3-0 (nondet) <c2;d2;c3;>
+ redoip: unnamed label
+ redofr: non 132
+ succip: unnamed label
+ succfr: non 119
+ internal frame on nondet side branch non 158
+       HeadVar__2             [2, 4, 5]
+       A                      2
+       TypeInfo_for_T         int
+       Z                      [4, 5]
+non 119: ordinary, 13 words, pred nondet_stack.qperm/2-0 (nondet) <s2-2;c2;>
+ redoip: unnamed label
+ redofr: non 119
+ succip: unnamed label
+ succfr: non  71
+ internal frame on nondet side branch non 247
+       HeadVar__1             [2, 4, 5]
+       TypeInfo_for_T         int
+       U                      5
+       Z                      [2, 4]
+non 106: temp
+ redoip: label UNKNOWN
+ redofr: non  84
+non 103: temp
+ redoip: label UNKNOWN
+ redofr: non  97
+non 100: temp
+ redoip: unnamed label
+ redofr: non  97
+non  97: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  97
+ succip: unnamed label
+ succfr: non  84
+ top frame of a nondet side branch non  97
+       HeadVar__2             [3, 4, 5]
+       TypeInfo_for_T         int
+non  84: ordinary, 13 words, pred nondet_stack.qdelete/3-0 (nondet) <c2;d2;c3;>
+ redoip: unnamed label
+ redofr: non  84
+ succip: unnamed label
+ succfr: non  71
+ internal frame on nondet side branch non  97
+       HeadVar__2             [2, 3, 4, 5]
+       A                      2
+       TypeInfo_for_T         int
+       Z                      [3, 4, 5]
+non  71: ordinary, 13 words, pred nondet_stack.qperm/2-0 (nondet) <s2-2;c2;>
+ redoip: unnamed label
+ redofr: non  71
+ succip: unnamed label
+ succfr: non  39
+ internal frame on nondet side branch non 247
+       HeadVar__1             [2, 3, 4, 5]
+       TypeInfo_for_T         int
+       U                      3
+       Z                      [2, 4, 5]
+non  58: temp
+ redoip: label UNKNOWN
+ redofr: non  52
+non  55: temp
+ redoip: unnamed label
+ redofr: non  52
+non  52: ordinary, 13 words
+ redoip: unnamed label
+ redofr: non  52
+ succip: unnamed label
+ succfr: non  39
+ top frame of a nondet side branch non  52
+       HeadVar__2             [1, 2, 3, 4, 5]
+       TypeInfo_for_T         int
+non  39: ordinary, 13 words, pred nondet_stack.qperm/2-0 (nondet) <s2-2;c2;>
+ redoip: unnamed label
+ redofr: non  39
+ succip: unnamed label
+ succfr: non  26
+ internal frame on nondet side branch non 247
+       HeadVar__1             [1, 2, 3, 4, 5]
+       TypeInfo_for_T         int
+       U                      1
+       Z                      [2, 3, 4, 5]
+non  26: ordinary, 12 words, pred nondet_stack.queen/2-0 (nondet) <c2;>
+ redoip: unnamed label
+ redofr: non  26
+ succip: unnamed label
+ succfr: non  10
+ internal frame on nondet side branch non 247
+       Data (arg 1)           [1, 2, 3, 4, 5]
+       TypeCtorInfo_5         int
+non  14: temp
+ redoip: label UNKNOWN
+ redofr: non  10
+ detfr:  det  14
+non  10: ordinary, 6 words
+ redoip: label global_fail
+ redofr: non  10
+ succip: label wrapper_not_reached
+ succfr: non   4
+mdb> continue -S
+[2, 5, 3, 1, 4]




More information about the reviews mailing list