doc/cex.svg

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
 "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<!-- Generated by graphviz version 2.49.2 (0)
 -->
<!-- Title: G Pages: 1 -->
<svg width="1772pt" height="1161pt"
 viewBox="0.00 0.00 1772.00 1161.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 1157)">
<title>G</title>
<polygon fill="white" stroke="transparent" points="-4,4 -4,-1157 1768,-1157 1768,4 -4,4"/>
<!-- 0 -->
<g id="node1" class="node">
<title>0</title>
<polygon fill="#ffddcc" stroke="black" points="632.5,-1080 195.5,-1080 195.5,-982 632.5,-982 632.5,-1080"/>
<text text-anchor="start" x="203.5" y="-1064.8" font-family="Courier New" font-size="14.00" fill="#343434">[ Block: 0x0 ]</text>
<text text-anchor="start" x="203.5" y="-1049.8" font-family="Courier New" font-size="14.00" fill="#343434">0 cond.1 = ((bool2bv 64) (bvslt x.1 array1_size.1))</text>
<text text-anchor="start" x="203.5" y="-1034.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; A$ cond.1 = ((bool2bv 64) (bvslt 0x0:0 0x0:0))</text>
<text text-anchor="start" x="203.5" y="-1019.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; A@ cond.1 = 0x0:0</text>
<text text-anchor="start" x="203.5" y="-1004.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; B$ cond.1 = ((bool2bv 64) (bvslt 0x0:0 0x0:0))</text>
<text text-anchor="start" x="203.5" y="-989.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; B@ cond.1 = 0x0:0</text>
</g>
<!-- 7 -->
<g id="node6" class="node">
<title>7</title>
<polygon fill="#ffddcc" stroke="black" points="670,-440 158,-440 158,-282 670,-282 670,-440"/>
<text text-anchor="start" x="166" y="-424.8" font-family="Courier New" font-size="14.00" fill="#343434">[ Block: 0x7 ]</text>
<text text-anchor="start" x="166" y="-409.8" font-family="Courier New" font-size="14.00" fill="#343434">1 branch 0x4:64 if (= cond.1 0x0:64)</text>
<text text-anchor="start" x="166" y="-394.8" font-family="Courier New" font-size="14.00" fill="#343434">	# branch_target(0x1:64, 0x4:64) if (= cond.1 0x0:64)</text>
<text text-anchor="start" x="166" y="-379.8" font-family="Courier New" font-size="14.00" fill="#343434">	# branch_condition(0x1:64, (= cond.1 0x0:64))</text>
<text text-anchor="start" x="166" y="-364.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; A$ branch 0x4:64 if (= 0x0:0 0x0:64)</text>
<text text-anchor="start" x="166" y="-349.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; A# branch_target(0x1:1, 0x4:3)</text>
<text text-anchor="start" x="166" y="-334.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; A# branch_condition(0x1:1, true)</text>
<text text-anchor="start" x="166" y="-319.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; B$ branch 0x4:64 if (= 0x0:0 0x0:64)</text>
<text text-anchor="start" x="166" y="-304.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; B# branch_target(0x1:1, 0x4:3)</text>
<text text-anchor="start" x="166" y="-289.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; B# branch_condition(0x1:1, true)</text>
</g>
<!-- 0&#45;&gt;7 -->
<g id="edge1" class="edge">
<title>0&#45;&gt;7</title>
<path fill="none" stroke="#000000" stroke-opacity="0.333333" d="M408.13,-981.96C403.57,-944.58 398,-899 398,-899 398,-899 398,-899 398,-509 398,-509 400.98,-481.59 404.37,-450.45"/>
<polygon fill="#000000" fill-opacity="0.333333" stroke="#000000" stroke-opacity="0.333333" points="407.88,-450.55 405.48,-440.23 400.92,-449.8 407.88,-450.55"/>
<text text-anchor="middle" x="551" y="-693.8" font-family="Courier New" font-size="14.00" fill="#343434" fill-opacity="0.333333">(not (speculate _predictor.1 0x1:64))</text>
</g>
<!-- 8 -->
<g id="node7" class="node">
<title>8</title>
<polygon fill="#e1e1e1" stroke="black" points="1238.5,-916 1015.5,-916 1015.5,-880 1238.5,-880 1238.5,-916"/>
<text text-anchor="start" x="1023.5" y="-894.3" font-family="Courier New" font-size="14.00" fill="#343434">[ Block: 0x8, Transient ]</text>
</g>
<!-- 0&#45;&gt;8 -->
<g id="edge2" class="edge">
<title>0&#45;&gt;8</title>
<path fill="none" stroke="#ed403c" stroke-width="8.5" d="M632.77,-989.81C763.11,-965.86 922.47,-936.58 1024.35,-917.86"/>
<polygon fill="#ed403c" stroke="#ed403c" stroke-width="8.5" points="1025.84,-925.15 1034.33,-916.03 1023.16,-910.52 1025.84,-925.15"/>
<text text-anchor="start" x="935" y="-952.8" font-family="Courier New" font-size="14.00" fill="#343434">[speculate]</text>
<text text-anchor="middle" x="1063" y="-937.8" font-family="Courier New" font-size="14.00" fill="#343434">(speculate _predictor.1 0x1:64)</text>
</g>
<!-- 2 -->
<g id="node2" class="node">
<title>2</title>
<polygon fill="#ffddcc" fill-opacity="0.333333" stroke="black" points="528,-231 0,-231 0,-148 528,-148 528,-231"/>
<text text-anchor="start" x="8" y="-215.8" font-family="Courier New" font-size="14.00" fill="#343434" fill-opacity="0.333333">[ Block: 0x2 ]</text>
<text text-anchor="start" x="8" y="-200.8" font-family="Courier New" font-size="14.00" fill="#343434" fill-opacity="0.333333">2 v.2 = load(_memory.1, (bvadd array1.1 x.1))</text>
<text text-anchor="start" x="8" y="-185.8" font-family="Courier New" font-size="14.00" fill="#343434" fill-opacity="0.333333">	# cache_fetch((bvadd array1.1 x.1), 64)</text>
<text text-anchor="start" x="8" y="-170.8" font-family="Courier New" font-size="14.00" fill="#343434" fill-opacity="0.333333">3 tmp.2 = load(_memory.1, (bvadd array2.1 (bvshl v.2 0x8:64)))</text>
<text text-anchor="start" x="8" y="-155.8" font-family="Courier New" font-size="14.00" fill="#343434" fill-opacity="0.333333">	# cache_fetch((bvadd array2.1 (bvshl v.2 0x8:64)), 64)</text>
</g>
<!-- 4 -->
<g id="node3" class="node">
<title>4</title>
<polygon fill="#ffddcc" stroke="black" points="480,-111 348,-111 348,-73 480,-73 480,-111"/>
<text text-anchor="start" x="356" y="-95.8" font-family="Courier New" font-size="14.00" fill="#343434">[ Block: 0x4 ]</text>
<text text-anchor="start" x="356" y="-80.8" font-family="Courier New" font-size="14.00" fill="#343434">4 skip</text>
</g>
<!-- 2&#45;&gt;4 -->
<g id="edge3" class="edge">
<title>2&#45;&gt;4</title>
<path fill="none" stroke="#000000" stroke-opacity="0.333333" d="M327.61,-148C344.28,-137.39 361.71,-126.29 376.51,-116.87"/>
<polygon fill="#000000" fill-opacity="0.333333" stroke="#000000" stroke-opacity="0.333333" points="378.81,-119.56 385.36,-111.23 375.05,-113.65 378.81,-119.56"/>
</g>
<!-- 6 -->
<g id="node5" class="node">
<title>6</title>
<polygon fill="#ffddcc" stroke="black" points="480,-36 348,-36 348,0 480,0 480,-36"/>
<text text-anchor="start" x="356" y="-14.3" font-family="Courier New" font-size="14.00" fill="#343434">[ Block: 0x6 ]</text>
</g>
<!-- 4&#45;&gt;6 -->
<g id="edge4" class="edge">
<title>4&#45;&gt;6</title>
<path fill="none" stroke="#ed403c" stroke-width="8.5" d="M414,-72.83C414,-64.89 414,-55.41 414,-46.63"/>
<polygon fill="#ed403c" stroke="#ed403c" stroke-width="8.5" points="421.44,-46.42 414,-36.42 406.56,-46.42 421.44,-46.42"/>
</g>
<!-- 5 -->
<g id="node4" class="node">
<title>5</title>
<polygon fill="#ffddcc" stroke="black" points="480,-1153 348,-1153 348,-1117 480,-1117 480,-1153"/>
<text text-anchor="start" x="356" y="-1131.3" font-family="Courier New" font-size="14.00" fill="#343434">[ Block: 0x5 ]</text>
</g>
<!-- 5&#45;&gt;0 -->
<g id="edge5" class="edge">
<title>5&#45;&gt;0</title>
<path fill="none" stroke="#ed403c" stroke-width="8.5" d="M414,-1116.7C414,-1109.19 414,-1099.92 414,-1090.29"/>
<polygon fill="#ed403c" stroke="#ed403c" stroke-width="8.5" points="421.44,-1090.19 414,-1080.19 406.56,-1090.19 421.44,-1090.19"/>
</g>
<!-- 7&#45;&gt;2 -->
<g id="edge6" class="edge">
<title>7&#45;&gt;2</title>
<path fill="none" stroke="#000000" stroke-opacity="0.333333" d="M344.71,-281.7C331.75,-267.05 318.55,-252.15 306.7,-238.75"/>
<polygon fill="#000000" fill-opacity="0.333333" stroke="#000000" stroke-opacity="0.333333" points="309.13,-236.21 299.88,-231.04 303.89,-240.85 309.13,-236.21"/>
<text text-anchor="middle" x="421" y="-252.8" font-family="Courier New" font-size="14.00" fill="#343434" fill-opacity="0.333333">(not (= cond.1 0x0:64))</text>
</g>
<!-- 7&#45;&gt;4 -->
<g id="edge7" class="edge">
<title>7&#45;&gt;4</title>
<path fill="none" stroke="#ed403c" stroke-width="8.5" d="M500.56,-281.61C512.07,-271.18 520,-264 520,-264 520,-264 537,-231 537,-231 537,-231 537,-148 537,-148 537,-148 497.85,-130.5 463.73,-115.24"/>
<polygon fill="#ed403c" stroke="#ed403c" stroke-width="8.5" points="466.44,-108.3 454.27,-111.01 460.37,-121.88 466.44,-108.3"/>
<text text-anchor="start" x="537" y="-193.3" font-family="Courier New" font-size="14.00" fill="#343434">[taken]</text>
<text text-anchor="middle" x="607.5" y="-178.3" font-family="Courier New" font-size="14.00" fill="#343434">(= cond.1 0x0:64)</text>
</g>
<!-- 10 -->
<g id="node8" class="node">
<title>10</title>
<polygon fill="#e1e1e1" stroke="black" points="1531.5,-829 722.5,-829 722.5,-566 1531.5,-566 1531.5,-829"/>
<text text-anchor="start" x="730.5" y="-813.8" font-family="Courier New" font-size="14.00" fill="#343434">[ Block: 0xA, Transient ]</text>
<text text-anchor="start" x="730.5" y="-798.8" font-family="Courier New" font-size="14.00" fill="#343434">2 v.3 = load(_memory.1, (bvadd array1.1 x.1))</text>
<text text-anchor="start" x="730.5" y="-783.8" font-family="Courier New" font-size="14.00" fill="#343434">	# cache_fetch((bvadd array1.1 x.1), 64)</text>
<text text-anchor="start" x="730.5" y="-768.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; A$ v.3 = load(_memory.1, (bvadd 0x7C0000000000297B:63 0x0:0))</text>
<text text-anchor="start" x="730.5" y="-753.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; A@ v.3 = 0xF:4</text>
<text text-anchor="start" x="730.5" y="-738.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; A# cache_fetch(0x7C0000000000297B:63, 64)</text>
<text text-anchor="start" x="730.5" y="-723.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; B$ v.3 = load(_memory.1, (bvadd 0x7C0000000000297B:63 0x0:0))</text>
<text text-anchor="start" x="730.5" y="-708.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; B@ v.3 = 0xF03FFFFFFFFFFEF:60</text>
<text text-anchor="start" x="730.5" y="-693.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; B# cache_fetch(0x7C0000000000297B:63, 64)</text>
<text text-anchor="start" x="730.5" y="-678.8" font-family="Courier New" font-size="14.00" fill="#343434">3 tmp.3 = load(_memory.1, (bvadd array2.1 (bvshl v.3 0x8:64)))</text>
<text text-anchor="start" x="730.5" y="-663.8" font-family="Courier New" font-size="14.00" fill="#343434">	# cache_fetch((bvadd array2.1 (bvshl v.3 0x8:64)), 64)</text>
<text text-anchor="start" x="730.5" y="-648.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; A$ tmp.3 = load(_memory.1, (bvadd 0xF8000000000041FC:64 (bvshl 0xF:4 0x8:64)))</text>
<text text-anchor="start" x="730.5" y="-633.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; A@ tmp.3 = 0x0:0</text>
<text text-anchor="start" x="730.5" y="-618.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; A# cache_fetch(0xF8000000000050FC:64, 64)</text>
<text text-anchor="start" x="730.5" y="-603.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; B$ tmp.3 = load(_memory.1, (bvadd 0xF8000000000041FC:64 (bvshl 0xF03FFFFFFFFFFEF:60 0x8:64)))</text>
<text text-anchor="start" x="730.5" y="-588.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; B@ tmp.3 = 0xF0F0F0F0F0F0F0F:60</text>
<text text-anchor="start" x="730.5" y="-573.8" font-family="Courier New" font-size="14.00" fill="#343434"> &#45; B# cache_fetch(0xFC000000000030FC:64, 64)</text>
</g>
<!-- 8&#45;&gt;10 -->
<g id="edge8" class="edge">
<title>8&#45;&gt;10</title>
<path fill="none" stroke="#ed403c" stroke-width="8.5" d="M1127,-879.73C1127,-869.42 1127,-855.25 1127,-839.34"/>
<polygon fill="#ed403c" stroke="#ed403c" stroke-width="8.5" points="1134.44,-839.23 1127,-829.23 1119.56,-839.23 1134.44,-839.23"/>
<text text-anchor="middle" x="1263.5" y="-850.8" font-family="Courier New" font-size="14.00" fill="#343434">(not (taken _predictor.1 0x1:64))</text>
</g>
<!-- 11 -->
<g id="node9" class="node">
<title>11</title>
<polygon fill="#e1e1e1" stroke="black" points="1238.5,-529 1015.5,-529 1015.5,-491 1238.5,-491 1238.5,-529"/>
<text text-anchor="start" x="1023.5" y="-513.8" font-family="Courier New" font-size="14.00" fill="#343434">[ Block: 0xB, Transient ]</text>
<text text-anchor="start" x="1023.5" y="-498.8" font-family="Courier New" font-size="14.00" fill="#343434">4 skip</text>
</g>
<!-- 8&#45;&gt;11 -->
<g id="edge9" class="edge">
<title>8&#45;&gt;11</title>
<path fill="none" stroke="#000000" stroke-opacity="0.333333" d="M1238.87,-882.87C1315.75,-873.15 1404,-862 1404,-862 1404,-862 1541,-829 1541,-829 1541,-829 1541,-566 1541,-566 1541,-566 1371.06,-543.42 1248.94,-527.2"/>
<polygon fill="#000000" fill-opacity="0.333333" stroke="#000000" stroke-opacity="0.333333" points="1249.14,-523.7 1238.76,-525.85 1248.21,-530.63 1249.14,-523.7"/>
<text text-anchor="start" x="1541" y="-701.3" font-family="Courier New" font-size="14.00" fill="#343434" fill-opacity="0.333333">[taken]</text>
<text text-anchor="middle" x="1652.5" y="-686.3" font-family="Courier New" font-size="14.00" fill="#343434" fill-opacity="0.333333">(taken _predictor.1 0x1:64)</text>
</g>
<!-- 10&#45;&gt;11 -->
<g id="edge10" class="edge">
<title>10&#45;&gt;11</title>
<path fill="none" stroke="#ed403c" stroke-width="8.5" d="M1127,-565.9C1127,-556.25 1127,-547.25 1127,-539.46"/>
<polygon fill="#ed403c" stroke="#ed403c" stroke-width="8.5" points="1134.44,-539.28 1127,-529.28 1119.56,-539.28 1134.44,-539.28"/>
</g>
<!-- 11&#45;&gt;7 -->
<g id="edge11" class="edge">
<title>11&#45;&gt;7</title>
<path fill="none" stroke="#ed403c" stroke-width="8.5" d="M1039.57,-490.97C950.24,-472.56 807.01,-443.03 680.13,-416.87"/>
<polygon fill="#ed403c" stroke="#ed403c" stroke-width="8.5" points="681.54,-409.57 670.24,-414.83 678.54,-424.13 681.54,-409.57"/>
<text text-anchor="middle" x="976.5" y="-461.8" font-family="Courier New" font-size="14.00" fill="#343434">[rollback]</text>
</g>
</g>
</svg>