GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
438 stars 63 forks source link

Add more information to printed `JavaClass` values #885

Open brianhuffman opened 4 years ago

brianhuffman commented 4 years ago

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 commented 3 years ago

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.