Open depted opened 2 years ago
depted
commented
2 years ago [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
commented
1 year ago 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
commented
1 year ago 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)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. :)
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!