testsmt / yinyang

A fuzzing framework for SMT solvers
https://testsmt.github.io/
MIT License
185 stars 23 forks source link

[A*] Improve Array type support by moving sort parsing logic from `sort2type` into `AstVisitor` #46

Closed maurobringolf closed 3 years ago

maurobringolf commented 3 years ago

I did some major changes on the handling of compound types, e.g. (Array (Array X Y) Y). As far as I understand, in the current code:

  1. The raw parser produces a structured representation of them, e.g. the grammar has all the necessary rules.
  2. The AstVisitor converts this structure into textual representation
  3. The sort2type function converts sort strings back to type objects ( ARRAY_TYPE, BITVECTOR_TYPE, etc.).

I propose to eliminate sort2type entirely and produce structured type representations in the AstVisitor directly, as done in this PR. This is only halfway done though, as BitVector and FloatingPoint is still parsed in sort2type.

Apart from that it looks like Opfuzz uses sort2type for constructing rules, so if that is needed then we could move sort2type into the opfuzz module.