crytic / tealer

Static Analyzer for Teal
GNU Affero General Public License v3.0
61 stars 14 forks source link

Add support to analyse and-or-! connected equations #132

Closed S3v3ru5 closed 1 year ago

S3v3ru5 commented 1 year ago

Fixes issues #90, #95

It is common to use logical operators to validate multiple fields at a time. examples include:

txn RekeyTo
global ZeroAddress
==
txn CloseRemainderTo
global ZeroAddress
==
&&
txn AssetCloseTo
global ZeroAddress
&&
assert
txn OnCompletion
int UpdateApplication
==
txn OnCompletion
int DeleteApplication
==
||
!                                  // txn is not UpdateApplication or DeleteApplication.
assert

More complex patterns could be used to perform transaction field validations. This PR adds support to infer information about interested fields when the comparison equations are combined using logical operators &&, ||, and !.

S3v3ru5 commented 1 year ago

Builds on #131