1301 lines
39 KiB
MiniZinc
1301 lines
39 KiB
MiniZinc
%
|
|
% Main authors:
|
|
% Mats Carlsson <mats.carlsson@ri.se>
|
|
%
|
|
% This file is part of Unison, see http://unison-code.github.io
|
|
%
|
|
% Copyright (c) 2016, RISE SICS AB
|
|
% All rights reserved.
|
|
%
|
|
% Redistribution and use in source and binary forms, with or without
|
|
% modification, are permitted provided that the following conditions are met:
|
|
% 1. Redistributions of source code must retain the above copyright notice,
|
|
% this list of conditions and the following disclaimer.
|
|
% 2. Redistributions in binary form must reproduce the above copyright notice,
|
|
% this list of conditions and the following disclaimer in the documentation
|
|
% and/or other materials provided with the distribution.
|
|
% 3. Neither the name of the copyright holder nor the names of its contributors
|
|
% may be used to endorse or promote products derived from this software
|
|
% without specific prior written permission.
|
|
%
|
|
% THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
|
% AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
|
% IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
|
% ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
|
|
% LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
|
% CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
|
% SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
|
% INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
|
% CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
|
% ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
|
% POSSIBILITY OF SUCH DAMAGE.
|
|
|
|
include "globals.mzn";
|
|
|
|
%% solver parameters
|
|
|
|
bool: optimize_cycles;
|
|
|
|
%% some constants
|
|
%% N.B. keep in sync with modeler! see also isreal()!
|
|
|
|
int: TYPE_LINEAR = 0;
|
|
int: TYPE_BRANCH = 1;
|
|
int: TYPE_CALL = 2;
|
|
int: TYPE_TAIL = 3;
|
|
int: TYPE_IN = 4;
|
|
int: TYPE_OUT = 5;
|
|
int: TYPE_KILL = 6;
|
|
int: TYPE_DEFINE = 7;
|
|
int: TYPE_COMBINE = 8;
|
|
int: TYPE_LOW = 9;
|
|
int: TYPE_HIGH = 10;
|
|
int: TYPE_SPLIT2 = 11;
|
|
int: TYPE_SPLIT4 = 12;
|
|
int: TYPE_FUN = 13;
|
|
int: TYPE_COPY = 14;
|
|
|
|
%% problem parameters
|
|
|
|
int: MAXF;
|
|
int: MAXO;
|
|
int: MAXP;
|
|
int: MAXT;
|
|
int: MAXC;
|
|
int: MAXI;
|
|
int: MAXR;
|
|
int: MAXB = max(index_set(bb_ops));
|
|
int: MINL;
|
|
int: MAXL;
|
|
int: MAXINSNS = max(o in 0..MAXO)(card(op_instructions[o]));
|
|
int: MAXTEMPS = max(p in 0..MAXP)(card(operand_temps[p]));
|
|
|
|
set of int: expr = index_set(expr_op);
|
|
|
|
%% see JSON freq, maxc, ins, tmp, operands, optional_min
|
|
array[int] of int: bb_order;
|
|
array[int] of set of int: bb_ops;
|
|
array[int] of set of int: bb_operands;
|
|
array[int] of set of int: bb_temps;
|
|
array[int] of set of int: bb_subsumed;
|
|
array[int] of int: bb_frequency;
|
|
array[int] of int: bb_maxcycle;
|
|
array[int] of int: bb_optional_min;
|
|
|
|
%% see JSON operands, instructions, type
|
|
array[int] of set of int: op_operands;
|
|
array[int] of set of int: op_instructions;
|
|
array[int] of int: op_type;
|
|
array[int] of bool: op_mand;
|
|
|
|
%% see JSON atoms
|
|
array[int] of set of int: atom_regs; % atom -> registers
|
|
|
|
%% see JSON calleesaved, callersaved, infinite, bounded, range
|
|
set of int: calleesaved;
|
|
set of int: callersaved;
|
|
set of int: infinite;
|
|
array[int] of bool: bounded;
|
|
array[int] of set of int: range;
|
|
|
|
%% see JSON cap, con, dur, off
|
|
array[int] of int: res_cap;
|
|
array[int,int] of int: res_con;
|
|
array[int,int] of int: res_dur;
|
|
array[int,int] of int: res_off;
|
|
|
|
%% see JSON congr
|
|
array[int] of set of int: congr;
|
|
|
|
%% see JSON strictly_congr
|
|
array[int] of set of int: strictly_congr;
|
|
|
|
%% see JSON preassign
|
|
array[int] of int: preassign_operand;
|
|
array[int] of int: preassign_reg;
|
|
|
|
%% see JSON aligned/adist
|
|
array[int] of int: aligned_use;
|
|
array[int] of int: aligned_def;
|
|
array[int] of int: aligned_usei;
|
|
array[int] of int: aligned_defi;
|
|
array[int] of int: aligned_dist;
|
|
|
|
%% see JSON adjacent
|
|
array[int] of int: adj_from;
|
|
array[int] of int: adj_to;
|
|
|
|
%% see JSON quasi_adjacent
|
|
array[int] of int: quasi_adj_from;
|
|
array[int] of int: quasi_adj_to;
|
|
|
|
%% see JSON long_latency
|
|
array[int,int] of set of int: long_latency_index;
|
|
array[int] of int: long_latency_def;
|
|
array[int] of int: long_latency_use;
|
|
|
|
%% see JSON operands
|
|
array[int] of int: operand_definer; % operand -> defining op
|
|
|
|
%% see JSON use
|
|
array[int] of bool: operand_use;
|
|
|
|
%% see JSON last_use
|
|
array[int] of bool: operand_lastuse;
|
|
|
|
%% see JSON temps
|
|
array[int] of set of int: operand_temps;
|
|
|
|
%% see JSON class, operands, instructions
|
|
array[int,int] of int: operand_atom; % operand x operation -> atom
|
|
|
|
%% see JSON temps
|
|
array[int] of set of int: related_temps;
|
|
|
|
%% see JSON definer, temps, width, minlive
|
|
array[int] of int: temp_definer; % temp -> defining op
|
|
array[int] of int: temp_def; % temp -> defining operand
|
|
array[int] of int: temp_width; % temp -> width
|
|
array[int] of int: temp_minlive; % temp -> minlive
|
|
array[int] of set of int: temp_uses; % temp -> set of use operands
|
|
array[int] of set of int: temp_domain; % temp -> domain of regs
|
|
|
|
%% see JSON packed, pinstrs
|
|
array[int,int] of int: packed_pq;
|
|
|
|
%% see JSON before
|
|
array[int] of int: before_pred;
|
|
array[int] of int: before_succ;
|
|
array[int] of expr: before_cond;
|
|
|
|
%% see JSON E
|
|
array[int] of int: adhoc;
|
|
|
|
%% see JSON nogoods
|
|
array[int] of expr: nogood;
|
|
|
|
%% see JSON across
|
|
array[int] of int: across_op;
|
|
array[int] of set of int: across_regs;
|
|
array[int] of set of int: across_items;
|
|
array[int] of int: across_item_temp;
|
|
array[int] of expr: across_item_cond;
|
|
|
|
%% see JSON set_across
|
|
array[int] of int: setacross_op;
|
|
array[int] of set of int: setacross_regs;
|
|
array[int] of set of int: setacross_tempsets;
|
|
|
|
%% see JSON difftemps
|
|
array[int] of set of int: difftemp;
|
|
|
|
%% see JSON diffregs
|
|
array[int] of set of int: diffreg;
|
|
|
|
%% see JSON domops
|
|
array[int] of set of int: domop_operands;
|
|
array[int] of set of int: domop_temps;
|
|
|
|
%% see JSON domuse
|
|
array[int] of int: domuse_p;
|
|
array[int] of int: domuse_q;
|
|
array[int] of int: domuse_r;
|
|
|
|
%% see JSON infassign
|
|
array[int,int] of int: infassign;
|
|
|
|
%% see JSON space
|
|
array[int] of int: space;
|
|
|
|
%% see JSON dominates
|
|
array[int] of int: dominate_ing;
|
|
array[int] of int: dominate_ed;
|
|
array[int] of set of int: dominate_instructions;
|
|
array[int] of set of int: dominate_temps;
|
|
|
|
%% see JSON precedences
|
|
array[int] of expr: precedence;
|
|
|
|
%% see JSON active_tables, tmp_tables
|
|
array[int] of set of int: table_exists_ops;
|
|
array[int] of set of int: table_iffall_ops;
|
|
array[int] of set of int: relation_ops;
|
|
array[int] of set of int: relation_temps;
|
|
array[int] of int: relation_ntuples;
|
|
array[int] of set of int: relation_range;
|
|
|
|
%% see JSON calleesaved_spill
|
|
array[int] of set of int: calleesaved_spill;
|
|
array[int,int] of int: cs_spill_transpose;
|
|
|
|
%% see JSON activators
|
|
array[int] of set of int: activator_insns;
|
|
array[int] of set of int: activator_ops;
|
|
|
|
%% see JSON value_precede_chain
|
|
array[int] of int: value_precede_min;
|
|
array[int] of int: value_precede_max;
|
|
array[int] of set of int: value_precede_regs;
|
|
array[int] of int: value_precede_temps;
|
|
|
|
%% see JSON lat
|
|
array[int,int] of int: lat_table;
|
|
|
|
%% see JSON preschedule
|
|
array[int] of int: preschedule_op;
|
|
array[int] of int: preschedule_cycle;
|
|
|
|
%% see JSON bypass
|
|
array[int,int] of int: bypass_table;
|
|
|
|
%% see JSON exrelated, table
|
|
array[int] of int: exrelated_p;
|
|
array[int] of int: exrelated_q;
|
|
array[int] of set of int: exrelated_rows;
|
|
array[int,int] of int: exrelated_ext;
|
|
|
|
%% see JSON wcet
|
|
array[int,int] of int: wcet;
|
|
|
|
%% extra storage for constraint expressions
|
|
array[int] of int: expr_op;
|
|
array[int] of int: expr_arg1;
|
|
array[int] of int: expr_arg2;
|
|
array[int] of int: expr_arg3;
|
|
array[int] of set of int: expr_children;
|
|
|
|
%% extra store for relations in table constraints
|
|
array[int] of int: ints;
|
|
|
|
%% extra storage: each set is a set of temporaries
|
|
array[int] of set of int: sets;
|
|
|
|
%% problem variables
|
|
|
|
var 0..MAXF: objective;
|
|
array[0..MAXO] of var bool: a;
|
|
array[0..MAXO] of var 1..MAXINSNS: ii; % same as in gecode-solver
|
|
array[0..MAXO] of var -1..MAXC: c;
|
|
array[0..MAXP] of var -1..MAXR: rt;
|
|
array[0..MAXP] of var MINL..MAXL: lt; % operand latency
|
|
array[0..MAXP] of var -MAXL..MAXL: s; % global operand slack
|
|
array[0..MAXP] of var 1..MAXTEMPS: y; % same as in gecode-solver
|
|
array[-1..MAXT] of var -1..MAXR: r;
|
|
array[-1..MAXT] of var -1..MAXC: ls;
|
|
array[-1..MAXT] of var 0..MAXC: ld;
|
|
array[-1..MAXT] of var -1..MAXC: le;
|
|
array[1..MAXB] of var 0..MAXC: copysum;
|
|
|
|
%% PREDICATES AND TESTS
|
|
|
|
test isreal(int: o) = (op_type[o] in
|
|
{TYPE_LINEAR, TYPE_BRANCH, TYPE_CALL, TYPE_TAIL, TYPE_FUN, TYPE_COPY});
|
|
|
|
test fixedop(int: o) = (
|
|
op_instructions[o] != {0} /\ card(op_instructions[o]) = 1
|
|
);
|
|
|
|
test all_equal_ints(array[int] of int: x) =
|
|
forall(i, j in index_set(x) where i < j) ( x[i] = x[j] );
|
|
|
|
var int: res_con_of_op(int: res, int: o) =
|
|
let {array[int] of int: I = op_instructions[o]} in
|
|
let {array[int] of int: ints = [res_con[res,I[i]] | i in index_set(I)]} in
|
|
if all_equal_ints(ints) then ints[1] else ints[ii[o]] endif;
|
|
|
|
var int: res_dur_of_op(int: res, int: o) =
|
|
let {array[int] of int: I = op_instructions[o]} in
|
|
let {array[int] of int: ints = [res_dur[res,I[i]] | i in index_set(I)]} in
|
|
if all_equal_ints(ints) then ints[1] else ints[ii[o]] endif;
|
|
|
|
var int: res_off_of_op(int: res, int: o) =
|
|
let {array[int] of int: I = op_instructions[o]} in
|
|
let {array[int] of int: ints = [res_off[res,I[i]] | i in index_set(I)]} in
|
|
if all_equal_ints(ints) then ints[1] else ints[ii[o]] endif;
|
|
|
|
predicate insn_eq(int: o, int: x) =
|
|
let {array[int] of int: I = op_instructions[o]} in
|
|
exists(j in index_set(I) where I[j]=x)(ii[o]=j);
|
|
|
|
predicate insn_in(int: o, set of int: X) =
|
|
if card(X)=0 then
|
|
false
|
|
else if card(X)=1 then
|
|
insn_eq(o, min(X))
|
|
else
|
|
let {array[int] of int: I = op_instructions[o]} in
|
|
ii[o] in {j | j in index_set(I) where I[j] in X}
|
|
endif endif;
|
|
|
|
predicate smart_alldiff(array[int] of var int: X) =
|
|
if length(X)<2 then
|
|
true
|
|
else if length(X)=2 then
|
|
let {set of int: S = index_set(X)} in
|
|
X[min(S)] != X[max(S)]
|
|
else
|
|
all_different(X)
|
|
endif endif;
|
|
|
|
predicate ra_diffn(array[int] of var int: R,
|
|
array[int] of int: W,
|
|
array[int] of set of int: D,
|
|
array[int] of var int: LS,
|
|
array[int] of var int: LD,
|
|
array[int] of var int: LE) =
|
|
diffn_nonstrict(R, LS, W, LD);
|
|
|
|
predicate disjoint1(array[int] of var int: x,
|
|
array[int] of var int: w) =
|
|
diffn(x, [1 | i in index_set(x)], w, [1 | i in index_set(x)]) ;
|
|
|
|
predicate noverlap(array[int] of var int: x,
|
|
array[int] of var int: w) = (
|
|
if min([lb(z) | z in w]) < max([ub(z) | z in w]) then
|
|
disjoint1(x, w)
|
|
else if length(x) = 2 then
|
|
x[1] != x[2]
|
|
else
|
|
smart_alldiff(x)
|
|
endif endif
|
|
);
|
|
|
|
predicate live_overlap(int: k, int: j) = (ls[k] < le[j] /\ ls[j] < le[k]);
|
|
|
|
predicate operand_live_overlap(int: p, int: q) = (ls_t(p) < le_t(q) /\ ls_t(q) < le_t(p));
|
|
|
|
predicate operand_live_before(int: p, int: q) = (le_t(p) <= ls_t(q));
|
|
|
|
test operand_related(int: p, int: q) =
|
|
operand_temps[p] subset operand_temps[q] \/ operand_temps[q] subset operand_temps[p];
|
|
|
|
predicate same_temp(int: p, int: q) =
|
|
assert(operand_related(p,q), "same_temp[\(p),\(q)] with unrelated operands") /\
|
|
y[p] = y[q];
|
|
|
|
predicate temp_eq(int: p, int: t) =
|
|
let {array[int] of int: ts = operand_temps[p]} in
|
|
exists(j in index_set(ts) where ts[j]=t)(y[p]=j);
|
|
|
|
predicate temp_in(int: p, set of int: T) =
|
|
if card(T)=0 then
|
|
false
|
|
else if card(T)=1 then
|
|
temp_eq(p, min(T))
|
|
else
|
|
let {array[int] of int: ts = operand_temps[p]} in
|
|
y[p] in {j | j in index_set(ts) where ts[j] in T}
|
|
endif endif;
|
|
|
|
test temp_is_unsafe(int: t) =
|
|
if op_type[temp_definer[t]] in {TYPE_IN,TYPE_DEFINE,TYPE_FUN} then
|
|
false
|
|
else
|
|
let {array[int] of int: dlats = [lat_table[j,4] | j in index_set_1of2(lat_table)
|
|
where
|
|
lat_table[j,2] != 0 /\
|
|
lat_table[j,3] = temp_def[t]
|
|
],
|
|
array[int] of int: ulats = [lat_table[j,4] | j in index_set_1of2(lat_table)
|
|
where
|
|
lat_table[j,2] != 0 /\
|
|
lat_table[j,3] in temp_uses[t]
|
|
]} in
|
|
temp_minlive[t] > min(dlats) + min(ulats)
|
|
endif;
|
|
|
|
test temp_must_be_real(int: p) =
|
|
min(operand_temps[p])>=0;
|
|
|
|
predicate temp_is_real(int: p) =
|
|
if min(operand_temps[p])>=0 then
|
|
true
|
|
else
|
|
y[p]!=1
|
|
endif;
|
|
|
|
predicate temp_is_real_reif(int: p, var bool: re) =
|
|
if min(operand_temps[p])>=0 then
|
|
re
|
|
else
|
|
re <-> y[p]!=1
|
|
endif;
|
|
|
|
predicate insn_is_real_reif(int: o, var bool: re) =
|
|
if min(op_instructions[o])>=1 then
|
|
re
|
|
else
|
|
re <-> ii[o]!=1
|
|
endif;
|
|
|
|
predicate temp_member_reif(set of int: P, int: t, var bool: re) =
|
|
(re <-> exists(p in P)(temp_eq(p,t)));
|
|
|
|
var int: t(int: p) =
|
|
if card(operand_temps[p])=1 then min(operand_temps[p])
|
|
else if card(operand_temps[p])=2 then
|
|
let {int: a = min(operand_temps[p]),
|
|
int: b = max(operand_temps[p])}
|
|
in (b-a)*y[p] -b+a+a
|
|
else
|
|
operand_temps[p][y[p]]
|
|
endif endif;
|
|
|
|
var int: ls_t(int: p) = [ls[t] | t in operand_temps[p]][y[p]];
|
|
|
|
var int: le_t(int: p) = [le[t] | t in operand_temps[p]][y[p]];
|
|
|
|
%% conditions
|
|
predicate eval_expr(int: l) = (
|
|
let {int: tag = expr_op[l],
|
|
int: arg1 = expr_arg1[l],
|
|
int: arg2 = expr_arg2[l],
|
|
int: arg3 = expr_arg3[l],
|
|
} in (
|
|
if tag=0 then exists(j in expr_children[l])(eval_expr(j))
|
|
else if tag=1 then forall(j in expr_children[l])(eval_expr(j))
|
|
else if tag=2 then eval_expr(arg1) xor eval_expr(arg2)
|
|
else if tag=3 then eval_expr(arg1) -> eval_expr(arg2)
|
|
else if tag=4 then not eval_expr(arg1)
|
|
else if tag=5 then a[arg1]
|
|
else if tag=6 then temp_eq(arg1,arg2)
|
|
else if tag=7 then insn_eq(arg1,arg2)
|
|
else if tag=8 then c[arg2] >= c[arg1] + arg3
|
|
else if tag=9 then same_temp(arg1,arg2)
|
|
else if tag=10 then operand_live_overlap(arg1,arg2)
|
|
else if tag=11 then live_overlap(arg1,arg2)
|
|
else if tag=12 then r[arg1] in callersaved
|
|
else if tag=13 then rt[arg1] in atom_regs[arg2]
|
|
else false endif endif endif endif endif endif endif endif endif endif endif endif endif endif
|
|
)
|
|
);
|
|
|
|
var int: ite(var bool: cond, var int: thenval, var int: elseval) = (
|
|
let {array[1..2] of var int: ar = [elseval,thenval]} in
|
|
ar[cond+1]
|
|
);
|
|
|
|
0..MAXT: single_temp(int: p) = max(operand_temps[p]);
|
|
|
|
set of 0..MAXT: real_temps(int: p) = operand_temps[p] intersect 0..MAXT;
|
|
|
|
%% (mostly) ESSENTIAL CONSTRAINT
|
|
|
|
%% basic invariants, null instructions
|
|
|
|
test opt_in_temporary(int: v) =
|
|
let {int: p = temp_def[v]} in
|
|
op_type[temp_definer[v]] = TYPE_IN /\ card(operand_temps[p])>1;
|
|
|
|
constraint
|
|
r[-1] = -1 /\
|
|
ls[-1] = -1 /\
|
|
ld[-1] = 0 /\
|
|
le[-1] = -1 /\
|
|
forall(o in 0..MAXO where op_mand[o]) (a[o]) /\
|
|
forall(o in 0..MAXO where not op_mand[o]) (insn_is_real_reif(o,a[o])) /\
|
|
forall(o in 0..MAXO) (a[o] <-> c[o] >= 0) /\
|
|
forall(p in 0..MAXP where card(operand_temps[p])>1) (rt[p] = [r[v] | v in operand_temps[p]][y[p]]) /\
|
|
forall(p in 0..MAXP where card(operand_temps[p])=1) (rt[p] = r[single_temp(p)]) /\
|
|
forall(p in 0..MAXP where not op_mand[operand_definer[p]]) % rematerialization
|
|
(temp_is_real_reif(p,a[operand_definer[p]])) /\
|
|
forall(v in 0..MAXT) (ls[v]+ld[v] = le[v]) /\
|
|
forall(v in 0..MAXT where not opt_in_temporary(v)) % rematerialization
|
|
(ls[v] = c[temp_definer[v]] /\
|
|
(a[temp_definer[v]] <-> r[v] >= 0)) /\
|
|
forall(v in 0..MAXT where opt_in_temporary(v)) % rematerialization
|
|
(ls[v] in -1 .. 0 /\
|
|
(r[v] >= 0 <-> ls[v]=0) /\
|
|
(r[v] >= 0 <-> temp_eq(temp_def[v],v))) /\
|
|
forall(v in 0..MAXT) (
|
|
let {bool: unsafe = temp_is_unsafe(v),
|
|
set of int: pset = temp_uses[v],
|
|
set of int: prange = 1..card(pset),
|
|
array[prange] of int: parr = [p | p in pset],
|
|
array[prange] of var -1..MAXC: carr} in (
|
|
forall(p in prange) (carr[p] = ite(temp_eq(parr[p],v), c[operand_definer[parr[p]]], -1)) /\
|
|
if card(pset)=1 /\ not unsafe then
|
|
le[v] = carr[1]
|
|
else if not unsafe then
|
|
maximum(le[v], carr)
|
|
else
|
|
maximum(le[v], carr++[ls[v]+ % 20130930: live range can extend past last use
|
|
temp_minlive[v]*bool2int(a[temp_definer[v]])])
|
|
endif endif
|
|
)
|
|
);
|
|
|
|
%% objective, bounds on (out) cycle
|
|
|
|
constraint
|
|
forall(b in 1..MAXB) (
|
|
forall(o in bb_ops[b])(c[o] in -1..bb_maxcycle[b]) /\
|
|
c[min(bb_ops[b])] = 0 /\
|
|
copysum[b] = sum(o in bb_ops[b] where not op_mand[o])(bool2int(a[o])) /\
|
|
copysum[b] >= bb_optional_min[b]
|
|
) /\
|
|
if optimize_cycles then
|
|
objective = sum(b in 1..MAXB) (bb_frequency[b] * c[max(bb_ops[b])])
|
|
else
|
|
objective = sum(o in 0..MAXO)(res_con_of_op(1,o))
|
|
endif;
|
|
|
|
%% domains
|
|
constraint
|
|
forall(o in 0..MAXO) (ii[o] in 1..card(op_instructions[o]));
|
|
|
|
constraint
|
|
forall(q in 0..MAXP) (y[q] in 1..card(operand_temps[q]));
|
|
|
|
set of int: temp_insn_regs(int: v, int: j) =
|
|
let {int: p = temp_def[v],
|
|
int: w = temp_width[v],
|
|
int: oa = operand_atom[p,j],
|
|
set of int: ks = {k | k in index_set_1of2(infassign) where infassign[k,1]=v /\ infassign[k,2]=space[oa]},
|
|
set of int: unaligned =
|
|
if card(ks)>0 then
|
|
{r | r in atom_regs[oa]} intersect (infassign[min(ks),3]..infassign[min(ks),4])
|
|
else
|
|
{r | r in atom_regs[oa]}
|
|
endif}
|
|
in {r | r in unaligned /*where r mod w = 0*/}; % currently, that would over-constrain
|
|
|
|
set of int: generic_temp_domain(int: t1) =
|
|
if card(temp_domain[t1]) > 0 then
|
|
temp_domain[t1]
|
|
else
|
|
let {int: p = temp_def[t1],
|
|
set of int: rdom = array_union([temp_insn_regs(t1,j) | j in 1..MAXI]),
|
|
set of int: joker = if min(operand_temps[p])>=0 then {} else {-1} endif, % rematerialization
|
|
} in rdom union joker
|
|
endif;
|
|
|
|
constraint
|
|
forall(t1 in 0..MAXT) (r[t1] in generic_temp_domain(t1));
|
|
|
|
%% operation selection (register set depending on operation)
|
|
constraint
|
|
forall(p in 0..MAXP)(
|
|
let {int: o = operand_definer[p],
|
|
set of int: joker = if min(operand_temps[p])>=0 then {} else {-1} endif} in
|
|
if fixedop(o) then
|
|
rt[p] in atom_regs[operand_atom[p,min(op_instructions[o])]] union joker % rematerialization
|
|
else
|
|
let {array[int] of set of int: doms = [ if insn=0 then {-1} else atom_regs[operand_atom[p,insn]] endif
|
|
| insn in op_instructions[o]
|
|
],
|
|
array[int] of int: extension = [ if k=1 then j else r endif
|
|
| j in index_set(op_instructions[o]),
|
|
r in doms[j],
|
|
k in 1..2
|
|
],
|
|
int: nt = length(extension) div 2} in
|
|
if forall(i in index_set(doms))(doms[i] = doms[1]) then
|
|
rt[p] in doms[1]
|
|
else
|
|
table([ii[o],rt[p]], array2d(1..nt, 1..2, extension))
|
|
endif
|
|
endif
|
|
);
|
|
|
|
%% preassignments
|
|
constraint
|
|
forall(j in index_set(preassign_reg))
|
|
(rt[preassign_operand[j]] = preassign_reg[j]);
|
|
|
|
%% congruences
|
|
constraint
|
|
forall(cgr in strictly_congr) (
|
|
let {int: junior = min(cgr)} in (
|
|
forall(j in cgr where j>junior) (rt[junior] = rt[j])
|
|
)
|
|
);
|
|
|
|
%% adjacencies % rematerialization
|
|
constraint
|
|
forall( j in index_set(adj_from)
|
|
where not({adj_from[j],adj_to[j]} subset array_union(strictly_congr))
|
|
) (
|
|
let {int: p = adj_from[j],
|
|
int: q = adj_to[j]} in
|
|
(temp_is_real(q) -> temp_is_real(p)) /\
|
|
(temp_is_real(q) -> rt[p] = rt[q]) /\
|
|
(temp_is_real(p) -> exists(k in index_set(adj_from) where adj_from[k] = p)(temp_is_real(adj_to[k])))
|
|
);
|
|
|
|
constraint
|
|
forall(j in index_set(quasi_adj_from)) (
|
|
let {int: p = quasi_adj_from[j],
|
|
int: q = quasi_adj_to[j]} in
|
|
temp_is_real(q) -> temp_is_real(p)
|
|
);
|
|
|
|
%% aligned/adist
|
|
constraint
|
|
forall(j in index_set(aligned_use)) (
|
|
let {int: p = aligned_use[j],
|
|
int: q = aligned_def[j],
|
|
int: pi = aligned_usei[j],
|
|
int: qi = aligned_defi[j],
|
|
int: offset = aligned_dist[j]} in (
|
|
insn_eq(operand_definer[p],pi) /\ insn_eq(operand_definer[q],qi) -> rt[p] + offset = rt[q]
|
|
)
|
|
);
|
|
|
|
%% disjoint live ranges
|
|
constraint
|
|
forall(T in bb_temps) (
|
|
ra_diffn([r[v] | v in T],
|
|
[temp_width[v] | v in T],
|
|
[generic_temp_domain(v) | v in T],
|
|
[ls[v] | v in T],
|
|
[ld[v] | v in T],
|
|
[le[v] | v in T])
|
|
);
|
|
|
|
%% precedences (with conditions added by presolver)
|
|
constraint
|
|
forall(P in precedence) (
|
|
eval_expr(P)
|
|
);
|
|
|
|
%% slack and balancing
|
|
|
|
%% Model::global_operand
|
|
test global_operand(int: p) =
|
|
exists(j in index_set(adj_from))(adj_from[j]=p) \/
|
|
exists(j in index_set(adj_to))(adj_to[j]=p);
|
|
|
|
%% Model::slack
|
|
constraint
|
|
forall(p in 0..MAXP)(if not global_operand(p) then s[p]=0 else true endif);
|
|
|
|
%% CompleteModel::post_slack_balancing_constraints
|
|
constraint
|
|
forall(j in index_set(adj_from)) (
|
|
s[adj_from[j]] + s[adj_to[j]] = 0
|
|
);
|
|
|
|
%% Model::post_operand_latency_definition
|
|
constraint
|
|
forall(o in 0..MAXO, p in op_operands[o])(
|
|
let {array[int] of int: lcol = [ lat_table[j,4]
|
|
| j in index_set_1of2(lat_table)
|
|
where lat_table[j,1] = o /\ lat_table[j,3] = p
|
|
],
|
|
int: n = length(lcol),
|
|
bool: simple = if not op_mand[o] then
|
|
forall(k in 2..n)(lcol[k]=lcol[2])
|
|
else
|
|
forall(k in 1..n)(lcol[k]=lcol[1])
|
|
endif} in
|
|
if simple then
|
|
lt[p] = lcol[n]
|
|
else
|
|
lt[p] = lcol[ii[o]]
|
|
endif
|
|
);
|
|
|
|
%% Model::post_temporary_use_latency_definition
|
|
var -MAXL..3*MAXL: lat(int: q, int: v) =
|
|
let {int: p = temp_def[v]} in
|
|
lt[p] + s[p] + lt[q] + s[q];
|
|
|
|
%% data precedences with slack and everything
|
|
|
|
array[int] of var int: opnd_lbs(int: q) =
|
|
[ if v = -1 then -1
|
|
else c[temp_definer[v]] + lat(q,v)
|
|
endif
|
|
| v in operand_temps[q]
|
|
];
|
|
|
|
predicate post_data_prec(int: q) =
|
|
let {int: u = operand_definer[q],
|
|
array[int] of var int: lbs = opnd_lbs(q)} in
|
|
c[u] >= lbs[1] /\
|
|
c[u] >= lbs[y[q]];
|
|
|
|
%% Model::post_data_precedences_constraints
|
|
%% redundant if op_type[operand_definer[q]]!=TYPE_KILL and implied constraints are being posted
|
|
constraint
|
|
forall(q in 0..MAXP where operand_use[q])(post_data_prec(q));
|
|
|
|
%% resources
|
|
|
|
test unit_res_dur_cap(int: res, set of int: active) = (
|
|
forall(o in active, oi in op_instructions[o])(
|
|
res_con[res,oi]=res_cap[res] /\
|
|
res_dur[res,oi]=1 /\
|
|
res_off[res,oi]=0
|
|
)
|
|
);
|
|
|
|
test unit_res_dur(int: res, int: o) = (
|
|
forall(oi in op_instructions[o])(res_dur[res,oi]=1)
|
|
);
|
|
|
|
test zero_res_off(int: res, int: o) = (
|
|
forall(oi in op_instructions[o])(res_off[res,oi]=0)
|
|
);
|
|
|
|
constraint
|
|
forall(b in 1..MAXB, res in index_set(res_cap) diff bb_subsumed[b]) (
|
|
let {set of int: active = {o | o in bb_ops[b] where
|
|
exists(q in op_instructions[o])(res_con[res,q]>0)}} in (
|
|
if card(active)<=1 then true
|
|
else if unit_res_dur_cap(res,active) then
|
|
smart_alldiff([c[o] | o in active])
|
|
else
|
|
cumulative([ if zero_res_off(res,o) then c[o] else c[o]+res_off_of_op(res,o) endif
|
|
| o in active
|
|
],
|
|
[ if unit_res_dur(res,o) then 1 else res_dur_of_op(res,o) endif
|
|
| o in active
|
|
],
|
|
[ res_con_of_op(res,o)
|
|
| o in active
|
|
],
|
|
res_cap[res])
|
|
endif endif
|
|
)
|
|
);
|
|
|
|
|
|
%% packing constraints
|
|
%% see Model::post_packing_constraints()
|
|
constraint
|
|
forall(k in index_set_1of2(packed_pq)) (
|
|
let {int: p = packed_pq[k,1],
|
|
int: q = packed_pq[k,2],
|
|
int: w = temp_width[single_temp(p)],
|
|
array[int] of int: modtab = [-1,-1]++[ if k=1 then v else v + w - 2*(v mod 2*w) endif
|
|
| v in 0..MAXR, k in 1..2
|
|
where v mod w = 0
|
|
],
|
|
int: nt = length(modtab) div 2,
|
|
} in
|
|
table([rt[p], rt[q]], array2d(1..nt, 1..2, modtab))
|
|
);
|
|
|
|
%% activators
|
|
constraint
|
|
forall(x in index_set(activator_insns))(
|
|
let {set of int: is = activator_insns[x],
|
|
set of int: os = activator_ops[x]} in (
|
|
(a[min(os)] <-> exists(o in 0..MAXO)(insn_in(o,op_instructions[o] intersect is))) /\
|
|
forall(i2 in os where i2>min(os))(a[i2] <-> a[min(os)])
|
|
)
|
|
);
|
|
|
|
%% prescheduling
|
|
constraint
|
|
forall(j in index_set(preschedule_op))(
|
|
let {int: oper = preschedule_op[j],
|
|
int: cycle = preschedule_cycle[j],
|
|
int: bb = min({k | k in index_set(bb_ops) where oper in bb_ops[k]}),
|
|
int: outop = max(bb_ops[bb])}
|
|
in (a[oper] -> c[oper] = cycle) /\
|
|
(a[oper] <-> c[outop] > cycle)
|
|
);
|
|
|
|
%% bypass
|
|
constraint
|
|
forall(j in index_set_1of2(bypass_table))(
|
|
let {int: o = bypass_table[j,1],
|
|
int: insn = bypass_table[j,2],
|
|
int: p = bypass_table[j,3]}
|
|
in insn_eq(o,insn) -> c[o] = ls_t(p)
|
|
);
|
|
|
|
%% exrelated
|
|
constraint
|
|
forall(j in index_set(exrelated_p))(
|
|
let {int: p = exrelated_p[j],
|
|
int: q = exrelated_q[j],
|
|
array[int] of int: ext = [exrelated_ext[r,k] | r in exrelated_rows[j], k in 1..2]}
|
|
in table([rt[p],rt[q]], array2d(1..(length(ext) div 2), 1..2, ext))
|
|
);
|
|
|
|
%% ad-hoc
|
|
constraint
|
|
forall(L in adhoc) (
|
|
eval_expr(L)
|
|
);
|
|
|
|
%% IMPLIED CONSTRAINTS
|
|
|
|
%% effective copy, handling multiple defs and/or uses
|
|
constraint
|
|
symmetry_breaking_constraint(
|
|
forall(o in 0..MAXO where op_type[o] = TYPE_COPY)(
|
|
let {int: src = min([p | p in op_operands[o] where operand_use[p]]),
|
|
int: dst = min([p | p in op_operands[o] where not operand_use[p]])} in
|
|
a[o] -> rt[src] != rt[dst]
|
|
)
|
|
);
|
|
|
|
%% dominating copies
|
|
constraint
|
|
symmetry_breaking_constraint(
|
|
forall(k in index_set(dominate_ing)) (
|
|
let {int: ing = dominate_ing[k],
|
|
int: ed = dominate_ed[k],
|
|
int: edsrc = min(op_operands[ed]),
|
|
set of int: iset = dominate_instructions[k],
|
|
set of int: tset = dominate_temps[k]} in (
|
|
a[ing] \/ not a[ed] \/ insn_in(ed,iset) \/ temp_in(edsrc,tset)
|
|
)
|
|
)
|
|
);
|
|
|
|
%% disjoint registers
|
|
constraint
|
|
redundant_constraint(
|
|
forall(R in diffreg) (
|
|
noverlap([rt[j] | j in R],
|
|
[temp_width[min(operand_temps[j])] | j in R])
|
|
)
|
|
);
|
|
|
|
%% different temporaries
|
|
constraint
|
|
redundant_constraint(
|
|
forall(T in difftemp) (
|
|
let {array[int] of int: TA = T} in
|
|
forall(j in index_set(TA), k in index_set(TA) where j<k)(
|
|
assert(operand_related(TA[j],TA[k]), "difftemp(\(T)) with unrelated operands")
|
|
) /\
|
|
smart_alldiff([y[p] | p in T])
|
|
)
|
|
);
|
|
|
|
%% nogoods
|
|
constraint
|
|
redundant_constraint(
|
|
forall(N in nogood) (
|
|
not eval_expr(N)
|
|
)
|
|
);
|
|
|
|
%% Model::post_connected_users_constraints
|
|
constraint
|
|
redundant_constraint(
|
|
forall(p in 0..MAXP where not operand_use[p])(
|
|
let {int: v = single_temp(p)} in (
|
|
if temp_must_be_real(p) then
|
|
temp_member_reif(temp_uses[v], v, true)
|
|
else if opt_in_temporary(v) then
|
|
let {var bool: rp}
|
|
in (temp_is_real_reif(p,rp)) /\
|
|
(temp_member_reif(temp_uses[v], v, rp))
|
|
else
|
|
temp_member_reif(temp_uses[v], v, a[operand_definer[p]])
|
|
endif endif
|
|
)
|
|
)
|
|
);
|
|
|
|
%% Model::post_connected_users_constraints
|
|
constraint
|
|
redundant_constraint(
|
|
forall(p in 0..MAXP where not operand_use[p])(
|
|
let {int: v = single_temp(p)} in (
|
|
if temp_must_be_real(p) then
|
|
member([rt[p] | p in temp_uses[v]], r[v])
|
|
else
|
|
member([rt[p] | p in temp_uses[v]]++[-1], r[v])
|
|
endif
|
|
)
|
|
)
|
|
);
|
|
|
|
%% disjoint live ranges projected on callee-saved regs
|
|
constraint
|
|
redundant_constraint(
|
|
forall(T in bb_temps) (
|
|
cumulative([ls[v] | v in T],
|
|
[ld[v] | v in T],
|
|
[temp_width[v]*bool2int(r[v] in calleesaved) | v in T],
|
|
card(calleesaved))
|
|
)
|
|
);
|
|
|
|
%% temp symmetry breaking among interchangeable temporaries in their potential use operands
|
|
constraint
|
|
symmetry_breaking_constraint(
|
|
forall(j in index_set(domop_operands)) (
|
|
value_precede_chain(domop_temps[j], [t(o) | o in domop_operands[j]])
|
|
)
|
|
);
|
|
|
|
%% before
|
|
constraint
|
|
redundant_constraint(
|
|
forall(j in index_set(before_pred)) (
|
|
let {int: p = before_pred[j],
|
|
int: q = before_succ[j],
|
|
expr: bc = before_cond[j]} in (
|
|
eval_expr(bc) -> operand_live_before(p,q)
|
|
)
|
|
)
|
|
);
|
|
|
|
%% active_table, tmp_table
|
|
constraint
|
|
redundant_constraint(
|
|
forall(E in table_exists_ops) (
|
|
exists(j in E)(a[j])
|
|
)
|
|
);
|
|
|
|
constraint
|
|
redundant_constraint(
|
|
forall(XOR in table_iffall_ops) (
|
|
let {int: j = min(XOR),
|
|
int: k = max(XOR)} in (
|
|
a[j] <-> a[k]
|
|
)
|
|
)
|
|
);
|
|
|
|
constraint
|
|
redundant_constraint(
|
|
forall(j in index_set(relation_ops)) (
|
|
let{set of int: ops = relation_ops[j],
|
|
set of int: temps = relation_temps[j],
|
|
int: nt = relation_ntuples[j],
|
|
set of int: range = relation_range[j],
|
|
set of int: irange = 1..(card(ops)+card(temps)),
|
|
array[irange] of var int: vars = [bool2int(a[j]) | j in ops]++
|
|
[t(j) | j in temps]} in (
|
|
table(vars, array2d(1..nt,irange,[ints[j] | j in range]))
|
|
)
|
|
)
|
|
);
|
|
|
|
%% combine
|
|
constraint
|
|
redundant_constraint(
|
|
forall(o in 0..MAXO where op_type[o] = TYPE_COMBINE)(
|
|
let {array[int] of int: opnds = [x | x in op_operands[o]],
|
|
int: src1 = opnds[1],
|
|
int: src2 = opnds[2],
|
|
int: def = opnds[3]} in (
|
|
minimum(ls_t(def), [le_t(src1), le_t(def)]) /\
|
|
minimum(ls_t(def), [le_t(src2), le_t(def)])
|
|
)
|
|
)
|
|
);
|
|
|
|
%% low/high
|
|
constraint
|
|
redundant_constraint(
|
|
forall(o in 0..MAXO where op_type[o] in {TYPE_HIGH, TYPE_LOW})(
|
|
let {int: src = min(op_operands[o]),
|
|
int: def = max(op_operands[o])} in (
|
|
minimum(ls_t(def), [le_t(src), le_t(def)])
|
|
)
|
|
)
|
|
);
|
|
|
|
%% useless memory stores
|
|
constraint
|
|
symmetry_breaking_constraint(
|
|
forall(T in related_temps) (
|
|
sum([bool2int(r[v] in infinite) | v in T]) <= 1
|
|
)
|
|
);
|
|
|
|
%% across
|
|
constraint
|
|
redundant_constraint(
|
|
forall(j in index_set(across_op)) (
|
|
let {int: opi = across_op[j],
|
|
int: maxwidth = max(temp_width),
|
|
set of int: regs = across_regs[j],
|
|
set of int: items = across_items[j],
|
|
array[items] of int: cand =
|
|
array1d(items, [across_item_temp[k] | k in items]),
|
|
array[items] of var bool: active,
|
|
array[items] of var -maxwidth*(MAXT+1)..MAXR: selected,
|
|
array[int] of var int: allreg =
|
|
[x | x in callersaved] ++ [x | x in regs] ++ selected,
|
|
array[int] of int: allwidth =
|
|
[1 | x in callersaved] ++
|
|
[1 | x in regs] ++
|
|
[temp_width[cand[k]] | k in items]} in (
|
|
forall(k in items)(
|
|
let {int: ck = cand[k]} in (
|
|
( active[k] <->
|
|
eval_expr(across_item_cond[k]) \/
|
|
(ls[ck] <= c[opi] /\ c[opi] < le[ck])) /\
|
|
selected[k] = ite(active[k], r[ck], -maxwidth*(ck+1))
|
|
)
|
|
) /\
|
|
noverlap(allreg, allwidth)
|
|
)
|
|
)
|
|
);
|
|
|
|
%% set_across
|
|
constraint
|
|
redundant_constraint(
|
|
forall(j in index_set(setacross_op)) (
|
|
let {int: opi = setacross_op[j],
|
|
set of int: regs = setacross_regs[j],
|
|
set of int: itemsset = setacross_tempsets[j],
|
|
set of int: items = 1..card(itemsset),
|
|
array[items] of set of int: cands = [sets[it] | it in itemsset],
|
|
array[items] of var 0..MAXR: selected,
|
|
array[items] of var 0..max(temp_width): width,
|
|
array[int] of var int: allreg =
|
|
[x | x in callersaved] ++ [x | x in regs] ++ selected,
|
|
array[int] of var int: allwidth =
|
|
[1 | x in callersaved] ++ [1 | x in regs] ++ width} in (
|
|
forall(it in items)(
|
|
let {set of int: cit = cands[it],
|
|
array[int] of int: ws = [temp_width[k] | k in cit],
|
|
array[int] of var int: rs = [r[k] | k in cit],
|
|
array[int] of var int: lss = [ls[k] | k in cit],
|
|
array[int] of var int: les = [le[k] | k in cit],
|
|
var 1..card(cit): k} in (
|
|
width[it] = if min(ws) < max(ws) then ws[k] else min(ws) endif /\
|
|
selected[it] = rs[k] /\
|
|
lss[k] <= c[opi] /\ c[opi] < les[k]
|
|
)
|
|
) /\
|
|
noverlap(allreg, allwidth)
|
|
)
|
|
)
|
|
);
|
|
|
|
%% spill callee-saved if and only if some temp interfers with it
|
|
constraint
|
|
symmetry_breaking_constraint(
|
|
if card(index_set(calleesaved_spill))>0 then
|
|
let {int: nrows = card(index_set_1of2(cs_spill_transpose)),
|
|
int: ncols = card(index_set_2of2(cs_spill_transpose)),
|
|
set of int: css_ops = {cs_spill_transpose[j,k] | j in 1..nrows, k in 1..ncols},
|
|
set of int: preass_ops = {o | o in 0..MAXO where op_type[o] in {TYPE_IN,TYPE_CALL,TYPE_TAIL,TYPE_FUN}},
|
|
set of int: tcands = {o | o in 0..MAXT where not (temp_definer[o] in css_ops union preass_ops)}} in (
|
|
forall(j in 1..ncols) (
|
|
let {int: theop = cs_spill_transpose[1,j],
|
|
int: thepu = min(op_operands[theop]),
|
|
int: thetu = single_temp(thepu),
|
|
int: thepd = temp_def[thetu],
|
|
int: thea = min(k in index_set(preassign_reg) where preassign_operand[k]=thepd)(preassign_reg[k]),
|
|
int: thew = temp_width[thetu]} in (
|
|
a[theop] <-> exists(ti in tcands)(r[ti]+temp_width[ti] > thea /\ r[ti] in 0..thea+thew-1)
|
|
)
|
|
)
|
|
)
|
|
else true endif
|
|
);
|
|
|
|
%% break symmetries among which callee-saved to spill
|
|
constraint
|
|
symmetry_breaking_constraint(
|
|
if card(index_set(calleesaved_spill))>0 then
|
|
forall(j in index_set(calleesaved_spill)) (
|
|
let {set of int: cgr = calleesaved_spill[j],
|
|
int: cur = min(cgr)} in (
|
|
forall(x in cgr where x>cur) (a[cur] <-> a[x])
|
|
)
|
|
) /\
|
|
let {int: nrows = card(index_set_1of2(cs_spill_transpose)),
|
|
int: ncols = card(index_set_2of2(cs_spill_transpose)),
|
|
set of int: spill = if nrows>=1 then {cs_spill_transpose[1,j] | j in 1..ncols}
|
|
else {} endif,
|
|
set of int: unspill = if nrows>=2 then {cs_spill_transpose[2,j] | j in 1..ncols}
|
|
else {} endif} in (
|
|
decreasing([a[cs_spill_transpose[1,k]] | k in 1..ncols]) /\
|
|
forall(k in 2..ncols)(
|
|
a[cs_spill_transpose[1,k]] -> c[cs_spill_transpose[1,k-1]] <= c[cs_spill_transpose[1,k]]
|
|
) /\
|
|
if spill subset bb_ops[1] /\ unspill subset bb_ops[1] then
|
|
forall(k in 1..ncols)(
|
|
let {int: u = cs_spill_transpose[2,k],
|
|
int: v = cs_spill_transpose[1,k]} in (
|
|
a[u] -> c[v] < c[u]
|
|
)
|
|
)
|
|
else true endif
|
|
)
|
|
else true endif
|
|
);
|
|
|
|
%% IMPORTED FROM Model::
|
|
|
|
%% Model::post_minimum_temporary_duration_constraints
|
|
constraint
|
|
redundant_constraint(
|
|
forall(o in 0..MAXO, dp in op_operands[o] where not operand_use[dp])(
|
|
let {int: v = single_temp(dp)} in
|
|
(temp_eq(dp,v) -> ld[v] >= temp_minlive[v]) /\
|
|
forall(up in temp_uses[v])(temp_eq(up,v) -> ld[v] >= lat(up,v))
|
|
)
|
|
);
|
|
|
|
%% Model::post_define_issue_cycle_constraints
|
|
constraint
|
|
symmetry_breaking_constraint(
|
|
forall(o in 0..MAXO where op_type[o]=TYPE_DEFINE)(
|
|
let {set of int: js = {operand_definer[q] | p in op_operands[o],
|
|
v in {single_temp(p)},
|
|
q in temp_uses[v]},
|
|
array[int] of var int: lats = [lat(q,v) | p in op_operands[o],
|
|
v in {single_temp(p)},
|
|
q in temp_uses[v]]} in
|
|
if card(js) = 1 then
|
|
c[min(js)] = c[o] + max(lats)
|
|
else true endif
|
|
)
|
|
);
|
|
|
|
%% DOMINATION: live range of temp occurring in (kill)
|
|
predicate kill_live_range(int: v) =
|
|
(ld[v] = lt[temp_def[v]]);
|
|
|
|
%% Model::post_kill_issue_cycle_constraints
|
|
constraint
|
|
symmetry_breaking_constraint(
|
|
forall(o2 in 0..MAXO where op_type[o2] = TYPE_KILL)(
|
|
if op_mand[o2] then % e.g. after function call, multiple operands
|
|
let {array[int] of var int: lats = [lat(q,v) | q in op_operands[o2],
|
|
v in {single_temp(q)}],
|
|
array[int] of int: ts = [v | q in op_operands[o2],
|
|
v in {single_temp(q)}],
|
|
set of int: o1s = {temp_definer[v] | q in op_operands[o2],
|
|
v in {single_temp(q)}},
|
|
} in
|
|
forall(v in ts)(kill_live_range(v)) /\
|
|
c[o2] = c[min(o1s)] + max(lats)
|
|
else % e.g. after move subject to pack, one operand, multiple temps
|
|
let {int: q1 = min(op_operands[o2]),
|
|
int: p1 = temp_def[single_temp(q1)],
|
|
set of int: o1s = {temp_definer[v] | v in real_temps(q1)},
|
|
array[int] of var int: issue = [-1] ++ [c[temp_definer[v]] + lat(q1,v) | v in real_temps(q1)],
|
|
} in
|
|
card(op_operands[o2]) = 1 /\ % sanity check
|
|
forall(v in real_temps(q1))(kill_live_range(v)) /\
|
|
c[o2] = issue[y[q1]] /\
|
|
if card(real_temps(q1))=1 then
|
|
same_temp(p1,q1) /\ rt[p1] = rt[q1]
|
|
else
|
|
sum(o in o1s)(a[o]) <= 1
|
|
endif
|
|
endif
|
|
)
|
|
);
|
|
|
|
%% domination constraint for slack, in fact make it a functional dependency
|
|
constraint
|
|
symmetry_breaking_constraint(
|
|
forall(j in index_set_1of2(long_latency_index))(
|
|
let {set of int: inps = long_latency_index[j,1],
|
|
set of int: inix = long_latency_index[j,2],
|
|
set of int: outps = long_latency_index[j,3],
|
|
set of int: outix = long_latency_index[j,4],
|
|
array[int] of var int: inubs = [ if temp_eq(q,single_temp(p)) then
|
|
c[operand_definer[q]] - lt[q] - s[q] - lt[p]
|
|
else MAXL endif
|
|
| i in inix,
|
|
p in [long_latency_def[i]],
|
|
q in [long_latency_use[i]]
|
|
],
|
|
array[int] of var int: outubs = [ if temp_eq(q,single_temp(p)) then
|
|
ld[single_temp(p)] - lt[q] - lt[p] - s[p]
|
|
else MAXL endif
|
|
| i in outix,
|
|
p in [long_latency_def[i]],
|
|
q in [long_latency_use[i]]
|
|
]} in
|
|
assert((card(inps)>0 /\ card(outps)>0), "invalid long_latency item") /\
|
|
let {var int: outlb = if length( inubs)>0 then -min( inubs) else -MAXL endif,
|
|
var int: outub = if length(outubs)>0 then min(outubs) else MAXL endif} in
|
|
outlb <= outub /\
|
|
forall(p in outps)(s[p] = min(outub,max(outlb,0)))
|
|
)
|
|
);
|
|
|
|
%% domination constraint: sequential schedule as a makespan UB
|
|
%% Model::post_sequential_upper_bound_constraints
|
|
constraint
|
|
symmetry_breaking_constraint(
|
|
forall(bb in index_set(bb_ops))(
|
|
let {set of int: os = bb_ops[bb],
|
|
array[os] of var 0..MAXC: wc = array1d(os, [o_wcet(o) | o in os])}
|
|
in c[max(os)] <= sum(o in os)(wc[o])
|
|
)
|
|
);
|
|
|
|
var 0..MAXC: o_wcet(0..MAXO: o) =
|
|
let {array[int] of var int: wcs = [wcet[jj,3] | jj in index_set_1of2(wcet) where wcet[jj,1] = o],
|
|
int: nwcs = length(wcs)}
|
|
in if forall(jj in 1..nwcs)(wcs[jj] = 1)
|
|
then a[o]
|
|
else if not op_mand[o] /\ forall(jj in 2..nwcs)(wcs[jj] = 1)
|
|
then a[o]
|
|
else
|
|
wcs[ii[o]]
|
|
endif endif;
|
|
|
|
%% output
|
|
|
|
%------------------------------------------------------------------------------
|
|
% Solve item
|
|
|
|
solve
|
|
:: seq_search([
|
|
seq_search([
|
|
int_search(
|
|
[y[p] | p in bb_operands[b] where operand_use[p] /\ op_mand[operand_definer[p]]],
|
|
first_fail, indomain_min, complete
|
|
)
|
|
] ++ [
|
|
int_search(
|
|
[0] ++ [y[p] | p in bb_operands[b] where operand_use[p] /\ not op_mand[operand_definer[p]]],
|
|
first_fail, indomain_min, complete
|
|
)
|
|
])
|
|
| b in bb_order
|
|
] ++ [
|
|
int_search([ii[o] | o in bb_ops[b]], input_order, indomain_min, complete)
|
|
| b in bb_order
|
|
] ++ [
|
|
seq_search([
|
|
int_search([c[max(bb_ops[b])]], input_order, indomain_min, complete),
|
|
int_search([c[o] | o in bb_ops[b]], smallest, indomain_min, complete)
|
|
])
|
|
| b in bb_order
|
|
] ++ [
|
|
int_search(
|
|
[r[t] | t in bb_temps[b] where op_type[temp_definer[t]] != TYPE_IN]++[0],
|
|
first_fail, indomain_min, complete
|
|
)
|
|
| b in bb_order
|
|
])
|
|
minimize objective;
|
|
|
|
%------------------------------------------------------------------------------
|
|
% Output item
|
|
|
|
output [
|
|
"c = array1d(0..\(MAXO), \(c));\n",
|
|
"ii = array1d(0..\(MAXO), \(ii));\n",
|
|
"y = array1d(0..\(MAXP), \(y));\n",
|
|
"r = array1d(-1..\(MAXT), \(r));\n",
|
|
"objective = \(objective);\n"
|
|
];
|
|
%++
|
|
% ["\"cost\": "] ++ [show(objective)] ++ ["\n"] ++
|
|
% ["\"cycles\": "] ++ [show(c)] ++ ["\n"] ++
|
|
% ["\"instructions\": "] ++ [show([op_instructions[o][fix(ii[o])] | o in 0..MAXO])] ++ ["\n"] ++
|
|
% ["\"temporaries\": "] ++ [show([operand_temps[p][fix(y[p])] | p in 0..MAXP])] ++ ["\n"] ++
|
|
% ["\"registers\": "] ++ [show([r[v] | v in 0..MAXT])] ++ ["\n"] ++
|
|
% ["\"live start\": "] ++ [show([ls[v] | v in 0..MAXT])] ++ ["\n"] ++
|
|
% ["\"live duration\": "] ++ [show([ld[v] | v in 0..MAXT])] ++ ["\n"] ++
|
|
% ["\"live end\": "] ++ [show([le[v] | v in 0..MAXT])] ++ ["\n"];
|
|
|