1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2% Copyright (c) 2013, University of Washington.
3% All rights reserved.
4%
5% This file is distributed under the terms in the attached LICENSE file.
6% If you do not find this file, copies can be found by writing to:
7% ETH Zurich D-INFK, Universitaetstrasse 6, CH-8092 Zurich. Attn: Systems Group.
8%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
9
10% This file fakes the machine config for 'bigfish' at UW. I got it
11% from running Barrelfish input to ECLiPSe on Linux and dumping the
12% result in here.
13%
14% It does a few checks to see that the machine it's running on is in
15% fact the same version of bigfish. It does so by evaluating a few
16% facts that should be inserted in the database. I got the facts by
17% running:
18%
19% sed -ne 's/assert(\(.*\))\./        \1,/p' bigfish.cmds > bigfish.facts
20%
21% And then inserting bigfish.facts into the beginning of
22% bridge_programming/2. The first time this actually blew the stack
23% of the SKB, so I removed all unneccessary things and kept only
24% things relevant to PCI bridge programming.
25
26:-lib(ic).
27:-lib(ic_global).
28:-use_module(library(ic_edge_finder)).
29
30:- set_flag(print_depth, 200).
31
32:-dynamic(currentbar/5).
33
34% :-include("../data/data_hand.txt").
35% :-include("../data/data_qemu_hand.txt").
36% :-include("../data/data_qemu.txt").
37% :-include("../data/data_nos3.txt").
38% :-include("../data/data_nos4.txt").
39% :-include("../data/data_nos5.txt").
40% :-include("../data/data_nos6.txt").
41% :-include("../data/data_gruyere.txt").
42% :-include("../data/data_sbrinz1.txt").
43% :-include("../data/data_loner.txt").
44
45
46
47%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
48% main goal to be called from outside
49%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
50
51bridge_programming(Plan, NrElements) :-
52        ioapic(0,4273995776,0),
53        memory_region(4273995776,12,4096, 6,0),
54        ioapic(1,4274520064,24),
55        memory_region(4274520064,12,4096, 6,0),
56        ioapic(2,4274782208,56),
57        memory_region(4274782208,12,4096, 6,0),
58        fixed_memory(4274585600,4274601984),
59        fixed_memory(4274847744,4274864128),
60        rootbridge_address_window(addr(0, 0, 0), mem(655360, 786431)),
61        rootbridge_address_window(addr(0, 0, 0), mem(4273995776, 4274520063)),
62        rootbridge_address_window(addr(0, 0, 0), mem(4274520064, 4274782207)),
63        rootbridge_address_window(addr(0, 0, 0), mem(3925868544, 4016046079)),
64        rootbridge_address_window(addr(0, 0, 0), mem(3917479936, 3925868543)),
65        rootbridge_address_window(addr(0, 0, 0), mem(4275306496, 4275326975)),
66        rootbridge(addr(0,0,0),childbus(0,30),mem(3925868544,4016046079)),
67        rootbridge_address_window(addr(32, 0, 0), mem(4274782208, 4275044351)),
68        rootbridge_address_window(addr(32, 0, 0), mem(3900702720, 3917479935)),
69        rootbridge(addr(32,0,0),childbus(32,62),mem(3900702720,3917479935)),
70        memory_affinity(0, 655360, 0),
71        memory_affinity(1048576, 3220176896, 0),
72        memory_affinity(4294967296, 1073741824, 0),
73        memory_affinity(5368709120, 4294967296, 1),
74        bridge(pcie,addr(0,2,0),4098,23062,6,4,0, secondary(1)),
75        bridge(pcie,addr(0,4,0),4098,23064,6,4,0, secondary(3)),
76        bridge(pcie,addr(3,0,0),4277,34340,6,4,0, secondary(4)),
77        bar(addr(3, 0, 0), 0, 16'ef2e0000, 16'20000, mem, nonprefetchable, 32),
78        bridge(pcie,addr(4,0,0),4277,34340,6,4,0, secondary(5)),
79        NrElements = 41,
80        Plan = [[buselement(device, addr(1, 0, 0), 0, 3925868544, 3959422976, 33554432, mem, nonprefetchable, pcie, 64), buselement(device, addr(1, 0, 1), 0, 3959422976, 3992977408, 33554432, mem, nonprefetchable, pcie, 64), buselement(device, addr(9, 0, 0), 0, 3992977408, 3993501696, 524288, mem, nonprefetchable, pcie, 64), buselement(device, addr(9, 0, 1), 0, 3993501696, 3994025984, 524288, mem, nonprefetchable, pcie, 64), buselement(device, addr(5, 0, 0), 3, 3995074560, 3995336704, 262144, mem, nonprefetchable, pcie, 64), buselement(device, addr(5, 0, 0), 1, 3995336704, 3995402240, 65536, mem, nonprefetchable, pcie, 64), buselement(device, addr(9, 0, 0), 4, 3994025984, 3994042368, 16384, mem, nonprefetchable, pcie, 64), buselement(device, addr(9, 0, 1), 4, 3994042368, 3994058752, 16384, mem, nonprefetchable, pcie, 64), buselement(device, addr(0, 17, 0), 5, 3996123136, 3996127232, 4096, mem, nonprefetchable, pcie, 32), buselement(bridge, addr(0, 20, 4), secondary(10), 3925868544, 3925868544, 0, mem, nonprefetchable, pcie, 0), buselement(bridge, addr(0, 9, 0), secondary(9), 3992977408, 3995074560, 2097152, mem, nonprefetchable, pcie, 0), buselement(bridge, addr(4, 5, 0), secondary(8), 3995074560, 3995074560, 0, mem, nonprefetchable, pcie, 0), buselement(bridge, addr(4, 4, 0), secondary(7), 3995074560, 3995074560, 0, mem, nonprefetchable, pcie, 0), buselement(bridge, addr(4, 1, 0), secondary(6), 3995074560, 3995074560, 0, mem, nonprefetchable, pcie, 0), buselement(bridge, addr(4, 0, 0), secondary(5), 3995074560, 3996123136, 1048576, mem, nonprefetchable, pcie, 0), buselement(bridge, addr(3, 0, 0), secondary(4), 3995074560, 3996123136, 1048576, mem, nonprefetchable, pcie, 0), buselement(bridge, addr(0, 4, 0), secondary(3), 3995074560, 3996123136, 1048576, mem, nonprefetchable, pcie, 0), buselement(bridge, addr(0, 3, 0), secondary(2), 3925868544, 3925868544, 0, mem, nonprefetchable, pcie, 0), buselement(bridge, addr(0, 2, 0), secondary(1), 3925868544, 3992977408, 67108864, mem, nonprefetchable, pcie, 0), buselement(bridge, addr(0, 20, 4), secondary(10), 3925868544, 3925868544, 0, mem, prefetchable, pcie, 0), buselement(bridge, addr(0, 9, 0), secondary(9), 3925868544, 3925868544, 0, mem, prefetchable, pcie, 0), buselement(bridge, addr(4, 5, 0), secondary(8), 3925868544, 3925868544, 0, mem, prefetchable, pcie, 0), buselement(bridge, addr(4, 4, 0), secondary(7), 3925868544, 3925868544, 0, mem, prefetchable, pcie, 0), buselement(bridge, addr(4, 1, 0), secondary(6), 3925868544, 3925868544, 0, mem, prefetchable, pcie, 0), buselement(bridge, addr(4, 0, 0), secondary(5), 3925868544, 3925868544, 0, mem, prefetchable, pcie, 0), buselement(bridge, addr(3, 0, 0), secondary(4), 3925868544, 3925868544, 0, mem, prefetchable, pcie, 0), buselement(bridge, addr(0, 4, 0), secondary(3), 3925868544, 3925868544, 0, mem, prefetchable, pcie, 0), buselement(bridge, addr(0, 3, 0), secondary(2), 3925868544, 3925868544, 0, mem, prefetchable, pcie, 0), buselement(bridge, addr(0, 2, 0), secondary(1), 3925868544, 3925868544, 0, mem, prefetchable, pcie, 0)], [buselement(device, addr(33, 0, 0), 1, 3900702720, 3904897024, 4194304, mem, nonprefetchable, pcie, 32), buselement(device, addr(33, 0, 1), 1, 3904897024, 3909091328, 4194304, mem, nonprefetchable, pcie, 32), buselement(device, addr(33, 0, 0), 0, 3909091328, 3909222400, 131072, mem, nonprefetchable, pcie, 32), buselement(device, addr(33, 0, 1), 0, 3909222400, 3909353472, 131072, mem, nonprefetchable, pcie, 32), buselement(device, addr(33, 0, 0), 3, 3909353472, 3909369856, 16384, mem, nonprefetchable, pcie, 32), buselement(device, addr(33, 0, 1), 3, 3909369856, 3909386240, 16384, mem, nonprefetchable, pcie, 32), buselement(bridge, addr(32, 11, 0), secondary(35), 3900702720, 3900702720, 0, mem, nonprefetchable, pcie, 0), buselement(bridge, addr(32, 3, 0), secondary(34), 3900702720, 3900702720, 0, mem, nonprefetchable, pcie, 0), buselement(bridge, addr(32, 2, 0), secondary(33), 3900702720, 3910139904, 9437184, mem, nonprefetchable, pcie, 0), buselement(bridge, addr(32, 11, 0), secondary(35), 3900702720, 3900702720, 0, mem, prefetchable, pcie, 0), buselement(bridge, addr(32, 3, 0), secondary(34), 3900702720, 3900702720, 0, mem, prefetchable, pcie, 0), buselement(bridge, addr(32, 2, 0), secondary(33), 3900702720, 3900702720, 0, mem, prefetchable, pcie, 0)]].
81
82%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
83% small tools
84%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
85
86adjust_range(X, buselement(T,A,Sec,B1,H1,S,Tp,PF, PCIe, Bits), buselement(T,A,Sec,B2,H2,S,Tp,PF, PCIe, Bits)) :-
87    B2 is B1 + X,
88    H2 is H1 + X.
89
90back_to_bytes(Granularity, buselement(T,A,Sec,BP,HP,SP,Tp,PF, PCIe, Bits), buselement(T,A,Sec,B,H,S,Tp,PF, PCIe, Bits)) :-
91    B is BP * Granularity,
92    H is HP * Granularity,
93    S is SP * Granularity.
94
95
96%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
97% the main part of the allocation. Called once per root bridge
98%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
99
100bridge_assignment(Plan, Root, Granularity, ExclRanges, IOAPICs) :-
101    root(Addr,childbus(MinBus,MaxBus),mem(LMem,HMem)) = Root,
102    X is HMem - LMem,
103    Type = mem,
104
105% prefetchable
106    constrain_bus(Granularity, Type, prefetchable, Addr,MinBus,MaxBus,LMem,HMem,BusElementListP),
107    RBaseP::[LMem..HMem],
108    RHighP::[LMem..HMem],
109    RSizeP::[0..X],
110    devicetree(BusElementListP,buselement(bridge,Addr,secondary(MinBus),RBaseP,RHighP,RSizeP, Type, prefetchable, _, _),TP),
111
112% nonprefetchable
113    constrain_bus(Granularity, Type, nonprefetchable, Addr,MinBus,MaxBus,LMem,HMem,BusElementListNP),
114    RBaseNP::[LMem..HMem],
115    RHighNP::[LMem..HMem],
116    RSizeNP::[0..X],
117    devicetree(BusElementListNP,buselement(bridge,Addr,secondary(MinBus),RBaseNP,RHighNP,RSizeNP, Type, nonprefetchable, _, _),TNP),
118
119% pseudo-root of both trees
120    PseudoBase::[LMem..HMem],
121    PseudoHigh::[LMem..HMem],
122    PseudoSize::[0..X],
123    T = t(buselement(bridge, addr(-1, -1, -1), childbus(-1, -1), PseudoBase, PseudoHigh, PseudoSize, _, _, _, _), [TP, TNP]),
124    setrange(T,_,_,_),
125    nonoverlap(T),
126    naturally_aligned(T, 256, LMem, HMem),
127    tree2list(T,ListaU),
128    sort(6, >=, ListaU, Lista),
129    not_overlap_memory_ranges(Lista, ExclRanges),
130    keep_orig_addr(Lista, 12, 3, _, _, _, _),
131    keep_ioapic_bars(Lista, IOAPICs),
132    labelall(Lista),
133    subtract(Lista,[buselement(bridge,Addr,_,_,_,_,_,prefetchable,_,_)],Pl3),
134    subtract(Pl3,[buselement(bridge,Addr,_,_,_,_,_,nonprefetchable,_,_)],Pl2),
135    subtract(Pl2,[buselement(bridge,addr(-1,-1,-1),_,_,_,_,_,_,_,_)],Pl),
136    maplist(adjust_range(0),Pl,PR),
137    maplist(back_to_bytes(Granularity),PR,Plan).
138
139% dot output:
140%    PrBaseBytePref is RBaseP * Granularity,
141%    PrHighBytePref is RHighP * Granularity,
142%    PrBaseByteNonPref is RBaseNP * Granularity,
143%    PrHighByteNonPref is RHighNP * Granularity,
144%    plan_to_dot(Granularity, Plan, Root, PrBaseBytePref, PrHighBytePref, PrBaseByteNonPref, PrHighByteNonPref).
145
146
147%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
148% instantiating the variables
149%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
150
151base(buselement(_,_,_,Base,_,_,_,_,_,_),Base).
152high(buselement(_,_,_,_,High,_,_,_,_,_),High).
153size(buselement(_,_,_,_,_,Size,_,_,_,_),Size).
154
155labelall(BusElementList) :-
156    maplist(base, BusElementList, Base),
157    maplist(high, BusElementList, High),
158    maplist(size, BusElementList, Size),
159    append(Base, High, L1),
160    append(L1, Size, L2),
161    labeling(L2).
162
163
164
165%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
166% create the list of devices and bridges in form of buselements and create the
167% variables.
168% we care about the allocation of memory mapped registers here, therefore we only
169% look at bar located in "mem", not "io"
170%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
171
172constrain_bus(Granularity, Type, Prefetch, RootAddr,Bus,MaxBus,LMem,HMem,OutBusElementList) :-
173    constrain_bus_ex(Granularity, Type, Prefetch, RootAddr,Bus,MaxBus,LMem,HMem,[],OutBusElementList).
174
175constrain_bus_ex(_, _, _, _,Bus,MaxBus,_,_,InL,InL) :- Bus > MaxBus.
176constrain_bus_ex(Granularity, Type, Prefetch, RootAddr,Bus,MaxBus,LMem,HMem,InBusElementList,OutBusElementList) :-
177    Bus =< MaxBus,
178    SMax is HMem - LMem,
179    ( is_predicate(bridge/8) ->
180	    findall(buselement(bridge,addr(Bus,Dev,Fun),secondary(Sec),Base,High,Size,Type,Prefetch, PCIe, 0),
181	            ( bridge(PCIe, addr(Bus,Dev,Fun), _, _, _, _, _, secondary(Sec)),
182	              not addr(Bus,Dev,Fun) = RootAddr,
183	              Base::[LMem..HMem],High::[LMem..HMem],Size::[0..SMax]
184	            ),BridgeList);
185        BridgeList = []
186    ),
187    ( is_predicate(device/8) ->
188	    findall(buselement(device,addr(Bus,Dev,Fun),BAR,Base,High,SizeP,Type,Prefetch, PCIe, Bits),
189	            ( device(PCIe, addr(Bus,Dev,Fun),_,_,_,_,_,_),
190	              bar(addr(Bus,Dev,Fun),BAR,_,Size, Type, Prefetch, Bits),
191	              Base::[LMem..HMem],High::[LMem..HMem],
192	              ST1 is Size / Granularity,
193	              ceiling(ST1, ST2),
194	              integer(ST2, SizeP)
195	            ),DeviceList);
196        DeviceList = []
197    ),
198    append(BridgeList, DeviceList, MyBusElementList),
199    append(InBusElementList, MyBusElementList, NewBusElementList),
200    NextBus is Bus + 1,
201    constrain_bus_ex(Granularity, Type, Prefetch, RootAddr, NextBus, MaxBus, LMem,HMem,NewBusElementList,OutBusElementList).
202
203
204%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
205% create the PCI(e) device tree from a list of "buselement" and return it in Tree
206%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
207
208devicetree(List,CurrRoot,Tree) :-
209    buselement(bridge,_,secondary(Sec),_,_,_,_,_,_,_) = CurrRoot,
210    findall(X,(
211               member(Y,List),
212               buselement(_,addr(Sec,_,_),_,_,_,_,_,_,_,_) = Y,
213               devicetree(List, Y, X)),Children
214           ),
215    Tree = t(CurrRoot,Children).
216devicetree(_,CurrRoot,Tree) :-
217    buselement(device,_,_,_,_,_,_,_,_,_) = CurrRoot,
218    Tree = t(CurrRoot, []).
219
220
221%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
222% convert a tree to a list of buselements
223%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
224
225tree2list([],[]).
226tree2list(Tree, List) :-
227    t(Node,Children) = Tree,
228    ( foreach(El,Children),
229      foreach(L1,ChildList)
230      do
231        tree2list(El,L1)
232    ),
233    flatten(ChildList,L2),
234    List = [Node|L2].
235
236
237
238%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
239% store the new values of the BARs
240%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
241replace_current_BAR_values(L) :-
242    delete_current_BAR_values(L),
243    store_current_BAR_values(L).
244
245store_current_BAR_values([]).
246store_current_BAR_values([H|T]) :-
247    ( buselement(device,Addr,BAR,Base,High,Size,_,_,_,_) = H ->
248         assert(currentbar(Addr,BAR,Base,High,Size));
249        true
250    ),
251    store_current_BAR_values(T).
252
253
254delete_current_BAR_values([]).
255delete_current_BAR_values([H|T]) :-
256    ( buselement(device,Addr,BAR,_,_,_,_,_,_,_) = H ->
257        ( currentbar(Addr,BAR,_,_,_) ->
258            retract(currentbar(Addr,BAR,_,_,_));
259            true
260        );
261        true
262    ),
263    delete_current_BAR_values(T).
264
265
266
267
268%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
269% add constraints to the tree
270%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
271
272% make sure that the bridge has a range which includes all the children
273setrange(Tree,SubTreeSize,SubTreeMin,SubTreeMax) :-
274    t(Node,Children) = Tree,
275    ( foreach(El,Children),
276      foreach(Sz,SizeList),
277      foreach(Mi,MinList),
278      foreach(Ma,MaxList)
279      do
280        setrange(El,Sz,Mi,Ma)
281    ),
282    ic_global:sumlist(SizeList,Size),
283    buselement(_,_,_,Base,High,ElemSize,_,_,_,_) = Node,
284    ElemSize $>= Size,
285    ( not MinList=[] ->
286        ic:minlist(MinList,Min),
287        ic:maxlist(MaxList,Max),
288        Min $>= Base,
289        Max $=< High;
290        true
291    ),
292    High $= Base + ElemSize,
293    SubTreeSize $= ElemSize,
294    SubTreeMin $= Base,
295    SubTreeMax $= High.
296setrange([],0,_,_).
297
298
299% make sure that the children do not overlap
300child(t(C,_),C).
301nonoverlap(Tree) :-
302    t(_ ,Children) = Tree,
303    maplist(child,Children,ChildList),
304    ( not ChildList=[] ->
305        maplist(base,ChildList,Base),
306        maplist(size,ChildList,Size),
307        disjunctive(Base,Size);
308        true
309    ),
310    ( foreach(El, Children)
311      do
312        nonoverlap(El)
313    ).
314
315
316naturally_aligned(Tree, BridgeAlignment, LMem, HMem) :-
317    t(Node,Children) = Tree,
318    ( buselement(device,_,_,Base,High,Size,_,_,_,_) = Node ->
319      Divisor is Size
320      ;
321      buselement(bridge,_,_,Base,High,_,_,_,_,_) = Node ->
322      Divisor is BridgeAlignment
323    ),
324
325    T1 is (HMem - LMem) / Divisor,
326    ceiling(T1, T2),
327    integer(T2, Nr),
328    N::[0..Nr],
329    N2::[0..Nr],
330    mod(LMem,Divisor,Remainder),
331    ( Remainder =:= 0 ->
332        Corr is 0;
333        Corr is Divisor - Remainder
334    ),
335    Base $= N*Divisor + LMem + Corr,
336    High $>= Base,
337    High $= N2*Divisor + LMem + Corr,
338    ( foreach(El, Children),
339      param(BridgeAlignment),
340      param(LMem),
341      param(HMem)
342      do
343        naturally_aligned(El, BridgeAlignment, LMem, HMem)
344    ).
345
346
347% do not overlap with the given list of memory ranges
348not_overlap_memory_ranges([], _).
349not_overlap_memory_ranges(_, []).
350not_overlap_memory_ranges([buselement(bridge,_,_,_,_,_,_,_,_,_)|PCIList], MemoryRanges) :-
351    not_overlap_memory_ranges(PCIList, MemoryRanges).
352not_overlap_memory_ranges([H|PCIList], MemoryRanges) :-
353    ( foreach(range(RBase,RSize),MemoryRanges),
354      param(H)
355      do
356      buselement(device,_,_,Base,_,Size,_,_,_,_) = H,
357      append([Base],[RBase],Bases),
358      append([Size],[RSize],Sizes),
359      disjunctive(Bases,Sizes)
360    ),
361    not_overlap_memory_ranges(PCIList, MemoryRanges).
362
363
364keep_orig_addr([], _, _, _, _, _, _).
365keep_orig_addr([H|Buselements], Class, SubClass, ProgIf, Bus, Dev, Fun) :-
366    ( buselement(device,addr(Bus,Dev,Fun),BAR,Base,_,_,_,_,_,_) = H,device(_,addr(Bus,Dev,Fun),_,_,Class, SubClass, ProgIf,_),bar(addr(Bus,Dev,Fun),BAR,OrigBase,_,_,_,_) ->
367       T1 is OrigBase / 4096,
368       floor(T1,T2),
369       integer(T2,KeepBase),
370        Base $= KeepBase;
371        true
372    ),
373    keep_orig_addr(Buselements, Class, SubClass, ProgIf, Bus, Dev, Fun).
374
375% on some machines (sbrinz1) one of the two IOAPICs appears as a BAR
376% on a device which claims to be a RAM memory controller. If this occurs,
377% we want to avoid moving this BAR as otherwise the IOAPIC cannot be reached
378% anymore.
379keep_ioapic_bars(_, []).
380keep_ioapic_bars(Buselements, [H|IOAPICList]) :-
381    (
382    range(B, _) = H,
383    bar(addr(Bus,Dev,Fun),_,OrigBase,_,_,_,_),
384    T1 is OrigBase / 4096,
385    floor(T1,T2),
386    integer(T2,KeepBase),
387    KeepBase =:= B ->
388    keep_orig_addr(Buselements, _, _, _, Bus, Dev, Fun);
389    true
390    ),
391    keep_ioapic_bars(Buselements, IOAPICList).
392