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.

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

Unexpected and unused material in printed output #1175

Closed
msaaltink opened this issue Apr 6, 2021 · 2 comments · Fixed by #1276
Closed

Unexpected and unused material in printed output #1175

msaaltink opened this issue Apr 6, 2021 · 2 comments · Fixed by #1276
Assignees
Labels
subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem

Comments

@msaaltink
Copy link
Contributor

In a recent SAW (a923cfe)

sawscript> {{ [0x1,0x2] @ 0b01 }}
[14:18:58.877] let { x@1 = Prelude.Nat
      -> sort 0
      -> sort 0
      x@2 = Cryptol.TCNum 1
      x@3 = Cryptol.TCNum 2
      x@4 = Prelude.Vec 2 Prelude.Bool
      x@5 = Prelude.Vec 4 Prelude.Bool
      x@6 = Cryptol.PLiteralSeqBool (Cryptol.TCNum 4)
    }
 in Cryptol.ecAt x@3 x@5 x@4 (Cryptol.PIntegralSeqBool x@3)
      [Cryptol.ecNumber x@2 x@5 x@6, Cryptol.ecNumber x@3 x@5 x@6]
      (Cryptol.ecNumber x@2 x@4 (Cryptol.PLiteralSeqBool x@3))

What is that x@1 doing there? It is not used anywhere in the formula.

@brianhuffman
Copy link
Contributor

A quick search over the saw-core prelude reveals that Nat -> sort 0 -> sort 0 shows up as the type of the primitive Vec. Each occurrence of a constant or primitive in the term AST includes a reference to its type, so the term prettyprinter must have added a declaration x@1 because it found those two references to the same type.

However, the prettyprinter doesn't actually show the types of every constant, so we should really be excluding those when we collect all the subterms that are used multiple times. We just need to add another special case to function scTermCount in module Verifier.SAW.Term.Pretty in the saw-core package. This should be easy to fix.

@brianhuffman brianhuffman added the subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem label Apr 6, 2021
@brianhuffman brianhuffman self-assigned this Apr 6, 2021
@brianhuffman
Copy link
Contributor

With #1276, we now get the output you expect:

sawscript> {{ [0x1,0x2] @ 0b01 }}
[23:47:56.100] let { x@1 = Cryptol.TCNum 1
      x@2 = Cryptol.TCNum 2
      x@3 = Prelude.Vec 4 Prelude.Bool
      x@4 = Prelude.Vec 2 Prelude.Bool
      x@5 = Cryptol.PLiteralSeqBool (Cryptol.TCNum 4)
    }
 in Cryptol.ecAt x@2 x@3 x@4 (Cryptol.PIntegralSeqBool x@2)
      [Cryptol.ecNumber x@1 x@3 x@5, Cryptol.ecNumber x@2 x@3 x@5]
      (Cryptol.ecNumber x@1 x@4 (Cryptol.PLiteralSeqBool x@2))

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants