Fix lem build in Makefile #353

Alasdair · 2023-11-18T00:34:54Z

'class' is a reserved keyword in lem, so the use of class as a variable name was causing issues. While ultimately this should be fixed in Sail this can easily be worked around here.

Fortunately the code in questions was always using a pattern like

let class = f(x);
let y = match class {
  ...
};
y

which can be simplified to

match f(x) {
  ...
}

So I didn't have to invent a new variable name, and got to make the code simpler in the process!

Fixing this unfortunately causes some other issues to become apparent. The machine words library can't handle the large vlenmax, so we have to create a separate file with a smaller vlenmax for the theorem provers. There were also some other issues, so I switched out the default representation to bitlists until they can be resolved, and cleaned up some legacy cruft in handwritten_support while I was there.

The rmem target has similar issues, but as this is only really useful for rmem maintainers it doesn't make sense to run by default, so I removed it from the default set of targets.

This should fix #325

Alasdair · 2023-11-18T00:40:22Z

I split the commits so the actual model changes are in the first commit (which are all small refactorings).

The second commit contains all the lem hackery to fix the build

github-actions · 2023-11-18T00:59:23Z

Unit Test Results

712 tests ±0 712 ✔️ ±0 0s ⏱️ ±0s
    6 suites ±0     0 💤 ±0
    1 files ±0     0 ❌ ±0

Results for commit 17a6c93. ± Comparison against base commit 9f4cad6.

billmcspadden-riscv

My review is mainly questions. I don't see anything wrong in the code and will approve the PR once the questions are answered.

One exception: the 'effects' of certain functions need to be removed, yes?

Unable to comment on lem code due to lack of knowledge.

billmcspadden-riscv · 2023-11-29T18:06:26Z

Makefile

@@ -184,15 +185,7 @@ C_LIBS += $(SAIL_LIB_DIR)/coverage/libsail_coverage.a -lm -lpthread -ldl
 endif

 RISCV_EXTRAS_LEM_FILES = riscv_extras.lem mem_metadata.lem riscv_extras_fdext.lem
-# Feature detect if we are on the latest development version of Sail


Why was the check of the Sail version removed?

It's a check for a version of Sail that is many years old, and no longer works with the model.

billmcspadden-riscv · 2023-12-06T15:01:51Z

model/riscv_insts_vext_utils.sail

@@ -976,8 +976,7 @@ function rsqrt7 (v, sub) = {

 val riscv_f16Rsqrte7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) effect {rreg}


Remove effect throughout.

These lines are not part of this PR

You are seeing them just because this PR was opened before my other PR removing the effects separately was merged.

billmcspadden-riscv · 2023-12-06T15:02:37Z

model/riscv_insts_vext_utils.sail

@@ -1006,14 +1003,12 @@ function riscv_f32Rsqrte7 (rm, v) = {
    0x0080 => (zeros(5), 0x00000000),
    0x0020 => (zeros(5), rsqrt7(v, true)[31 .. 0]),
    _      => (zeros(5), rsqrt7(v, false)[31 .. 0])
-  };
-  (fflags, result)
+  }
 }

 val riscv_f64Rsqrte7 : (bits_rm, bits_D) -> (bits_fflags, bits_D) effect {rreg}


Remove effect

billmcspadden-riscv · 2023-12-06T15:02:51Z

model/riscv_insts_vext_utils.sail

@@ -988,14 +987,12 @@ function riscv_f16Rsqrte7 (rm, v) = {
    0x0080 => (zeros(5), 0x0000),
    0x0020 => (zeros(5), rsqrt7(v, true)[15 .. 0]),
    _      => (zeros(5), rsqrt7(v, false)[15 .. 0])
-  };
-  (fflags, result)
+  }
 }

 val riscv_f32Rsqrte7 : (bits_rm, bits_S) -> (bits_fflags, bits_S) effect {rreg}


Remove effect.

billmcspadden-riscv · 2023-12-06T15:05:36Z

model/riscv_vlen256.sail

Why is this part of this PR? Seems like an orthogonal addition.

There are two reasons the lem build fails. First, the use of class as an identifier, and second that the vlenmax is much too high. To make the lem build work we need a smaller vlenmax.

Ideally we would be able to disable V, but the extension is too intertwined into the base model right now to have a sail-riscv model without V, so having a shorter vlenmax is the best we can do.

jrtc27 · 2023-12-06T18:26:06Z

Merge branch 'master' into class_fix

Please rebase rather than merge to keep the history untangled

Alasdair · 2023-12-06T18:28:37Z

Merge branch 'master' into class_fix

Please rebase rather than merge to keep the history untangled

Sorry, I didn't realise the github update branch button did a merge by default. I'll fix it.

class is a reserved keyword in lem, so the use of class as a variable name was causing issues. While ultimately this should be fixed in Sail this can easily be worked around here. Fortunately the code in questions was ultimately using a pattern like let class = f(x); let y = match class { ... }; y which can be simplified to match f(x) { ... } removing the variable entirely, and making the code simpler so a win-win overall!

github-actions · 2023-12-06T18:55:10Z

Test Results

712 tests ±0 712 ✔️ ±0 0s ⏱️ ±0s
    6 suites ±0     0 💤 ±0
    1 files ±0     0 ❌ ±0

Results for commit 2f3dc1c. ± Comparison against base commit 393e7ed.

♻️ This comment has been updated with latest results.

bacam · 2023-12-07T13:07:11Z

For what it's worth, I've got development versions of Lem and Sail to handle the model with vectors and machine words, but I think the switch to bitlists by default is worthwhile because it's a little more robust. However, this does mean that the vlenmax change is unnecessary, so I suggest dropping that.

Switch to bitlist representation because the machine words can't handle the vector code currently Remove RMEM target from default set of targets in Makefile. This is only interesting for RMEM maintainers. There's no reason for it to be generated by default, and it's also broken. While we are hacking on these files purge the duplicate versions for Sail 0.11+

Alasdair · 2023-12-07T22:04:02Z

Ok, the additional vlen file is gone and it seems to build fine.

Alasdair · 2023-12-19T20:25:03Z

I think more people are running into this issue, would be good to get this merged I think

billmcspadden-riscv · 2023-12-19T20:49:04Z

Will do

…

On Tue, Dec 19, 2023, 12:25 PM Alasdair Armstrong ***@***.***> wrote: I think more people are running into this issue, would be good to get this merged I think — Reply to this email directly, view it on GitHub <#353 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AXROLOHXZTUH2L3QRLA4OBDYKHZ2VAVCNFSM6AAAAAA7QRUDXCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQNRTGQZDKNBYHA> . You are receiving this because you were assigned.Message ID: ***@***.***>

Alasdair mentioned this pull request Nov 18, 2023

Fail to run 'make' for sail-riscv #325

Closed

Alasdair mentioned this pull request Nov 18, 2023

Getting a makefile error when running make in the root directory #352

Closed

billmcspadden-riscv self-assigned this Nov 29, 2023

billmcspadden-riscv reviewed Dec 6, 2023

View reviewed changes

Alasdair force-pushed the class_fix branch from 508c4c9 to 0476651 Compare December 6, 2023 18:30

Alasdair force-pushed the class_fix branch from 0476651 to 2f3dc1c Compare December 7, 2023 22:02

Alasdair mentioned this pull request Dec 19, 2023

syntax error building rems-project/sail#408

Closed

billmcspadden-riscv merged commit d7a3d80 into riscv:master Dec 19, 2023
2 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix lem build in Makefile #353

Fix lem build in Makefile #353

Alasdair commented Nov 18, 2023

Alasdair commented Nov 18, 2023

github-actions bot commented Nov 18, 2023

billmcspadden-riscv left a comment

billmcspadden-riscv Nov 29, 2023

Alasdair Dec 6, 2023

billmcspadden-riscv Dec 6, 2023

Alasdair Dec 6, 2023

Alasdair Dec 6, 2023

billmcspadden-riscv Dec 6, 2023

billmcspadden-riscv Dec 6, 2023

billmcspadden-riscv Dec 6, 2023

Alasdair Dec 6, 2023 •

edited

Loading

Alasdair Dec 6, 2023

jrtc27 commented Dec 6, 2023

Alasdair commented Dec 6, 2023

github-actions bot commented Dec 6, 2023 •

edited

Loading

bacam commented Dec 7, 2023

Alasdair commented Dec 7, 2023

Alasdair commented Dec 19, 2023

billmcspadden-riscv commented Dec 19, 2023 via email

		@@ -976,8 +976,7 @@ function rsqrt7 (v, sub) = {

		val riscv_f16Rsqrte7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) effect {rreg}

Fix lem build in Makefile #353

Fix lem build in Makefile #353

Conversation

Alasdair commented Nov 18, 2023

Alasdair commented Nov 18, 2023

github-actions bot commented Nov 18, 2023

Unit Test Results

billmcspadden-riscv left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Alasdair Dec 6, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jrtc27 commented Dec 6, 2023

Alasdair commented Dec 6, 2023

github-actions bot commented Dec 6, 2023 • edited Loading

Test Results

bacam commented Dec 7, 2023

Alasdair commented Dec 7, 2023

Alasdair commented Dec 19, 2023

billmcspadden-riscv commented Dec 19, 2023 via email

Alasdair Dec 6, 2023 •

edited

Loading

github-actions bot commented Dec 6, 2023 •

edited

Loading