Erroneous bitcast for indefinite array allocation

[anydsl]

Erroneous bitcast for indefinite array allocation

[leissa]

So, here is the deal:

Thorin at its core is designed to be type-safe. This means you have to track all array sizes explicitly in the type. In order to support unsafe features such as C-like arrays, we need unsafe axioms such as :bitcast. On top of that, indices of arity ⊤∷nat such as 23∷(int ⊤∷nat) encode unsafe indices which makes «⊤∷nat; r32» an unsafe array.

If I understand your use case correctly, the real solution would be to simply not use an unsafe array but a safe array at the allocation. Later on, you can cast the safe array to an unsafe one like so:

N: nat = ...; // doesn't need to be a constant btw
_1: [:mem, :ptr («N; r32», 0∷nat)] = :alloc («N; r32», 0∷nat) mem1;
_2: :ptr («⊤∷nat; r32», 0∷nat) = :bitcast (:ptr («⊤∷nat; r32», 0∷nat), :ptr («N; r32», 0∷nat)) _1#1∷i1;

And here a little background regarding the :alloc vs :malloc:

Both things mean the same thing. The only difference is that the size computation in :alloc happens implicitly by looking at its type whereas :malloc performs this computation explicitly. This just makes our life in the backend a little bit easier, as we have the size computation now explicitly at the term level. I find this situation a bit unpleasant and would love to see a solution where we don't need two axioms which are basically doing the same thing. What is more, the size argument of :malloc isn't type-safe, which is even more weird. I'm happy to hear suggestions :)

Finally, the LLVM backend should probably throw an exception with a reasonable error message instead of just asserting or returning "<TODO>" but this is already covered in issue #9.

Does this solve your issue?

[leissa]

An unsafe Array only makes sense when having a pointer to it and :ptr («3∷nat; r32», 0∷nat) really is the same thing as float* in C. So there is no way for Thorin knowing the size. What is more, if you have an array like «n; r32», this is not a pair consisting of the actual array and a "size" field initialized to n. It is just an array of size n where n is some other term that occurs in the program. This leaves you with the following options.

1. Use safe arrays instead of unsafe ones. For example, the signature of a matmul would look like this:

   [T: *, n: nat, m: nat, o: nat] -> [a: :ptr «n, m; T», b: :ptr «m, o; T»] -> :ptr «n, o; T»
   

   (I'm taking some liberties with the syntax here, but I guess you see the point).
2. Instead of directly using Thorin arrays, use this type: [n: Nat, :ptr «n; r32»].
   This is a pair of size and and array of exactly that size.
3. Alternatively, you can you do sth like this: [i64, :ptr «⊤∷nat; r32»].
   This is basically this:

   struct MyArray {
       size_t size;
       float* array;
   };

Note that with approach 2) and 3) you duplicate size information when doing sth like the matmul. Finally, 3) is an unsafe C-style way of doing things and is only present in Thorin in order to communicate with unsafe code and should only be used when you really have to do this.

[NeuralCoder3]

In my use case, I get provided with an unsafe array (_2 in the example above) for instance as an argument in a function.
I then want to create an array of the same size.
Therefore, the allocation would need to know the size of the provided array at runtime.
Is this possible or do I have to rely on the user to also provide me with the second array?