static */
| 1125 | } |
| 1126 | |
| 1127 | /* static */ bool ShapeUtil::ReshapeIsBitcast(const Shape& input_shape, |
| 1128 | const Shape& output_shape) { |
| 1129 | CHECK(input_shape.IsArray()); |
| 1130 | CHECK(output_shape.IsArray()); |
| 1131 | CHECK(LayoutUtil::HasLayout(input_shape)); |
| 1132 | CHECK(LayoutUtil::HasLayout(output_shape)); |
| 1133 | |
| 1134 | if (!SameElementType(input_shape, output_shape)) { |
| 1135 | return false; |
| 1136 | } |
| 1137 | |
| 1138 | CHECK_EQ(ElementsIn(input_shape), ElementsIn(output_shape)); |
| 1139 | if (ElementsIn(input_shape) == 0) { |
| 1140 | return true; |
| 1141 | } |
| 1142 | |
| 1143 | // TL;DR: The rest of the method checks that the reshape does not change the |
| 1144 | // physical location of any unit input or output index. Unit indices have |
| 1145 | // exactly one dimension that equals 1 and other dimensions 0. This condition |
| 1146 | // is necessary for the reshape to be a bitcast, because a bitcast-equivalent |
| 1147 | // reshape shouldn't change the physical location of any element. It is also a |
| 1148 | // sufficient condition as is proved below (note: many details are omitted for |
| 1149 | // space). |
| 1150 | // |
| 1151 | // Definitions: |
| 1152 | // |
| 1153 | // * Denote the input shape by IS and output shape by OS. IS[i] or OS[i] means |
| 1154 | // the size of i-th least significant dimension of IS or OS (this is opposite |
| 1155 | // to how we define the index of Shape::dimensions()). |
| 1156 | // |
| 1157 | // * Given an input or output index I, denote by p(I) I's physical linear |
| 1158 | // index (or physical index for short) and l(I) I's logical linear index (or |
| 1159 | // logical index for short). |
| 1160 | // |
| 1161 | // * Given a logical index k, denote by II(k) the input index whose linear |
| 1162 | // index is k, and OI(k) the corresponding output index. |
| 1163 | // |
| 1164 | // * Denote by IT[i] the increment of physical index if i-th dimension of the |
| 1165 | // input index is increased by 1. Similarly, OT[i] means the increment if i-th |
| 1166 | // dimension of the output index is increased by 1. Note that IT[i] or OT[i] |
| 1167 | // is a function of IS or OS and the layout, and not dependent on the specific |
| 1168 | // input or output index. |
| 1169 | // |
| 1170 | // To prove the reshape from IS to OS is a bitcast, it is sufficient to prove |
| 1171 | // that, for any linear index k, p(II(k))=p(OI(k)). We prove this by |
| 1172 | // induction. We know p(II(0))=p(OI(0)) is trivially true, so what's left is |
| 1173 | // to prove, with every increment on k, the above formula still holds. |
| 1174 | // |
| 1175 | // First, suppose reshaping from IS to OS is non-factorizable (we discuss |
| 1176 | // refactorizable reshapes later). A reshape from IS to OS is factorizable, if |
| 1177 | // there exists (i,j) such that |
| 1178 | // |
| 1179 | // 0<=i<=|IS| |
| 1180 | // 0<=j<=|OS| |
| 1181 | // |IS|-i+|OS|-j > 0 (i.e., i,j mustn't both point to the end) |
| 1182 | // product(IS[i], IS[i+1], ..., IS[|IS|-1]) |
| 1183 | // = product(OS[j], OS[j+1], ..., OS[|OS|-1]) |
| 1184 | // |
nothing calls this directly
no test coverage detected