[Libre-soc-dev] Task 939 and its subtasks

[Jacob Lifshay]

On Wed, Nov 23, 2022, 18:34 Luke Kenneth Casson Leighton via Libre-soc-dev <
libre-soc-dev at lists.libre-soc.org> wrote:

> Hendrik: the Formal Proof of the Power ISA was done by Boris
> Shingarov, last year.  at the very least he used the same
> MDWN files which are in Power ISA pseudocode, as used by the
> ISACaller compiler.
>
> the pseudocode is not even recognised by the original authors
> as a language, let alone a Turing-complete unambiguous one.
> we were the first and only team to say "that's not ok, there
> is too much to do here", everyone else hand-wrote simulators
> and decoders (including qemu, including binutils, quantity
> 10,000 instructions)
>
> Jacob, you keep doing this: you have a very ungrounded concept
> of time vs effort, because of lack of experience. Also,
> Asperger's prioritises "tidiness" and "exactness" over all
> other factors including "realistically affordable".  your
> suggestions are the "perfect scenario" where neither time
> nor cost matter in the least.
>

I keep pushing for getting better error checking and more maintainable code
because I consider my sanity valuable, I do not want to have to spend an
extra 5hr debugging every time I try to change something even remotely
complex in the pseudocode.

>
> Please respect when i say "no", and think "why has he said no,
> what factors did I miss". you are intelligent enough to
> work them out, and I simply do not have the time to explain
> them. it is therefore your responsibility to work through
> "why did he say no" so that i am not burdened with explaining.
>
> Dimitry, yes an expression is quite a high threshold, an
> even simpler one is just to return the incoming register.
> don't even add to it, not even a constant.
>
> there is only one type: a fixed-bit-length integer.
>

that's wrong, there is also Python int (e.g. XLEN and the output of all
MASK() calls) and maybe str too, icr for sure.

> also fixed-bit-length integer is not one type, it is many different types:
one for each different length.

absolutely nothing else.  lengths may be inferred especially
> when doing "result[0:XLEN-1] = something", you *know*
> result must be declared at precisely XLEN bits.
>
> accumulating these lengths allows the (one) type of object
> to be statically declared by adding to a list, that is
> last-minute added after all BNF tree-walking finishes, to
> the top of the AST.
>
> it is extremely straightforward.
>

that is two things:
1. insufficient as described to generate correct C, expressions have types
too, also you have to keep track of variables' and functions' types (which
may be generic) so you can look-up variables and functions later and know
exactly what types expressions using them have.

2. exactly (in spirit) the type deduction and checking you repeatedly
objected to me adding.

>
> the only tricky bit is EXTS() and undefined() both of which
>

EXTS simply returns a 256-bit integer (since that kludge seems to work) --
ideally it would just return a Python int (doesn't require infinite
storage, simple range analysis can deduce the maximum number of bits needed
for storage, making it a signed fixed-length integer that can't be
sliced/indexed)

>
undefined() is trivial -- the output type is the same as the input type.
Just look at the Python implementation.

Jacob