Parsing error

[depted]

Greetings,

While trying to parse code written in smtlibv2 through yinyang, I found some bugs that yinyang cannot parse some codes.

For example, parsing results of yinyang are (None, None) about the below codes.

Could I know why it happened?

Thanks for your time!

(set-info :smt-lib-version 2.6)
(set-logic QF_ABV)
(set-info :source |
Crafted benchmarks created for "Sharing is Caring: Combination of Theories" by Dejan Jovanovic and Clark Barrett. In Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCoS '11), Oct. 2011, pp. 195-210. Based on Example 4 from Section 5.
|)
(set-info :category "crafted")
(set-info :status sat)
(declare-fun a_0 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_0 () (_ BitVec 128))
(declare-fun a_1 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_1 () (_ BitVec 128))
(declare-fun a_2 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_2 () (_ BitVec 128))
(declare-fun a_3 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_3 () (_ BitVec 128))
(declare-fun a_4 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_4 () (_ BitVec 128))
(declare-fun a_5 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_5 () (_ BitVec 128))
(declare-fun a_6 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_6 () (_ BitVec 128))
(declare-fun a_7 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_7 () (_ BitVec 128))
(declare-fun a_8 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_8 () (_ BitVec 128))
(declare-fun a_9 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_9 () (_ BitVec 128))
(declare-fun a_10 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_10 () (_ BitVec 128))
(declare-fun a_11 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_11 () (_ BitVec 128))
(declare-fun a_12 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_12 () (_ BitVec 128))
(declare-fun a_13 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_13 () (_ BitVec 128))
(declare-fun a_14 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_14 () (_ BitVec 128))
(declare-fun a_15 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_15 () (_ BitVec 128))
(declare-fun a_16 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_16 () (_ BitVec 128))
(declare-fun a_17 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_17 () (_ BitVec 128))
(declare-fun a_18 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_18 () (_ BitVec 128))
(declare-fun a_19 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_19 () (_ BitVec 128))
(declare-fun a_20 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_20 () (_ BitVec 128))
(declare-fun a_21 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_21 () (_ BitVec 128))
(declare-fun a_22 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_22 () (_ BitVec 128))
(declare-fun a_23 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_23 () (_ BitVec 128))
(declare-fun a_24 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_24 () (_ BitVec 128))
(declare-fun a_25 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_25 () (_ BitVec 128))
(declare-fun a_26 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_26 () (_ BitVec 128))
(declare-fun a_27 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_27 () (_ BitVec 128))
(declare-fun a_28 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_28 () (_ BitVec 128))
(declare-fun a_29 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_29 () (_ BitVec 128))
(declare-fun a_30 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_30 () (_ BitVec 128))
(declare-fun a_31 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_31 () (_ BitVec 128))
(declare-fun a_32 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_32 () (_ BitVec 128))
(declare-fun a_33 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_33 () (_ BitVec 128))
(declare-fun a_34 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_34 () (_ BitVec 128))
(declare-fun a_35 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_35 () (_ BitVec 128))
(declare-fun a_36 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_36 () (_ BitVec 128))
(declare-fun a_37 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_37 () (_ BitVec 128))
(declare-fun a_38 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_38 () (_ BitVec 128))
(declare-fun a_39 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_39 () (_ BitVec 128))
(declare-fun a_40 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_40 () (_ BitVec 128))
(declare-fun a_41 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_41 () (_ BitVec 128))
(declare-fun a_42 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_42 () (_ BitVec 128))
(declare-fun a_43 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_43 () (_ BitVec 128))
(declare-fun a_44 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_44 () (_ BitVec 128))
(declare-fun a_45 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_45 () (_ BitVec 128))
(declare-fun a_46 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_46 () (_ BitVec 128))
(declare-fun a_47 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_47 () (_ BitVec 128))
(declare-fun a_48 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_48 () (_ BitVec 128))
(declare-fun a_49 () (Array (_ BitVec 128) (_ BitVec 128)))
(declare-fun x_49 () (_ BitVec 128))
(assert (not (= (select a_0 (bvmul x_0 x_1)) (select a_1 (bvmul x_1 x_2)))))
(assert (not (= (select a_1 (bvmul x_1 x_2)) (select a_2 (bvmul x_2 x_3)))))
(assert (not (= (select a_2 (bvmul x_2 x_3)) (select a_3 (bvmul x_3 x_4)))))
(assert (not (= (select a_3 (bvmul x_3 x_4)) (select a_4 (bvmul x_4 x_5)))))
(assert (not (= (select a_4 (bvmul x_4 x_5)) (select a_5 (bvmul x_5 x_6)))))
(assert (not (= (select a_5 (bvmul x_5 x_6)) (select a_6 (bvmul x_6 x_7)))))
(assert (not (= (select a_6 (bvmul x_6 x_7)) (select a_7 (bvmul x_7 x_8)))))
(assert (not (= (select a_7 (bvmul x_7 x_8)) (select a_8 (bvmul x_8 x_9)))))
(assert (not (= (select a_8 (bvmul x_8 x_9)) (select a_9 (bvmul x_9 x_10)))))
(assert (not (= (select a_9 (bvmul x_9 x_10)) (select a_10 (bvmul x_10 x_11)))))
(assert (not (= (select a_10 (bvmul x_10 x_11)) (select a_11 (bvmul x_11 x_12)))))
(assert (not (= (select a_11 (bvmul x_11 x_12)) (select a_12 (bvmul x_12 x_13)))))
(assert (not (= (select a_12 (bvmul x_12 x_13)) (select a_13 (bvmul x_13 x_14)))))
(assert (not (= (select a_13 (bvmul x_13 x_14)) (select a_14 (bvmul x_14 x_15)))))
(assert (not (= (select a_14 (bvmul x_14 x_15)) (select a_15 (bvmul x_15 x_16)))))
(assert (not (= (select a_15 (bvmul x_15 x_16)) (select a_16 (bvmul x_16 x_17)))))
(assert (not (= (select a_16 (bvmul x_16 x_17)) (select a_17 (bvmul x_17 x_18)))))
(assert (not (= (select a_17 (bvmul x_17 x_18)) (select a_18 (bvmul x_18 x_19)))))
(assert (not (= (select a_18 (bvmul x_18 x_19)) (select a_19 (bvmul x_19 x_20)))))
(assert (not (= (select a_19 (bvmul x_19 x_20)) (select a_20 (bvmul x_20 x_21)))))
(assert (not (= (select a_20 (bvmul x_20 x_21)) (select a_21 (bvmul x_21 x_22)))))
(assert (not (= (select a_21 (bvmul x_21 x_22)) (select a_22 (bvmul x_22 x_23)))))
(assert (not (= (select a_22 (bvmul x_22 x_23)) (select a_23 (bvmul x_23 x_24)))))
(assert (not (= (select a_23 (bvmul x_23 x_24)) (select a_24 (bvmul x_24 x_25)))))
(assert (not (= (select a_24 (bvmul x_24 x_25)) (select a_25 (bvmul x_25 x_26)))))
(assert (not (= (select a_25 (bvmul x_25 x_26)) (select a_26 (bvmul x_26 x_27)))))
(assert (not (= (select a_26 (bvmul x_26 x_27)) (select a_27 (bvmul x_27 x_28)))))
(assert (not (= (select a_27 (bvmul x_27 x_28)) (select a_28 (bvmul x_28 x_29)))))
(assert (not (= (select a_28 (bvmul x_28 x_29)) (select a_29 (bvmul x_29 x_30)))))
(assert (not (= (select a_29 (bvmul x_29 x_30)) (select a_30 (bvmul x_30 x_31)))))
(assert (not (= (select a_30 (bvmul x_30 x_31)) (select a_31 (bvmul x_31 x_32)))))
(assert (not (= (select a_31 (bvmul x_31 x_32)) (select a_32 (bvmul x_32 x_33)))))
(assert (not (= (select a_32 (bvmul x_32 x_33)) (select a_33 (bvmul x_33 x_34)))))
(assert (not (= (select a_33 (bvmul x_33 x_34)) (select a_34 (bvmul x_34 x_35)))))
(assert (not (= (select a_34 (bvmul x_34 x_35)) (select a_35 (bvmul x_35 x_36)))))
(assert (not (= (select a_35 (bvmul x_35 x_36)) (select a_36 (bvmul x_36 x_37)))))
(assert (not (= (select a_36 (bvmul x_36 x_37)) (select a_37 (bvmul x_37 x_38)))))
(assert (not (= (select a_37 (bvmul x_37 x_38)) (select a_38 (bvmul x_38 x_39)))))
(assert (not (= (select a_38 (bvmul x_38 x_39)) (select a_39 (bvmul x_39 x_40)))))
(assert (not (= (select a_39 (bvmul x_39 x_40)) (select a_40 (bvmul x_40 x_41)))))
(assert (not (= (select a_40 (bvmul x_40 x_41)) (select a_41 (bvmul x_41 x_42)))))
(assert (not (= (select a_41 (bvmul x_41 x_42)) (select a_42 (bvmul x_42 x_43)))))
(assert (not (= (select a_42 (bvmul x_42 x_43)) (select a_43 (bvmul x_43 x_44)))))
(assert (not (= (select a_43 (bvmul x_43 x_44)) (select a_44 (bvmul x_44 x_45)))))
(assert (not (= (select a_44 (bvmul x_44 x_45)) (select a_45 (bvmul x_45 x_46)))))
(assert (not (= (select a_45 (bvmul x_45 x_46)) (select a_46 (bvmul x_46 x_47)))))
(assert (not (= (select a_46 (bvmul x_46 x_47)) (select a_47 (bvmul x_47 x_48)))))
(assert (not (= (select a_47 (bvmul x_47 x_48)) (select a_48 (bvmul x_48 x_49)))))
(assert (not (= (select a_48 (bvmul x_48 x_49)) (select a_49 (bvmul x_49 x_0)))))
(assert (not (= (select a_49 (bvmul x_49 x_0)) (select a_0 (bvmul x_0 x_1)))))
(check-sat)
(exit)

[depted]

[2022/12/05 04:30:38 AM] Strategy: typefuzz, 2 testing targets, 15084 seeds
Runtime error at /home/smtfuzz/venv/lib/python3.10/site-packages/yinyang/src/parsing/Typechecker.py:524
msg: 'str' object has no attribute 'index_type'
cmd: /home/smtfuzz/venv/bin/typefuzz "z3 model_validate=true;cvc4 --check-models -m -i -q" QF_ABV
version: yinyang 0.3.0 unknown
Please file an issue: https://github.com/testsmt/yinyang/issues

[muchang]

Hi @fwangdo, sorry for the late reply. Does this issue still exist on your side? It seems that yinyang has no runtime error for this case now.

[depted]

Greetings, @muchang. First of all, thanks for your attention.

As for your question, yes, I have this issue still in the latest commit version as well. The code below is what I used to know the result of parsing from yinyang implementation(Note that, 'bv.smt2' in the code below is what we reported before in this issue).

/yinyang# ./bin/typefuzz "z3 model_validate=true;cvc5 --check-models -m -i -q" ./bv.smt2
[2023/03/01 04:24:21 PM] Strategy: typefuzz, 2 testing targets, 1 seeds
the res of 'parse_file' is (None, None)
All seeds processed
1 seeds processed, 0 valid, 1 invalid
0 bug triggers found

/yinyang/tests# python3 ./BvTest.py
the res of 'parse_file' is (None, None)

/yinyang/tests# cat ./BvTest.py
# MIT License
#
# Copyright (c) [2020 - 2021] The yinyang authors
#
# Permission is hereby granted, free of charge, to any person obtaining a copy
# of this software and associated documentation files (the "Software"), to deal
# in the Software without restriction, including without limitation the rights
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
# copies of the Software, and to permit persons to whom the Software is
# furnished to do so, subject to the following conditions:
#
# The above copyright notice and this permission notice shall be included in
# all copies or substantial portions of the Software.
#
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
# SOFTWARE.

import unittest
import sys
sys.path.append("../")
import os
from yinyang.src.parsing.Parse import *
from yinyang.src.parsing.Typechecker import Context, typecheck
from yinyang.src.mutators.GenTypeAwareMutation.GenTypeAwareMutation import *
from yinyang.src.mutators.GenTypeAwareMutation.Util import *


def test():
    path = '../bv.smt2'
    parse_file(path)

if __name__ == "__main__":
    test()

I changed parse_file in Parse.py a little bit like this.

 def parse_file(fn, timeout_limit=30, silent=True):
    """
    Parse SMT-LIB file.

    :fn: path to SMT-LIB file.
    :silent: if silent=True the parser will withhold stacktrace from user
             on crash.
    :returns: Script object representing AST of SMT-LIB file. None if timeout
              or crash occurred.
    """
    res = parse(parse_filestream, fn, timeout_limit, silent)
    print("the res of 'parse_file' is", res)
    return parse(parse_filestream, fn, timeout_limit, silent)

[depted]

Is there anything that I did wrong? If so, I hope you tell me the point. I will use yinyang in your intention and tell you the result. :)