angr / claripy

An abstraction layer for constraint solvers.
BSD 2-Clause "Simplified" License
284 stars 93 forks source link

generate basic type-hint using pytest-monkeytype #352

Closed syheliel closed 3 months ago

syheliel commented 1 year ago
  1. install pytest-monkeytype
    pip install  pip install pytest-monkeytype
    pytest --monkeytype-output=./monkeytype.sqlite3 
  2. list stubed modules
    monkeytype list-modules
  3. apply stubs:
    
    #!/bin/bash

strings=( claripy.strings claripy.solvers claripy.simplifications claripy.operations claripy.frontend claripy.fp claripy.bv claripy.balancer claripy.backends claripy.backend_manager claripy.annotation )

for string in "${strings[@]}" do monkeytype apply "$string" --pep_563 done


notice that the type is generated by recording the execution of tests, so it can't infer the parent class when inheritance exists. Maunal efforts in #351 is still necessary. 
syheliel commented 1 year ago

Seems the import order cracks, let me fix it first

twizmwazin commented 1 year ago

This is pretty cool, but I think we would want to manually check over types before merging something like this. Would it be possible for you to also include runtime types observed during the angr test suite as well?

@zwimer has discussed how we mis-use types in claripy, and I think something like this could be a great way to identify those cases and fix them, to reduce the amount of complexity in a native port.

syheliel commented 1 year ago

mypy shows that Found 177 errors in 19 files (checked 70 source files). So type hinting should be built with serveral PR. But I'm currently working on to the type error in ./tests folder first.

syheliel commented 1 year ago

I tested monkeytype on angr. The test-suite for angr is too heavy for monkeytype to record the input.

syheliel commented 1 year ago

So far for this PR. Besides the monkeytype's modification, I have modified:

  1. backends/__init__.py, backends/backend.py: ensure correct import order
  2. claripy/ast/bv.py, claripy/ast/fp.py: add type hint for magic method like __add__. Now mypy can recognize operatior override

Other modification may be put in next PR.

rhelmot commented 1 year ago

You are duplicating work from the PR you linked at the start, which I am planning on merging tomorrow. Please be advised you will have merge conflicts.

syheliel commented 1 year ago

Can someone triggers the CI? I'd like to see if my code is correct.

syheliel commented 1 year ago

This should be the end of this PR... even still with lint's problem...

syheliel commented 1 year ago

Maybe trigger the CI? I'd like to let this to be merged

syheliel commented 1 year ago

I'm trying to eliminate mypy's error. Is this expected? Or I will add type: ignore[misc] for it.

claripy/solvers.py:97: error: Definition of "max" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "Frontend"  [misc]
claripy/solvers.py:97: error: Definition of "batch_eval" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "ConstraintFilterMixin"  [misc]
claripy/solvers.py:97: error: Definition of "batch_eval" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "LightFrontend"  [misc]
claripy/solvers.py:97: error: Definition of "batch_eval" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "ConstrainedFrontend"  [misc]
claripy/solvers.py:97: error: Definition of "batch_eval" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "Frontend"  [misc]
claripy/solvers.py:97: error: Definition of "is_true" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "ConstraintFilterMixin"  [misc]
claripy/solvers.py:97: error: Definition of "is_true" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "LightFrontend"  [misc]
claripy/solvers.py:97: error: Definition of "is_true" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "ConstrainedFrontend"  [misc]
claripy/solvers.py:97: error: Definition of "is_true" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "Frontend"  [misc]
claripy/solvers.py:97: error: Definition of "min" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "ConstraintFilterMixin"  [misc]
claripy/solvers.py:97: error: Definition of "min" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "LightFrontend"  [misc]
claripy/solvers.py:97: error: Definition of "min" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "ConstrainedFrontend"  [misc]
claripy/solvers.py:97: error: Definition of "min" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "Frontend"  [misc]
claripy/solvers.py:97: error: Definition of "eval" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "ConstraintFilterMixin"  [misc]
claripy/solvers.py:97: error: Definition of "eval" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "LightFrontend"  [misc]
claripy/solvers.py:97: error: Definition of "eval" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "ConstrainedFrontend"  [misc]
claripy/solvers.py:97: error: Definition of "eval" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "Frontend"  [misc]
claripy/solvers.py:97: error: Definition of "solution" in base class "ConcreteHandlerMixin" is incompatible with definition in base class "ConstraintFilterMixin"  [misc]
syheliel commented 1 year ago

reports is avaliable in https://github.com/syheliel/claripy/actions/runs/5185413513/jobs/9345293603

twizmwazin commented 3 months ago

While I am very supportive of adding more types and mypy, this doesn't seem like the right approach unless someone wants to spend a lot of time rebasing this work and cleaning up some of the weirder signatures.