# LLM4SS **Repository Path**: lapulatos/llm4-ss ## Basic Information - **Project Name**: LLM4SS - **Description**: This project aims to leverage existing open-source LLMs such as ChatGPT and the CPAchecker verification suite to enhance configurable program analysis. - **Primary Language**: Unknown - **License**: Not specified - **Default Branch**: master - **Homepage**: None - **GVP Project**: No ## Statistics - **Stars**: 0 - **Forks**: 0 - **Created**: 2024-02-27 - **Last Updated**: 2024-03-07 ## Categories & Tags **Categories**: Uncategorized **Tags**: None ## README # Enhancing Configurable Program Analysis through LLM-driven Strategy Selection Based on Code Features ---------- ## 项目介绍 ### Background Configurable Program Analysis (CPA) is a technique that allows users to customize the analysis of programs based on their specific needs and preferences. The well-known framework, CPAchecker, facilitates easy configuration and subsequent automatic execution of program analysis and verification procedures. However, like many other program verification tools, CPAchecker requires users to choose both the strategy and configuration parameters. This often necessitates a deep understanding of the target source code and the use of expert knowledge to select strategies based on identified program features, which can be a tedious and error-prone process. In this paper, we present a novel approach to efficiently perform program verification tasks by harnessing the capabilities of Large Language Models (LLMs) to automatically select verification strategies based on code features. Our key insight is that LLMs possess advanced program comprehension capabilities, allowing them to serve as proficient human experts in identifying code features, selecting verification strategies, and generating configuration parameters. In this spirit, we begin by extracting relevant code snippets and querying LLMs to identify code features, such as arrays, pointers, floating points, loops, multi-threading, etc. Based on these identified code features, we propose a strategy selector to automatically choose the verification strategy. Finally, we execute the CPAchecker with the selected verification strategy and the generated configuration parameters. We evaluated our approach using a diverse set of 600 verification tasks. The results demonstrate the effectiveness of our approach, as it is not only characterized by simplicity and ease of comprehension, but also outperforms individual methods. ### Goals This project aims to leverage existing open-source LLMs such as ChatGPT and the CPAchecker verification suite to enhance configurable program analysis. ---------- ## 安装和部署 ### Requirements - Hardware Requirements: Workstations/PC with multi-core processors - Operating System: >= Ubuntu 18.04 LTS ### 克隆LLM-Toolset父仓库，并测试GPT-3.5和GPT-4的可用性 ```sh # clone repo. $ git clone https://github.com/wcventure/LLM-Toolset.git $ cd LLM-Toolset # Install core dependencies (required) $ pip3 install -r requirements.txt # or $ pip3 install -r requirements.txt -i http://pypi.douban.com/simple --trusted-host pypi.douban.com ``` The template for the configuration file is located in the config template.json file in the conf directory, and the template needs to be copied to create the final effective config.json file: ```sh $ cp config-template.json config.json ``` Please edit your proxy IP in conf/conf.json, for example: ``` { "proxy": "http://127.0.0.1:4780", "https_proxy": "http://127.0.0.1:4780", "http_proxy": "http://127.0.0.1:4780", } ``` （如果你在海外，或使用全局模式的话，双引号内为空就可） A simple example is already prepared in the tutorial folder. A simplified library is in turorial/libgpt.py folder. Running the following command to query the ChatGPT with the sample prompt. ```sh $ python3 tutorial/hello_world.py ``` ### 克隆CFStra子仓库 ```sh # clone sub repo. $ cd LLM-Toolset $ git clone https://gitee.com/lapulatos/llm4-ss.git CFStra ``` ### 安装CPAchecker ``` # install cpachecker. $ cd LLM-Toolset/CFStra $ bash ./scripts/intall/install_cpachecker.sh ``` ### 安装BenchExec ``` # install benchexec. $ git clone https://github.com/sosy-lab/benchexec.git $ source ./scripts/install/install_benchexec.sh ``` ---------- ## Usage ### Set up Environment Everytime you open a new terminal you need to set up an environment variable. ```sh # set up environment $ cd LLM-Toolset $ export PYTHONPATH=$PWD:$PYTHONPATH ``` ### Determine the strategy to verify a program Usage: ``` usage: strategy_selection.py [-h] -s SOURCE_FILE -p PROPERTY_FILE [-m {gpt-3.5-turbo,gpt-3.5-turbo-0613,gpt-3.5-turbo-16k,gpt-3.5-turbo-16k-0613,gpt-4,gpt-4-0613,gpt-4-32k,gpt-4-32k-0613}] [-a {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}] [-ef] [-ss] -sd STRATEGY_DESCRIPTION_FILE -pt {spc,fc,spfc} [-d MAX_DEPTH] [-e ENTRY_POINT] [-l {c,c++,python,java,ruby,go,javascript}] options: -h, --help show this help message and exit -s SOURCE_FILE, --source-file SOURCE_FILE The input source code file. -p PROPERTY_FILE, --property-file PROPERTY_FILE The input property file that contains the specifications to be verified. -m {gpt-3.5-turbo,gpt-3.5-turbo-0613,gpt-3.5-turbo-16k,gpt-3.5-turbo-16k-0613,gpt-4,gpt-4-0613,gpt-4-32k,gpt-4-32k-0613}, --llm-model {gpt-3.5-turbo,gpt-3.5-turbo-0613,gpt-3.5-turbo-16k,gpt-3.5-turbo-16k-0613,gpt-4,gpt-4-0613,gpt-4-32k,gpt-4-32k-0613} The LLM model used to perform the feature extraction and strategy selection operations. -a {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}, --api-key-no {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19} The API key. -ef, --use-llm-extract-feature Whether use LLM to extract feature. If this option not enabled, then feature will be empty. -ss, --use-llm-select-strategy Whether use LLM to select strategy. If this options not enabled, then strategy will be selected manually. -sd STRATEGY_DESCRIPTION_FILE, --strategy-description-file STRATEGY_DESCRIPTION_FILE The strategy description file that contains the description of each strategy. -pt {spc,fc,spfc}, --prompt-template {spc,fc,spfc} The prompt used in selecting the strategy. -d MAX_DEPTH, --depth MAX_DEPTH The maximum search depth of caller function (default: 2). -e ENTRY_POINT, --entry-point ENTRY_POINT The entry point of the source file (default: main). -l {c,c++,python,java,ruby,go,javascript}, --analysis-language {c,c++,python,java,ruby,go,javascript} The programming language of the source code. ``` For example: `test/test.c` ```C // This file is part of the SV-Benchmarks collection of verification tasks: // https://github.com/sosy-lab/sv-benchmarks // // SPDX-FileCopyrightText: 2011-2020 The SV-Benchmarks community // SPDX-FileCopyrightText: The CSeq project // // SPDX-License-Identifier: Apache-2.0 extern void abort(void); #include void reach_error() { assert(0); } #include #include #include void __VERIFIER_assert(int expression) { if (!expression) { ERROR: {reach_error();abort();}}; return; } char *v; void *thread1(void * arg) { v = calloc(8, sizeof(char)); return 0; } void *thread2(void *arg) { if (v) strcpy(v, "Bigshot"); return 0; } int main() { pthread_t t1, t2; pthread_create(&t1, 0, thread1, 0); pthread_create(&t2, 0, thread2, 0); pthread_join(t1, 0); pthread_join(t2, 0); __VERIFIER_assert(!v || v[0] == 'B'); return 0; } ``` run `python3 ./confselect/strategy_selection.py -s ./test/test.c -p ./test/unreach-call.prp -ef -sd ./config/strategy_descriptions.txt` Then you can utilize LLM to extract the features of code and specification, and get the predict stratetgy file `config/svcomp23-pichecker.properties` in a fixed strategy selection order, looks like: ```C INFO:root:👻: What are the features of the given source code and specification? INFO:root:LLM querying ... 👽: Code Features: Concurrency Specification Features: unreach INFO:root:total_token: 820 Selected Config: config/svcomp23-pichecker.properties start time: 2024-02-27 13:56:51.804696, stop time: 2024-02-27 13:56:54.877647 @@@ Finished @@@ ``` run `python3 ./confselect/strategy_selection.py -s ./test/test.c -p ./test/unreach-call.prp -ef -ss -sd ./config/strategy_descriptions.txt -pt fc` Then you can utilize LLM to extract the features of code and specification, and then use LLM to get the predict stratetgy file `config/svcomp23-pichecker.properties`, looks like: ``` INFO:root:👻: What are the features of the given source code and specification? INFO:root:LLM querying ... 👽: Code Features: Concurrency, Pointer, Array Access, Member Variable Access Specification Features: Unreach INFO:root:total_token: 790 INFO:root:👻: What is the best strategy for verifying the given program? INFO:root:LLM querying ... 👽: Selected Config: PIChecker INFO:root:total_token: 1589 Selected Config: config/svcomp23-pichecker.properties start time: 2024-02-27 14:05:48.277121, stop time: 2024-02-27 14:05:52.078079 @@@ Finished @@@ ``` ### Benchmarking Task definition: ```XML **/*.graphml ../sv-benchmarks/c/ConcurrencySafety-Main.set ../sv-benchmarks/c/properties/unreach-call.prp Used algorithm property ``` run `benchexec --no-container --tool-directory ./CFStra ./cfstra.xml` ----------