Juneyoung Lee

Exception specification in declaration does not match previous declaration

9

When I compile folly (commit `689ef9`, Nov 17 2018) with Clang 6.0.0 on Ubuntu 16.04, I get this error: ``` $ make Scanning dependencies of target folly_base [ 0%] Building...

Sometimes simply encoding the mapping (i, j, k) -> blk offset using UF is more efficient than writing its full expression. Previously we had this option but is removed in...

It can be replaced with loadTensor + storeTensorTo + Tensor::conv.

Integer summation must be commutative as well

1

The precondition for this is not encoded.

- hoist-mul: https://stackoverflow.com/questions/60130513/take-out-common-variables-using-z3 - parallel: From 4.8.0 it is supported for QF_BV. ``` A parallel mode is available for select theories, including QF_BV. By setting parallel.enable=true Z3 will spawn a...

Transformations of interest

8

Here is the list of transformations that we'd like to verify primarily: - [x] linalg.conv->matmul - [x] linalg-fusion-for-tensor-ops(https://github.com/llvm/llvm-project/blob/d6467e00dfccf10aa91e5a1d55d981a9b13642a3/mlir/include/mlir/Dialect/Linalg/Passes.td#L59) - [ ] [tileLinalgOp code](https://github.com/llvm/llvm-project/blob/5540470f642a3118439996cbcde7d90530588eb5/mlir/include/mlir/Dialect/Linalg/Transforms/Transforms.h#L144) - [x] linalg.matmul to a loop of...

1. when the linalg.generic loop is full parallel & the affine.for contains memref ops 2. when the linalg.generic loop does reduction..? the memref store must put e.g. summation

tosa.add is commutative and nosideeffect

1

``` def Tosa_AddOp : Tosa_Op { ``` Q: if two tensors of different sizes are given to tosa.add, can we satisfy both?

- Is there a case where the output memref's stride is larger than one? - Are two memrefs of different memspaces no-alias? In the case of LLVM, there was `addrspacecast`,...