Полная решающая процедура для теории ограниченной адресной арифметики

Процесс разработки кода на Си довольно часто сопровождается появлением ошибок, связанных с использованием указателей и адресов памяти. В связи с этим возникает потребность создания инструментов автоматизированной проверки программ. Одним из методов, применяемых такими инструментами проверки, является использование решающих процедур на основе SMT-решателей. Но в то же время разрешимые логики (комбинации логических теорий), требуемые для адекватного моделирования указателей в языке Си, непосредственно не присутствуют в стандарте SMT-LIB и не реализованы в большинстве существующих SMT-решателей. Одним из возможных способов поддержки таких логик является непосредственная их реализация в каком-либо SMT-решателе, однако такой подход часто оказывается трудоемким (требуется изменение исходного кода решателя), негибким (трудно модифицировать сигнатуру и семантику новых теорий) и ограниченным (требуется отдельная реализация поддержки теории в каждом используемом решателе). Другим способом является реализация пользовательских стратегий конечного инстанцирования кванторов для сведения формул в неподдерживаемых логиках к формулам в широко распространенных разрешимых логиках, таких как QF_UFLIA. В данной статье представлена процедура инстанцирования лемм для трансляции формул в теории типизированной адресной арифметики в логику QF_UFLIA. Для процедуры трансляции даны доказательства корректности и полноты, а также описана формализация этих доказательств в системе Isabelle/HOL. Сама теория адресной арифметики сформулирована на основе известных ошибок использования адресной арифметики в языке Си, а также спецификаций семантики этих операций из стандарта языка. Аналогичные доказательства и процедура также могут быть сформулированы для фрагмента теории бит-векторов (монотонные формулы над равенствами между выражениями с побитовыми операциями, такими как исключающее “или”, сдвиг, конкатенация, экстракция, отрицание). Представленная в статье процедура трансляции, в частности, позволяет легко реализовать полный метод доказательства утверждений в теории адресной арифметики в системе Isabelle/HOL на основе существующей в этой системе поддержки SMT-решателей (Z3 или VeriT).