Add support for indexing register array

[ffengyu]

Isla doesn't support pmpcfg and pmpaddr in the constraints because their type is
both ir::Val::Vector<_>, which falls into the default failure match arm of
function smt_value in file primop_until.rs.

There are two ways to fix it: extract the element from the vector before passing
it to smt_value, or provide the new matching pattern for vector in
smt_value. Considering Z3's array theory is for an infinite array, we must add
many constraints to imitate the extensional behavior of fixed-size array. In the
meantime, seq theory is not supported in Isla at all. We choose the first
option.

We extract the option in the get_loc_and_initialize because the arguments of
smt_value are got from the result of this function. We add additional Loc type
in smt_parser.lalrpop to combine the index and array together.

In the linearization.rc file, the ssa number is always -1 for the new Loc type because
the index is not variable and not assignable.

[bacam]

It would be nice to have a test too. I've just written one; I'll see if I can push it to your branch...

[bacam]

Shouldn't this just use a u32 like Loc?

[ffengyu]

Yes, it's essentially a wrapper of u32. I use SSAName for consistency in style.

[Alasdair]

It should just be u32. It should only be a SSAName if it was originally a Name in the non-SSA IR.

Name::from_u32(n) could maybe have a more descriptive name - it is not just creating a Name for the number, it's creating a name that indexes the nth element of the symbol table which is not what we want here.