trailofbits / binary_type_inference

GNU General Public License v3.0
12 stars 0 forks source link

Property Tests for Transducer Simplification #16

Open 2over12 opened 2 years ago

2over12 commented 2 years ago

Need to look into the complexity theory of this but I think it should be possible to generate a push down system where the stack configuration of that weighted PDS is recognized by some regular language L. ie given an input language L generate a PDS with stack configurations that are = to L. If we can do that then we can generate the set of constraints represented by the PDS and compute the FSA. Then we can check if the FSA recognizes things outside the language L or that it recognizes things inside the language L.

If we can't get equality on the stack configurations we could also get weaker checking by constructing a PDS that is at least guaranteed to be recognized, or guaranteed to contain all words in L.