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

Add more information to printed JavaClass values #885

Open
brianhuffman opened this issue Oct 31, 2020 · 1 comment
Open

Add more information to printed JavaClass values #885

brianhuffman opened this issue Oct 31, 2020 · 1 comment
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm tech debt Issues that document or involve technical debt type: bug Issues reporting bugs or unexpected/unwanted behavior
Milestone

Comments

@brianhuffman
Copy link
Contributor

A saw-script JavaClass value, obtained from java_load_class, prints out a summary of the contents of the JVM class file. For example:

Class name: Test (super)
Superclass: java/lang/Object

Fields:
  default long val

Methods:
  void <init> ()
  void <init> (int)
  void <init> (long)
  long get ()
  void increment ()
  void increment (Test)
  void increment (int)
  void increment (long)

However, there are a couple of additional relevant pieces of information that would be good to add here. First of all, we should say whether each method is static or not, as that determines whether or not it should take a this reference as an extra first argument.

Also, in addition to the pretty-printed method type signatures, it might be nice to display the type descriptor string which can be used by the new crucible_jvm_verify command (as implemented in #884). Perhaps we could display those descriptor-extended names in a comment, but only for names that appear more than once.

@brianhuffman brianhuffman added the subsystem: crucible-jvm Issues related to Java verification with crucible-jvm label Oct 31, 2020
@brianhuffman brianhuffman self-assigned this Nov 13, 2020
@atomb atomb added this to the 0.8 milestone Nov 13, 2020
brianhuffman pushed a commit that referenced this issue Nov 14, 2020
brianhuffman pushed a commit that referenced this issue Nov 16, 2020
brianhuffman pushed a commit that referenced this issue Nov 17, 2020
brianhuffman pushed a commit that referenced this issue Nov 18, 2020
brianhuffman pushed a commit that referenced this issue Nov 18, 2020
@brianhuffman
Copy link
Contributor Author

We also need to improve the line-breaking and indentation for printing type signatures of methods with multiple arguments; it's pretty bad right now. Here's a selection from the pretty-printed java.math.BigInteger class:

  static java.math.BigInteger multiplyKaratsuba (java.math.BigInteger,
  java.math.BigInteger)
  static int[] multiplyToLen (int[],
  int,
  int[],
  int,
  int[])
  static java.math.BigInteger multiplyToomCook3 (java.math.BigInteger,
  java.math.BigInteger)
  java.math.BigInteger negate ()

As you can see, it's quite hard to read.

@atomb atomb modified the milestones: 0.8, 0.9 Apr 19, 2021
@atomb atomb removed this from the 0.9 milestone Sep 22, 2021
@sauclovian-g sauclovian-g added type: bug Issues reporting bugs or unexpected/unwanted behavior tech debt Issues that document or involve technical debt labels Oct 29, 2024
@sauclovian-g sauclovian-g added this to the Someday milestone Oct 29, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm tech debt Issues that document or involve technical debt type: bug Issues reporting bugs or unexpected/unwanted behavior
Projects
None yet
Development

No branches or pull requests

3 participants