Convert sail to lem

[applepingge]

Hi! I want to convert the sail file to a lem file. For example, I executed the command sail -lem -o test -lem_mwords -lem_lib test_extras prelude.sail no_devices.sail aarch_types.sail aarch_mem.sail aarch64.sail aarch64_float.sail aarch64_vector.sail aarch32.sail aarch_decode.sail in the sail-arm/model folder. but a type error occurs, i.e., Type error:

2444	_GTE_PPU_Address[region] = _GTEParam[1];	^----------------------^	Vector assignment not provably in bounds _GTE_PPU_Address[region]	This error occured because of a previous error:	aarch_mem.sail:2444:4-28	2444	_GTE_PPU_Address[region] = _GTEParam[1];		^----------------------^		Vector assignment not provably in bounds _GTE_PPU_Address[region]

I don't know if the conversion method is wrong, or how should I convert the sail to lem? look forward to your reply, thank you.

[rmn30]

It looks like sail can't tell statically that region is definitely within the bounds of _GTE_PPU_Address. What are their types?

[bauereiss]

The problem can be worked around by disabling bounds checks in vector assignments using the -no_lexp_bounds_check option. Try using the aarch64.lem target of the Makefile in the arm-v8.5-a folder of the sail-arm repository; it uses this and some other options for Lem generation.

[applepingge]

It looks like sail can't tell statically that region is definitely within the bounds of _GTE_PPU_Address. What are their types?

Oh, maybe register _GTE_PPU_Address : vector(6, dec, bits(64)). I am sorry that I don't know much about the sail language. In fact, I just want to convert the sail implementation of ARMv8 to the isabelle language, so I first tried to convert to lem files according to the documentation(Using Sail Specifications in Isabelle/HOL) but I got this error.

[applepingge]

The problem can be worked around by disabling bounds checks in vector assignments using the -no_lexp_bounds_check option. Try using the aarch64.lem target of the Makefile in the arm-v8.5-a folder of the sail-arm repository; it uses this and some other options for Lem generation.

Oh, there are two files, aarch64_extras.lem in the arm-v8.5-a folder and aarch64.lem in the arm-v8.5-a/snapshots/lem folder. I would like to ask if this aarch64.lem file is generated by the all sail file in the arm-v8.5-a/model folder? I want to convert them to isabelle files as the ARM implementation in the isabelle prover. So could I convert this aarch64.lem directly to isabelle?

[applepingge]

Thank you very much for your reply. Thank you.

[PeterSewell]

Probably it'd be worth us adding checked-in snapshots of the generated Isa and HOL4?

On Fri, 31 May 2019 at 13:00, Thomas Bauereiss notifications@github.com wrote:

The problem can be worked around by disabling bounds checks in vector assignments using the -no_lexp_bounds_check option. Try using the aarch64.lem target of the Makefile in the arm-v8.5-a folder of the sail-arm repository; it uses this and some other options for Lem generation.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/rems-project/sail/issues/51?email_source=notifications&email_token=ABFMZZT57UAVUK6GZJC6OLDPYEHOLA5CNFSM4HRTZWLKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODWVA2PY#issuecomment-497683775, or mute the thread https://github.com/notifications/unsubscribe-auth/ABFMZZQNYMQNXYMMP5TYALLPYEHOLANCNFSM4HRTZWLA .

[bauereiss]

Sorry for the delay, but snapshots are now checked here (currently in a branch, but will be merged into master soon after the opam package of Sail has been upgraded to include some recent changes).

[applepingge]

Sorry for the delay, but snapshots are now checked here (currently in a branch, but will be merged into master soon after the opam package of Sail has been upgraded to include some recent changes).

Nothing, thank you and sorry to delay your work. I have seen the new snapshots. For previous work, I did solve the problem above according to your tips, and generated the lem file. But now both the new snapshots and old master only cover the base 64-bit ISA, so I tried to convert the 32-bit sail file like aarch32.sail to lem but some errors always occur. I am not sure if there is a problem with the command. An another question is the convention from lem to isa. I executed the command: lem -isa -outdir . -lib Sail=...... in the old sail-arm(master) and got the type error Type error: unbound variable for targets {isabelle}: integerOfString (line 1385), I guess if I need an extra command like -no_lexp_bounds_check as well. And in the new added branch yesterday(snapshots), I executed the lem ....... and got the syntax error Syntax error: couldn't parse integer 13883517620612518109 (line 23529). I would like to know how you convert lem to the four isa files (I know you want to get rid of me, hha), thank you.

[bauereiss]

Try upgrading Lem; integerOfString should be implemented in the current opam release. For the Lem files in the snapshots branch, you currently need the zarith branch of Lem for big integer and word literals.

The reason that the snapshots currently only cover a fragment of the spec is that the bitvector length monomorphisation requires some more patches in the other parts of the spec. The Makefile target for the Lem files in sail-arm does not enable monomorphisation and should successfully generate Lem files for the whole spec using a list representation of bitvectors instead of machine words, but I can confirm that there seems to be a bug in the rewriter to Lem that causes a type error in aarch32.sail. I'll look into it.

[Alasdair]

The issue is with the 32-bit vector instructions. Our ASL to Sail generates something like the following, where the constraint says that 'esize = 64 implies the correct bounds on 'd and 'm. This is generated automatically based on the structure of the code which is why it's a bit long and ugly

val VRINTZ_vfp_Op_A : forall 'd 'esize ('exact : Bool) 'm,
  ('m >= 0 & 'm <= 31 | not('esize == 16)) & ('d >= 0 & 'd <= 31 | not('esize == 16)) & ('m >= 0 & 'm <= 31 | not('esize == 32)) & ('d >= 0 & 'd <= 31 | not('esize == 32)) & ('m >= 0 & 'm <= 31 | not('esize == 64)) & ('d >= 0 & 'd <= 31 | not('esize == 64)).
  (int('d), int('esize), bool('exact), int('m), FPRounding) -> unit effect {escape, rreg, undef, wreg}

function VRINTZ_vfp_Op_A (d, esize, exact, m, rounding) = {
    if ConditionPassed() then {
        CheckVFPEnabled(true);
        match esize {
          16 => {
              S(d) = Zeros(16) @ FPRoundInt(slice(S(m), 0, 16), FPSCR, rounding, exact)
          },
          32 => {
              S(d) = FPRoundInt(S(m), FPSCR, rounding, exact)
          },
          64 => {
              D(d) = FPRoundInt(D(m), FPSCR, rounding, exact)
          }
        }
    }
}

The issue is the lem translation converts the integer match into an if-then-else statement but the final else loses the 'esize = 64 constraint that is required for it to typecheck.

This can be worked-around in Sail by adding a stronger sensible hand-written constraint like

('m >= 0 & 'm <= 31) & ('d >= 0 & 'd <= 31) & 'esize in {16, 32, 64}

which imples 'esize = 64 after the if 'esize = 16 and if 'esize = 32 cases.

I think there are maybe some other small issues where variables in the ASL end up having the same name as Lem builtins. For our work so far we've only used the 64-bit instruction set which is why I guess this hasn't been fixed yet.

[bauereiss]

I changed the rewriting step for guarded patterns so that it adds a fallthrough case for potentially incomplete pattern matches (and keeps the guards on other cases), which should solve the 'esize problem above. I also committed a change to Lem so that it declares function parameters more explicitly when generating Isabelle definitions, which should solve the name clash issue.

When you now run make aarch64.lem using the master branches of sail-arm and lem and the sail2 branch of Sail, this should give you Lem definitions for all instructions of ARMv8.5-A, including floating point, vector, and 32 bit (albeit with the list representation of bitvectors, as mentioned above).

[applepingge]

The issue is with the 32-bit vector instructions. Our ASL to Sail generates something like the following, where the constraint says that 'esize = 64 implies the correct bounds on 'd and 'm. This is generated automatically based on the structure of the code which is why it's a bit long and ugly

val VRINTZ_vfp_Op_A : forall 'd 'esize ('exact : Bool) 'm,
  ('m >= 0 & 'm <= 31 | not('esize == 16)) & ('d >= 0 & 'd <= 31 | not('esize == 16)) & ('m >= 0 & 'm <= 31 | not('esize == 32)) & ('d >= 0 & 'd <= 31 | not('esize == 32)) & ('m >= 0 & 'm <= 31 | not('esize == 64)) & ('d >= 0 & 'd <= 31 | not('esize == 64)).
  (int('d), int('esize), bool('exact), int('m), FPRounding) -> unit effect {escape, rreg, undef, wreg}

function VRINTZ_vfp_Op_A (d, esize, exact, m, rounding) = {
    if ConditionPassed() then {
        CheckVFPEnabled(true);
        match esize {
          16 => {
              S(d) = Zeros(16) @ FPRoundInt(slice(S(m), 0, 16), FPSCR, rounding, exact)
          },
          32 => {
              S(d) = FPRoundInt(S(m), FPSCR, rounding, exact)
          },
          64 => {
              D(d) = FPRoundInt(D(m), FPSCR, rounding, exact)
          }
        }
    }
}

The issue is the lem translation converts the integer match into an if-then-else statement but the final else loses the 'esize = 64 constraint that is required for it to typecheck.

This can be worked-around in Sail by adding a stronger sensible hand-written constraint like

('m >= 0 & 'm <= 31) & ('d >= 0 & 'd <= 31) & 'esize in {16, 32, 64}

which imples 'esize = 64 after the if 'esize = 16 and if 'esize = 32 cases.

I think there are maybe some other small issues where variables in the ASL end up having the same name as Lem builtins. For our work so far we've only used the 64-bit instruction set which is why I guess this hasn't been fixed yet.

OK, thank you, I have learned some more knowledge from this.

[applepingge]

I changed the rewriting step for guarded patterns so that it adds a fallthrough case for potentially incomplete pattern matches (and keeps the guards on other cases), which should solve the 'esize problem above. I also committed a change to Lem so that it declares function parameters more explicitly when generating Isabelle definitions, which should solve the name clash issue.

When you now run make aarch64.lem using the master branches of sail-arm and lem and the sail2 branch of Sail, this should give you Lem definitions for all instructions of ARMv8.5-A, including floating point, vector, and 32 bit (albeit with the list representation of bitvectors, as mentioned above).

OK, I am trying to generate the new definitions. I found that the installation instructions for the sail are also updated, and I am planning to reinstall the entire project on a new machine because many places have changed. For the past two days I have been solving the above problem(integerOfString).

[applepingge]

@bauereiss Hi, I am sorry to disturb you again. Is there a ready-made heap image in the directory sail-arm-snapshots/arm-v8.5-a/snapshots/isabelle? Because I spent a long time executing the command isabelle build -b -d lib -d . Sail-AArch64 and it was not built.

[bauereiss]

The build takes roughly 20 minutes on my (quite powerful) machine. What kind of machine are you using, which version of the sail-arm repository, and which version of Isabelle? (Those snapshots currently target Isabelle 2018; for 2019, a few tweaks are required.)

[applepingge]

The build takes roughly 20 minutes on my (quite powerful) machine. What kind of machine are you using, which version of the sail-arm repository, and which version of Isabelle? (Those snapshots currently target Isabelle 2018; for 2019, a few tweaks are required.)

We run the virtual machine on a 32GB memory machine and allocate 20GB of memory to it, the machine may be not powerful enough. The sail-arm is the latest repository you updated (17 days ago), and we use Isabelle 2018.

[PeterSewell]

Perhaps you could also say who you/your group are, and in what way(s) you'd like to use the model?

best, Peter

On 27/06/2019, applepingge notifications@github.com wrote:

The build takes roughly 20 minutes on my (quite powerful) machine. What kind of machine are you using, which version of the sail-arm repository, and which version of Isabelle? (Those snapshots currently target Isabelle 2018; for 2019, a few tweaks are required.)

We run the virtual machine on a 32GB memory machine and allocate 20GB of memory to it, the machine may be not powerful enough. The sail-arm is the latest repository you updated (17 days ago), and we use Isabelle 2018.

-- You are receiving this because you commented. Reply to this email directly or view it on GitHub: https://github.com/rems-project/sail/issues/51#issuecomment-506232593

[applepingge]

Perhaps you could also say who you/your group are, and in what way(s) you'd like to use the model? best, Peter … On 27/06/2019, applepingge @.***> wrote: > The build takes roughly 20 minutes on my (quite powerful) machine. What > kind of machine are you using, which version of the sail-arm repository, > and which version of Isabelle? (Those snapshots currently target Isabelle > 2018; for 2019, a few tweaks are required.) We run the virtual machine on a 32GB memory machine and allocate 20GB of memory to it, the machine may be not powerful enough. The sail-arm is the latest repository you updated (17 days ago), and we use Isabelle 2018. -- You are receiving this because you commented. Reply to this email directly or view it on GitHub: #51 (comment)

Thank you, I am now a master student from Capital Normal University, China, and the research direction is formal verification. We expect to learn some knowledge from your model and even get more details about ARMv8. In the future, we might expand some theories in this model.

[bauereiss]

A more powerful machine might help. You could also try opening an interactive session using isabelle jedit -d lib -d . Aarch64_lemmas.thy, which might allow you to observe where exactly it gets stuck. Note that the definition of the regstate type is expected to take some minutes to process due to its size.

[applepingge]

A more powerful machine might help. You could also try opening an interactive session using isabelle jedit -d lib -d . Aarch64_lemmas.thy, which might allow you to observe where exactly it gets stuck. Note that the definition of the regstate type is expected to take some minutes to process due to its size.

Yes, I guess so. I opened the two files Aarch64_type.thy and Aarch64.thy, and the regstate variable spent about 5 min on loading. But now they are successful, and I started some other extensions like events or lemmas. We might change a machine later.