Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Error while running make ( Type error: type mismatch: application expression ) #313

Open
shahzaibk23 opened this issue Oct 8, 2023 · 12 comments
Open

Error while running make ( Type error: type mismatch: application expression ) #313

shahzaibk23 opened this issue Oct 8, 2023 · 12 comments

Comments

@shahzaibk23
Copy link

When I run make in repo top, it breaks after running for a while.

OPAM version: 2.0.5
OCAML version: 4.08.0

Warning: Deprecated model/prelude.sail:80.22-43:
80 |val string_startswith = "string_startswith" : (string, string) -> bool
   |                      ^-------------------^
   | 
All external bindings should be marked as either monadic or pure

Warning: Duplicate function type definition for spc_forwards
model/prelude.sail:303.4-16:
303 |val spc_forwards : unit -> string
    |    ^----------^
    | This duplicate definition is being ignored!
Warning: Incomplete pattern match statement at model/riscv_types_kext.sail:240.2-7:
240 |  match (x, table) {
    |  ^---^
    | 
The following expression is unmatched: (undefined, [||])

echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/RV64/riscv_types.lem
lem -isa -outdir generated_definitions/isabelle/RV64 -lib Sail=/home/merledu1/.opam/4.08.0/share/sail/src/lem_interp -lib Sail=/home/merledu1/.opam/4.08.0/share/sail/src/gen_lib \
        handwritten_support/0.11/riscv_extras.lem handwritten_support/0.11/mem_metadata.lem handwritten_support/0.11/riscv_extras_fdext.lem \
        generated_definitions/lem/RV64/riscv_types.lem \
        generated_definitions/lem/RV64/riscv.lem
File "generated_definitions/lem/RV64/riscv.lem", line 50091, character 9 to line 50091, character 53
  Type error: type mismatch: application expression
    bool
  and
    Sail2_prompt_monad.monad _ bool _
make: *** [Makefile:318: generated_definitions/isabelle/RV64/Riscv.thy] Error 1
@kuopinghsu
Copy link

Same problem here. Is any specific OAPM version required.

OPAM 2.1.2
OCAML 5.1.0

@billmcspadden-riscv
Copy link
Collaborator

billmcspadden-riscv commented Oct 11, 2023 via email

@ved-rivos
Copy link
Contributor

I am facing the following error. Please help.
OPAM version: 2.0.5
OCAML version: 4.08.0

echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/RV64/riscv_types.lem
lem -isa -outdir generated_definitions/isabelle/RV64 -lib Sail=/home/vedvyas/.opam/4.08.0/share/sail/src/lem_interp -lib Sail=/home/vedvyas/.opam/4.08.0/share/sail/src/gen_lib \
	handwritten_support/0.11/riscv_extras.lem handwritten_support/0.11/mem_metadata.lem handwritten_support/0.11/riscv_extras_fdext.lem \
	generated_definitions/lem/RV64/riscv_types.lem \
	generated_definitions/lem/RV64/riscv.lem
File "generated_definitions/lem/RV64/riscv.lem", line 282, character 24 to line 282, character 34
  Type error: unbound variable for targets {isabelle}: sign_extend

@Alasdair
Copy link
Collaborator

opam update / opam upgrade maybe?

@ved-rivos
Copy link
Contributor

I did both opam update and opam upgrade. My opam version is 2.0.5 and ocaml version is 4.08.0.
I encounter a completely new issue now:

Warning: Deprecated model/prelude.sail:80.22-43:
80 |val string_startswith = "string_startswith" : (string, string) -> bool
   |                      ^-------------------^
   | 
All external bindings should be marked as either monadic or pure

Warning: Duplicate function type definition for spc_forwards
model/prelude.sail:303.4-16:
303 |val spc_forwards : unit -> string
    |    ^----------^
    | This duplicate definition is being ignored!
Warning: Incomplete pattern match statement at model/riscv_types_kext.sail:240.2-7:
240 |  match (x, table) {
    |  ^---^
    | 
The following expression is unmatched: (undefined, [||])

Type error:
No type declaration found for _s5408#
make: *** [Makefile:213: generated_definitions/ocaml/RV64/riscv.ml] Error 1

@Alasdair
Copy link
Collaborator

If you do make check or make csim does it work? What is you Sail version (sail -v) and Z3 version (z3 -version), and are you at the latest commit (c04cf29) in this repository?

Technically OCaml 4.08.1 is the lowest version we test with, but this doesn't seem like it would be caused by that.

@ved-rivos
Copy link
Contributor

ved-rivos commented Oct 17, 2023 •
edited
Loading

Sail version - Sail 0.16 (sail @ opam-v2.0.5)
Z3 version 4.8.7 - 64 bit
Both make check and make csim fail.

@Alasdair
Copy link
Collaborator

You might need to run make clean before those two commands. If both of those commands fail in the same way after make clean I don't really understand what could be happening, because the error refers to a makefile target they wouldn't touch.

@ved-rivos
Copy link
Contributor

I have hit make clean before each invocation.
make csim fails as follows:

Type error:
No type declaration found for _s5408#
make: *** [Makefile:247: generated_definitions/c/riscv_model_RV64.c] Error 1

make check just stops without any error

  |    ^----------^
   | This duplicate definition is being ignored!
Warning: Incomplete pattern match statement at model/riscv_types_kext.sail:240.2-7:
240 |  match (x, table) {
   |  ^---^
   | 
The following expression is unmatched: (undefined, [||])

@Alasdair
Copy link
Collaborator

I think that means make check is working, it'll print some warnings but that's ok.

I've tried to set up my environment as close to yours as possible, and so far I can't reproduce the error.

@Alasdair
Copy link
Collaborator

The error message suggests it has something to do with string append patterns, like in assembly clauses. As I think the _s5408# would be a generated name for a function that parses a string append pattern.

@shahzaibk23
Copy link
Author

OPAM version: 2.0.5
OCAML version: 4.08.0

I am also facing a new error, after pulling the latest changes from repo.....

Warning: Duplicate function type definition for spc_forwards
model/prelude.sail:303.4-16:
303 |val spc_forwards : unit -> string
    |    ^----------^
    | This duplicate definition is being ignored!
Warning: Incomplete pattern match statement at model/riscv_types_kext.sail:240.2-7:
240 |  match (x, table) {
    |  ^---^
    | 
The following expression is unmatched: (undefined, [||])

echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/RV64/riscv_types.lem
lem -isa -outdir generated_definitions/isabelle/RV64 -lib Sail=/home/merledu1/.opam/4.08.0/share/sail/src/lem_interp -lib Sail=/home/merledu1/.opam/4.08.0/share/sail/src/gen_lib \
        handwritten_support/0.11/riscv_extras.lem handwritten_support/0.11/mem_metadata.lem handwritten_support/0.11/riscv_extras_fdext.lem \
        generated_definitions/lem/RV64/riscv_types.lem \
        generated_definitions/lem/RV64/riscv.lem
File "generated_definitions/lem/RV64/riscv.lem", line 6583, character 12 to line 6583, character 35
  Type error: unbound variable: sys_enable_writable_fiom
make: *** [Makefile:318: generated_definitions/isabelle/RV64/Riscv.thy] Error 1
merledu1@merledu1:~/sail-riscv$ opam --version
2.0.5
merledu1@merledu1:~/sail-riscv$ ocaml --version
The OCaml toplevel, version 4.08.0

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
5 participants
@Alasdair @kuopinghsu @shahzaibk23 @ved-rivos @billmcspadden-riscv