isla-sail does not preserve initial values of sail registers

[cfbolz]

Hi Alasdair!

As we discussed in this issue I'm switching to use isla-sail to get an ASCII representation of JIB for use in Pydrofoil. This seems to work fine for the RISC-V model, so that's very cool! However, I encountered a problem when trying to use Pydrofoil to also generate an ARM 9.3 emulator with pydrofoil (I haven't done this so far). What happens is that an assert triggers while TakeReset is executed, and I think isla-sail is to blame:

It seems to me that isla-sail ignores the initial values of registers. concretely, this ARM register lead to a problem:

register CFG_RMR_AA64 : bits(1) = 0b1

the .ir file that isla-sail generates does not reflect the = 0b1 part anywhere, also not in initialize_registers, and there is no equivalent of model_init, like in the C backend.

To reproduce this in a smaller example, I tried this sail model x.sail:

default Order dec

$include <prelude.sail>

register PC : bits(16) = 0xcafe
register A : bits(16)

val main : unit -> unit

function main() -> unit = {
    PC = 0x0000;
    A = 0x0000;
}

running isla-sail x.sail gives this output:

val zz5i64zDzKz5i = "%i64->%i" : (%i64) ->  %i

union zexception {
  z__dummy_exnz3: %unit
}

val zundefined_bitvector = "undefined_bitvector" : (%i) ->  %bv

val zappend_64 = "append_64" : (%bv, %bv64) ->  %bv

register zPC : %bv16

register zA : %bv16

val zmain : (%unit) ->  %unit

fn zmain(zgsz30) {
  zPC = 0x0000 `0 11:9-11:15;
  zz40 : %unit `0 11:4-11:15;
  zz40 = () `0 11:4-11:15;
  zA = 0x0000 `0 12:8-12:14;
  return = () `0 12:4-12:14;
  end;
}

val zinitializze_registers : (%unit) ->  %unit

fn zinitializze_registers(zgsz32) {
  zz40 : %i `1;
  zz40 = zz5i64zDzKz5i(16) `2;
  zz41 : %bv `3;
  zz41 = zundefined_bitvector(zz40) `4;
  zA = zz41 `5;
  return = () `6;
  end;
}

files "x.sail"

the 0xCAFE initial value is nowhere in there. Am I missing something?

[Alasdair]

I think I'm just not printing it because I've been using the configuration files in https://github.com/rems-project/isla/tree/master/configs to control the initial state in Isla, but it should be an easy fix to just add this.

[cfbolz]

right, sure looks like it for my problem with arm: https://github.com/rems-project/isla/blob/master/configs/aarch64.toml#L85

(sorry, I have absolutely no idea how the rest of isla operates, I'm really just using isla-sail :sweat_smile:)

[martinberger]

but it should be an easy fix to just add this.

This is a critical blocker for Pydrofoil's development.

Do you have a time-frame when this will be fixed? In principle we can fix this ourselves and make a PR, it's probably very easy, just a few lines, but we would have to learn about isla-sail's structure, hidden invariants etc.

[bacam]

I'll try to look at it in the next day or two, because it's also a source of churn in the configuration files between model versions as features are added or configuration registers renamed.

[Alasdair]

Should be fixed by https://github.com/rems-project/isla/commit/641fef79adc4ec8801d28187100849025107b71c

[Alasdair]

Will now output something like:

register zPC : %bv16 {
  zPC = 0xCAFE `0 5:25-5:31;
}

[cfbolz]

Wonderful, thanks a lot! I'll check it out very soon.

[cfbolz]

unfortunately I now can't generate IR for arm-v9.3-a on the arm repo master branch:

arm/arm-v9.3-a/ $ make gen_ir
[WARNING] var was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
mkdir -p ir
isla-sail -v 1 -memo_z3 -mono_rewrites src/prelude.sail src/decode_start.sail src/builtins.sail src/v8_base.sail src/config.sail src/sysops.sail src/instrs64.sail src/instrs32.sail src/devices.sail src/fetch.sail src/impdefs.sail src/interrupts.sail src/mem.sail src/step.sail src/map_clauses.sail src/event_clauses.sail src/stubs.sail src/elfmain.sail src/isla_main.sail -o ir/armv9
Type error:[===================                               ] 38% (9450/24552)          
src/v8_base.sail:147311.24-33:
147311 |    result : bits('N) = undefined;
       |                        ^-------^
       | Type bits('N) is empty
make: *** [Makefile:70: gen_ir] Error 1

any ideas? I'm using sail from git head (27a183e033f858d957758fef8ce34f71319d79c6) and your isla commit from yesterday.

[cfbolz]

right, I see. the problem is this function from v8_base.sail:

val BitReverse : forall 'N. bits('N) -> bits('N)

function BitReverse data = {
    result : bits('N) = undefined;
    foreach (i from 0 to ('N - 1) by 1 in inc) {
        result['N - i - 1] = Bit([data[i]])
    };
    return(result)
}

this Sail commit, which adds a check for undefined : T that T is inhabited breaks BitReverse, because 'N is not required to be > 0 here.

What should I do here, @Alasdair? Am I doing something stupid?

[Alasdair]

You could try the interface-v9 branch of the sail-arm repository, which has a fix for this issue I think. We should apply that same fix to master as well.

[cfbolz]

Thank you very much, this particular problem is solved! I am definitely getting much further than before.