Verifying sanitizer correctness through black-box learning: A symbolic finite transducer approach