VeriSmart-public icon indicating copy to clipboard operation
VeriSmart-public copied to clipboard

How to use src/exploit/train.py

Open summer-gcc opened this issue 2 years ago • 2 comments

What is the input of train.py, when I input a contract file, an error occurs

python3 train.py --input ~/VeriSmart-public/examples/example2.sol --ngram 2 --maxtime 10000 Traceback (most recent call last): File "train.py", line 402, in main() File "train.py", line 335, in main lines = list (filter (lambda line: float(line['disproven_time']) <= args.maxtime, lines)) File "train.py", line 335, in lines = list (filter (lambda line: float(line['disproven_time']) <= args.maxtime, lines)) KeyError: 'disproven_time'

summer-gcc avatar May 11 '22 07:05 summer-gcc

Hi @summer-gcc ,

The input should be analysis results generated from the tool, not Solidity files.

I will add a manual for it as soon as possible, and let you know.

sunbeomso avatar May 12 '22 01:05 sunbeomso

thank you for your reply,and I would like to ask, when using the command -ngram 3, an error will appear, indicating that there is no such file, how to generate these files

~/t/VeriSmart-public master !2 ?6 ▓▒░ ./main.native -input examples/example2.sol -mode exploit -exploit_timeout 10 io -debug prob -ngram 2 [CHECKER] Integer Over/Underflows

  • all funcs : 12
  • reachable : 11
  • [STEP] Generating Paths ... took 8.7e-05s
  • #paths : 18

[INFO] Violate CEI: false [INFO] msg.sender = this possible: false Model Uploading ... Sys_error("./src/exploit/train/typeRank.txt: No such file or directory") Raised by primitive operation at file "stdlib.ml", line 390, characters 28-54 Called from file "src/batFile.ml", line 160, characters 49-82 Called from file "src/batFile.ml", line 170, characters 35-49 Called from file "src/exploit/exploit.ml", line 165, characters 28-51 Called from file "src/exploit/exploit.ml", line 195, characters 39-83 Called from file "src/main.ml", line 55, characters 16-40 Called from file "src/main.ml", line 97, characters 12-19

When I add the -validate command, it prompts that there is no ValiSmarTest/scripts/run.py file

~/test/VeriSmart-public master !3 ?7 ▓▒░ ./main.native -input examples/example2.sol -mode exploit -exploit_timeout 10 io -refined_vcgen -validate ░▒▓ ✔ 16:34:39 [CHECKER] Integer Over/Underflows

  • all funcs : 12
  • reachable : 11
  • [STEP] Generating Paths ... took 0.000129s
  • #paths : 18

[INFO] Violate CEI: false [INFO] msg.sender = this possible: false Model Uploading ... Generating Exploits ... Iter : 1, # of Workset Elements : 1, Total elapsed : 0.006221

Concrete Validation Begins ... python3: can't open file '/home/vkg/ValiSmarTest/scripts/run.py': [Errno 2] No such file or directory python3: can't open file '/home/vkg/ValiSmarTest/scripts/run.py': [Errno 2] No such file or directory python3: can't open file '/home/vkg/ValiSmarTest/scripts/run.py': [Errno 2] No such file or directory

summer-gcc avatar May 12 '22 01:05 summer-gcc