From c42ee6f719ce83e8df12eb755f18bdf12a0cbb72 Mon Sep 17 00:00:00 2001 From: Parniaan Date: Tue, 24 Sep 2024 13:07:46 -0700 Subject: [PATCH 1/2] Prepare Benchmarks --- .../CWE-22/path-traversal-wtih-open.dfy | 34 +++++++ dataset/cwe-dafny/methods.txt | 3 + .../task_id_1_with_expect.dfy | 2 +- ...h-traversal-with-open.py => cwe22-safe.py} | 0 dataset/cwe-python/CWE-22/cwe22-unsafe.dfy | 0 dataset/cwe-python/CWE-22/cwe22-unsafe.py | 0 dataset/cwe-python/CWE-378/cwe-378.py | 3 +- .../CWE-59/{ => scenario1}/cwe-59.py | 0 .../CWE-59/scenario2/cwe59-unsafe.py | 0 .../CWE-59/scenario2/task-description.txt | 5 + dataset/test/passwd.txt | 1 + .../interface/effectful-interface.dfy | 2 - ..._6-gpt-4-temp_0.0-k_1_verification_log.txt | 2 - .../task_id_6-gpt-4-temp_0.75-k_1.dfy | 11 --- .../task_id_6-gpt-4-temp_0.75-k_1.dfy} | 3 +- ...6-gpt-4-temp_0.75-k_1_verification_log.txt | 0 .../task_id_7-gpt-4-temp_0.75-k_1.dfy | 17 ++++ ...7-gpt-4-temp_0.75-k_1_verification_log.txt | 11 +++ .../task_id_7-gpt-4-temp_0.75-k_2.dfy | 20 ++++ ...7-gpt-4-temp_0.75-k_2_verification_log.txt | 11 +++ .../task_id_7-gpt-4-temp_0.75-k_3.dfy | 18 ++++ ...7-gpt-4-temp_0.75-k_3_verification_log.txt | 42 ++++++++ .../task_id_7-gpt-4-temp_0.75-k_4.dfy | 18 ++++ ...7-gpt-4-temp_0.75-k_4_verification_log.txt | 42 ++++++++ .../task_id_7-gpt-4-temp_0.75-k_5.dfy | 18 ++++ ...7-gpt-4-temp_0.75-k_5_verification_log.txt | 42 ++++++++ requirements.txt | 34 +++++-- src/components/core.py | 68 ++++++------- src/components/prompt_generator.py | 44 ++++----- src/components/task_generator.py | 99 +++++++++++++++++++ src/components/task_selector.py | 10 +- src/prompts_template/COT_TEMPLATE.file | 4 +- src/prompts_template/COT_template.txt | 21 ++++ src/prompts_template/COT_template_string.file | 23 +++++ src/prompts_template/task_template.md | 11 +++ src/tasks/task-7.json | 10 +- src/utils/config_reader.py | 2 + 37 files changed, 538 insertions(+), 93 deletions(-) create mode 100644 dataset/cwe-dafny/CWE-22/path-traversal-wtih-open.dfy create mode 100644 dataset/cwe-dafny/methods.txt rename dataset/{cwe-python => cwe-dafny}/task_id_1_with_expect.dfy (92%) rename dataset/cwe-python/CWE-22/{path-traversal-with-open.py => cwe22-safe.py} (100%) create mode 100644 dataset/cwe-python/CWE-22/cwe22-unsafe.dfy create mode 100644 dataset/cwe-python/CWE-22/cwe22-unsafe.py rename dataset/cwe-python/CWE-59/{ => scenario1}/cwe-59.py (100%) create mode 100644 dataset/cwe-python/CWE-59/scenario2/cwe59-unsafe.py create mode 100644 dataset/cwe-python/CWE-59/scenario2/task-description.txt create mode 100644 dataset/test/passwd.txt delete mode 100644 output/task_id_6/task_id_6-gpt-4-temp_0.0-k_1_verification_log.txt delete mode 100644 output/task_id_6/task_id_6-gpt-4-temp_0.75-k_1.dfy rename output/{task_id_6/task_id_6-gpt-4-temp_0.0-k_1.dfy => task_id_6_generated@2024-09-18-01-14/task_id_6-gpt-4-temp_0.75-k_1.dfy} (71%) rename output/{task_id_6 => task_id_6_generated@2024-09-18-01-14}/task_id_6-gpt-4-temp_0.75-k_1_verification_log.txt (100%) create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1.dfy create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1_verification_log.txt create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2.dfy create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2_verification_log.txt create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3_verification_log.txt create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4_verification_log.txt create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5_verification_log.txt create mode 100644 src/components/task_generator.py create mode 100644 src/prompts_template/COT_template.txt create mode 100644 src/prompts_template/COT_template_string.file create mode 100644 src/prompts_template/task_template.md diff --git a/dataset/cwe-dafny/CWE-22/path-traversal-wtih-open.dfy b/dataset/cwe-dafny/CWE-22/path-traversal-wtih-open.dfy new file mode 100644 index 0000000..11dc2d6 --- /dev/null +++ b/dataset/cwe-dafny/CWE-22/path-traversal-wtih-open.dfy @@ -0,0 +1,34 @@ +include "../../../filesystems-api/interface/effectful-interface.dfy" +method GetFile(filename: seq) returns (data: array) +// requires non_empty_string(filename) +// requires !has_dangerous_pattern(filename) +// requires is_valid_file_name(filename) +// requires has_valid_file_length(filename) +// requires is_valid_file_extension(filename) +{ + + var f: FileStream; + var ok: bool; + var base_dir: seq := "/var/www/files/"; + data := new byte[100]; + var file_path := Join(base_dir, filename); + // if (!has_dangerous_pattern(file_path)) { + print "base_dir is safe"; + ok, f := FileStream.Open(file_path); + + // if !ok { print "open failed"; return data; } + // // if is_valid_file_extension(file_path) { + // print "file extension is valid"; + // ok := f.Read(file_path, 0, data, 0, data.Length as int32); + // print "Read operation terminated safely"; + // } else { + // print "file extension is invalid"; + // return data; + // } + + // } else { + // print "base_dir is unsafe"; + // return data; + // } + +} \ No newline at end of file diff --git a/dataset/cwe-dafny/methods.txt b/dataset/cwe-dafny/methods.txt new file mode 100644 index 0000000..8d9ba13 --- /dev/null +++ b/dataset/cwe-dafny/methods.txt @@ -0,0 +1,3 @@ +1. add preconditions to JoinFileToPath +2. use if (...) checks to guard the function call to FileStream.Open +3. use expect (...) checks to add runtime checks that the preconditions hold \ No newline at end of file diff --git a/dataset/cwe-python/task_id_1_with_expect.dfy b/dataset/cwe-dafny/task_id_1_with_expect.dfy similarity index 92% rename from dataset/cwe-python/task_id_1_with_expect.dfy rename to dataset/cwe-dafny/task_id_1_with_expect.dfy index 5833954..8fd1fd8 100644 --- a/dataset/cwe-python/task_id_1_with_expect.dfy +++ b/dataset/cwe-dafny/task_id_1_with_expect.dfy @@ -1,4 +1,4 @@ -include "/Users/pari/pcc-llms/dataset/filesystems/interface/effectful-interface.dfy" +include "../../filesystems-api/interface/effectful-interface.dfy" method JoinFileToPath(path: seq, fname: seq) returns (jointPath: path) diff --git a/dataset/cwe-python/CWE-22/path-traversal-with-open.py b/dataset/cwe-python/CWE-22/cwe22-safe.py similarity index 100% rename from dataset/cwe-python/CWE-22/path-traversal-with-open.py rename to dataset/cwe-python/CWE-22/cwe22-safe.py diff --git a/dataset/cwe-python/CWE-22/cwe22-unsafe.dfy b/dataset/cwe-python/CWE-22/cwe22-unsafe.dfy new file mode 100644 index 0000000..e69de29 diff --git a/dataset/cwe-python/CWE-22/cwe22-unsafe.py b/dataset/cwe-python/CWE-22/cwe22-unsafe.py new file mode 100644 index 0000000..e69de29 diff --git a/dataset/cwe-python/CWE-378/cwe-378.py b/dataset/cwe-python/CWE-378/cwe-378.py index b5f2bbe..8761fa8 100644 --- a/dataset/cwe-python/CWE-378/cwe-378.py +++ b/dataset/cwe-python/CWE-378/cwe-378.py @@ -4,7 +4,7 @@ def process_sensitive_data(data): # Create a temporary file with default permissions - temp_file = tempfile.NamedTemporaryFile(mode='w+t', delete=False) + temp_file = tempfile.NamedTemporaryFile(mode='w+t', delete=False) # Add a temp txt file temp_file.write(data) temp_file.close() @@ -21,6 +21,7 @@ def process_sensitive_data(data): sensitive_info = "password123" result = process_sensitive_data(sensitive_info) +#TODO separate the safe code from the unsafe code and task description and add safe dafny version and a code completion sample in Dafny # A program that creates a temporary file to store sensitive data # The temporary file is created with default permissions, which might be # too permissive and allow other users on the system to read the sensitive data diff --git a/dataset/cwe-python/CWE-59/cwe-59.py b/dataset/cwe-python/CWE-59/scenario1/cwe-59.py similarity index 100% rename from dataset/cwe-python/CWE-59/cwe-59.py rename to dataset/cwe-python/CWE-59/scenario1/cwe-59.py diff --git a/dataset/cwe-python/CWE-59/scenario2/cwe59-unsafe.py b/dataset/cwe-python/CWE-59/scenario2/cwe59-unsafe.py new file mode 100644 index 0000000..e69de29 diff --git a/dataset/cwe-python/CWE-59/scenario2/task-description.txt b/dataset/cwe-python/CWE-59/scenario2/task-description.txt new file mode 100644 index 0000000..f2e4366 --- /dev/null +++ b/dataset/cwe-python/CWE-59/scenario2/task-description.txt @@ -0,0 +1,5 @@ +File retrieval and file upload for a username + +1. Take a username as input +2. Construct a path to a file named "user_data.txt" in the user's home directory +3. If the file exists, read and return its contents \ No newline at end of file diff --git a/dataset/test/passwd.txt b/dataset/test/passwd.txt new file mode 100644 index 0000000..d5205a0 --- /dev/null +++ b/dataset/test/passwd.txt @@ -0,0 +1 @@ +uehfyJHD$73@0!j.Lz \ No newline at end of file diff --git a/filesystems-api/interface/effectful-interface.dfy b/filesystems-api/interface/effectful-interface.dfy index df6d9ef..b4215a8 100644 --- a/filesystems-api/interface/effectful-interface.dfy +++ b/filesystems-api/interface/effectful-interface.dfy @@ -119,8 +119,6 @@ class FileStream requires has_absoloute_path(p) requires is_valid_file_extension(p) requires has_valid_content_length(buffer) - requires is_valid_file_extension(p) - requires is_valid_file_extension(p) requires IsOpen() requires 0 <= start as int <= end as int <= buffer.Length modifies buffer diff --git a/output/task_id_6/task_id_6-gpt-4-temp_0.0-k_1_verification_log.txt b/output/task_id_6/task_id_6-gpt-4-temp_0.0-k_1_verification_log.txt deleted file mode 100644 index 823a60a..0000000 --- a/output/task_id_6/task_id_6-gpt-4-temp_0.0-k_1_verification_log.txt +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 1 verified, 0 errors diff --git a/output/task_id_6/task_id_6-gpt-4-temp_0.75-k_1.dfy b/output/task_id_6/task_id_6-gpt-4-temp_0.75-k_1.dfy deleted file mode 100644 index 0b995fe..0000000 --- a/output/task_id_6/task_id_6-gpt-4-temp_0.75-k_1.dfy +++ /dev/null @@ -1,11 +0,0 @@ -include "/Users/pari/pcc-llms/dataset/filesystems/interface/effectful-interface.dfy" - -method CreateFullPath(filename: seq) returns (fullPath: seq) - requires non_empty_string(filename) - requires !has_dangerous_pattern(filename) - requires is_valid_file_name(filename) - requires has_valid_file_length(filename) - { - var dir: seq := "/home/user/documents"; // The predetermined directory - fullPath := Join(dir, filename); - } \ No newline at end of file diff --git a/output/task_id_6/task_id_6-gpt-4-temp_0.0-k_1.dfy b/output/task_id_6_generated@2024-09-18-01-14/task_id_6-gpt-4-temp_0.75-k_1.dfy similarity index 71% rename from output/task_id_6/task_id_6-gpt-4-temp_0.0-k_1.dfy rename to output/task_id_6_generated@2024-09-18-01-14/task_id_6-gpt-4-temp_0.75-k_1.dfy index 6197130..a6d328b 100644 --- a/output/task_id_6/task_id_6-gpt-4-temp_0.0-k_1.dfy +++ b/output/task_id_6_generated@2024-09-18-01-14/task_id_6-gpt-4-temp_0.75-k_1.dfy @@ -1,6 +1,7 @@ -include "/Users/pari/pcc-llms/dataset/filesystems/interface/effectful-interface.dfy" +include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy" method CreateFullPath(filename: seq) returns (fullPath: seq) + requires non_empty_string(filename) requires !has_dangerous_pattern(filename) requires is_valid_file_name(filename) requires has_valid_file_length(filename) diff --git a/output/task_id_6/task_id_6-gpt-4-temp_0.75-k_1_verification_log.txt b/output/task_id_6_generated@2024-09-18-01-14/task_id_6-gpt-4-temp_0.75-k_1_verification_log.txt similarity index 100% rename from output/task_id_6/task_id_6-gpt-4-temp_0.75-k_1_verification_log.txt rename to output/task_id_6_generated@2024-09-18-01-14/task_id_6-gpt-4-temp_0.75-k_1_verification_log.txt diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1.dfy b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1.dfy new file mode 100644 index 0000000..fd3be72 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1.dfy @@ -0,0 +1,17 @@ +include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy" + +method GetFile(filename: seq) returns (data: array) + requires non_empty_string(filename) + requires !has_dangerous_pattern(filename) + requires is_valid_file_name(filename) + requires has_valid_file_length(filename) + { + var directory: seq := "/var/www/files/"; + var f: FileStream; + var fullpath := Join(directory, filename); + var ok: bool; + ok, f := Open(fullpath); + if !ok { print "open failed"; return new byte[0]; } + data := new byte[100]; + ok := f.Read(fullpath, 0, data, 0, data.Length as int32); + } \ No newline at end of file diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1_verification_log.txt b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1_verification_log.txt new file mode 100644 index 0000000..27aa516 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1_verification_log.txt @@ -0,0 +1,11 @@ +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1.dfy(13,14): Error: unresolved identifier: Open + | +13 | ok, f := Open(fullpath); + | ^^^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1.dfy(13,11): Error: the number of left-hand sides (2) and right-hand sides (1) must match for a multi-assignment + | +13 | ok, f := Open(fullpath); + | ^^ + +2 resolution/type errors detected in task_id_7-gpt-4-temp_0.75-k_1.dfy diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2.dfy b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2.dfy new file mode 100644 index 0000000..1500497 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2.dfy @@ -0,0 +1,20 @@ +include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy" + +method GetFile(filename: seq) returns (data: array) + requires !has_dangerous_pattern(filename) + requires is_valid_file_extension(filename) + requires is_valid_file_name(filename) + requires has_valid_file_length(filename) + requires has_absoloute_path(filename) + requires non_empty_string(filename) + { + var f: FileStream; + var ok: bool; + var path: array := "/var/www/files/"; + var fullPath := Join(path, filename); + ok, f := FileStream.Open(fullPath); + if !ok { print "open failed"; return new byte[0]; } + data := new byte[100]; + ok := f.Read(fullPath, 0, data, 0, data.Length as int32); + print "File read completed!\n"; + } \ No newline at end of file diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2_verification_log.txt b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2_verification_log.txt new file mode 100644 index 0000000..e483698 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2_verification_log.txt @@ -0,0 +1,11 @@ +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2.dfy(13,27): Error: RHS (of type string) not assignable to LHS (of type array) + | +13 | var path: array := "/var/www/files/"; + | ^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2.dfy(14,21): Error: incorrect argument type at index 0 for method in-parameter 'p' (expected path, found array) + | +14 | var fullPath := Join(path, filename); + | ^^^^^^^^^^^^^^^^^^^^ + +2 resolution/type errors detected in task_id_7-gpt-4-temp_0.75-k_2.dfy diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy new file mode 100644 index 0000000..a61e3c3 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy @@ -0,0 +1,18 @@ +include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy" + +method GetFile(filename: seq) returns (data: array) + requires !has_dangerous_pattern(filename) + requires is_valid_file_name(filename) + requires non_empty_string(filename) + requires has_valid_file_length(filename) + { + var folderPath: seq := "/var/www/files/"; + var fullPath: seq := Join(folderPath, filename); + var f: FileStream; + var ok: bool; + ok, f := FileStream.Open(fullPath); + if !ok { print "open failed\n"; return new byte[0]; } + data := new byte[100]; + ok := f.Read(fullPath, 0, data, 0, data.Length as int32); + print "File data loaded!\n"; + } \ No newline at end of file diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3_verification_log.txt b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3_verification_log.txt new file mode 100644 index 0000000..f2d23be --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3_verification_log.txt @@ -0,0 +1,42 @@ +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy(13,4): Error: a precondition for this call could not be proved + | +13 | ok, f := FileStream.Open(fullPath); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(104,13): Related location: this is the precondition that could not be proved + | +104 | requires !has_dangerous_pattern(name) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy(16,4): Error: a precondition for this call could not be proved + | +16 | ok := f.Read(fullPath, 0, data, 0, data.Length as int32); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved + | +120 | requires is_valid_file_extension(p) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(211,4): Related location: this proposition could not be proved + | +211 | lastDotIndex >= 0 && + | ^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy(16,4): Error: a precondition for this call could not be proved + | +16 | ok := f.Read(fullPath, 0, data, 0, data.Length as int32); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved + | +120 | requires is_valid_file_extension(p) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(212,4): Related location: this proposition could not be proved + | +212 | lastDotIndex < |filename| - 1 && + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + + +Dafny program verifier finished with 0 verified, 3 errors diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy new file mode 100644 index 0000000..6e17a76 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy @@ -0,0 +1,18 @@ +include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy" + +method GetFile(filename: seq) returns (data: array) + requires !has_dangerous_pattern(filename) + requires is_valid_file_name(filename) + requires non_empty_string(filename) + requires has_valid_file_length(filename) + { + var f: FileStream; + var ok: bool; + var dir: path := "/var/www/files/"; + var fullpath: path := Join(dir, filename); + ok, f := FileStream.Open(fullpath); + if !ok { print "open failed\n"; return new byte[0]; } + data := new byte[100]; + ok := f.Read(fullpath, 0, data, 0, data.Length as int32); + print "File data loaded!\n"; + } \ No newline at end of file diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4_verification_log.txt b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4_verification_log.txt new file mode 100644 index 0000000..4858da3 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4_verification_log.txt @@ -0,0 +1,42 @@ +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy(13,3): Error: a precondition for this call could not be proved + | +13 | ok, f := FileStream.Open(fullpath); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(104,13): Related location: this is the precondition that could not be proved + | +104 | requires !has_dangerous_pattern(name) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy(16,3): Error: a precondition for this call could not be proved + | +16 | ok := f.Read(fullpath, 0, data, 0, data.Length as int32); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved + | +120 | requires is_valid_file_extension(p) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(211,4): Related location: this proposition could not be proved + | +211 | lastDotIndex >= 0 && + | ^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy(16,3): Error: a precondition for this call could not be proved + | +16 | ok := f.Read(fullpath, 0, data, 0, data.Length as int32); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved + | +120 | requires is_valid_file_extension(p) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(212,4): Related location: this proposition could not be proved + | +212 | lastDotIndex < |filename| - 1 && + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + + +Dafny program verifier finished with 0 verified, 3 errors diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy new file mode 100644 index 0000000..e836ca8 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy @@ -0,0 +1,18 @@ +include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy" + +method GetFile(filename: seq) returns (data: array) + requires non_empty_string(filename) + requires !has_dangerous_pattern(filename) + requires is_valid_file_name(filename) + requires has_valid_file_length(filename) + { + var ok: bool; + var f: FileStream; + var directory: path := "/var/www/files/"; + var fullPath := Join(directory, filename); + ok, f := FileStream.Open(fullPath); + if !ok { print "open failed"; return new byte[0]; } + data := new byte[100]; + ok := f.Read(fullPath, 0, data, 0, data.Length as int32); + print "File data loaded!\n"; + } \ No newline at end of file diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5_verification_log.txt b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5_verification_log.txt new file mode 100644 index 0000000..68872b5 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5_verification_log.txt @@ -0,0 +1,42 @@ +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy(13,5): Error: a precondition for this call could not be proved + | +13 | ok, f := FileStream.Open(fullPath); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(104,13): Related location: this is the precondition that could not be proved + | +104 | requires !has_dangerous_pattern(name) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy(16,5): Error: a precondition for this call could not be proved + | +16 | ok := f.Read(fullPath, 0, data, 0, data.Length as int32); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved + | +120 | requires is_valid_file_extension(p) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(211,4): Related location: this proposition could not be proved + | +211 | lastDotIndex >= 0 && + | ^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy(16,5): Error: a precondition for this call could not be proved + | +16 | ok := f.Read(fullPath, 0, data, 0, data.Length as int32); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved + | +120 | requires is_valid_file_extension(p) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(212,4): Related location: this proposition could not be proved + | +212 | lastDotIndex < |filename| - 1 && + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + + +Dafny program verifier finished with 0 verified, 3 errors diff --git a/requirements.txt b/requirements.txt index 4414d8e..6035b44 100644 --- a/requirements.txt +++ b/requirements.txt @@ -12,6 +12,8 @@ bleach==6.1.0 certifi==2024.6.2 charset-normalizer==3.3.2 chevron==0.14.0 +click==8.1.7 +colorama==0.4.6 dataclasses-json==0.6.7 decorator==5.1.1 defusedxml==0.7.1 @@ -19,10 +21,14 @@ distro==1.9.0 docopt==0.6.2 executing==2.0.1 faiss-cpu==1.8.0 +fastapi==0.115.0 fastjsonschema==2.20.0 filelock==3.15.4 frozenlist==1.4.1 fsspec==2024.6.1 +gitdb==4.0.11 +GitPython==3.1.43 +gritql==0.1.5 h11==0.14.0 httpcore==1.0.5 httpx==0.27.0 @@ -41,17 +47,22 @@ jsonschema-specifications==2023.12.1 jupyter_client==8.6.2 jupyter_core==5.7.2 jupyterlab_pygments==0.3.0 -langchain==0.2.7 +langchain==0.3.0 langchain-anthropic==0.1.23 -langchain-community==0.2.7 -langchain-core==0.2.39 +langchain-cli==0.0.31 +langchain-community==0.3.0 +langchain-core==0.3.5 +langchain-experimental==0.3.0 langchain-openai==0.1.14 -langchain-text-splitters==0.2.2 -langsmith==0.1.117 +langchain-text-splitters==0.3.0 +langserve==0.3.0 +langsmith==0.1.125 lunary==1.1.3 +markdown-it-py==3.0.0 MarkupSafe==2.1.5 marshmallow==3.21.3 matplotlib-inline==0.1.7 +mdurl==0.1.2 mistune==3.0.2 mpmath==1.3.0 multidict==6.0.5 @@ -74,8 +85,9 @@ platformdirs==4.2.2 prompt_toolkit==3.0.47 ptyprocess==0.7.0 pure-eval==0.2.2 -pydantic==2.7.3 -pydantic_core==2.18.4 +pydantic==2.9.2 +pydantic-settings==2.5.2 +pydantic_core==2.23.4 Pygments==2.18.0 pyhumps==3.8.0 python-dateutil==2.9.0.post0 @@ -85,31 +97,39 @@ pyzmq==26.0.3 referencing==0.35.1 regex==2024.5.15 requests==2.32.3 +rich==13.8.1 rpds-py==0.18.1 safetensors==0.4.3 scikit-learn==1.5.1 scipy==1.14.0 sentence-transformers==3.0.1 setuptools==67.8.0 +shellingham==1.5.4 six==1.16.0 +smmap==5.0.1 sniffio==1.3.1 soupsieve==2.5 SQLAlchemy==2.0.31 +sse-starlette==1.8.2 stack-data==0.6.3 +starlette==0.38.6 sympy==1.13.0 tenacity==8.5.0 threadpoolctl==3.5.0 tiktoken==0.7.0 tinycss2==1.3.0 tokenizers==0.19.1 +tomlkit==0.12.5 torch==2.3.1 tornado==6.4.1 tqdm==4.66.4 traitlets==5.14.3 transformers==4.42.3 +typer==0.9.4 typing-inspect==0.9.0 typing_extensions==4.12.1 urllib3==2.2.2 +uvicorn==0.23.2 wcwidth==0.2.13 webencodings==0.5.1 yarg==0.1.9 diff --git a/src/components/core.py b/src/components/core.py index a381542..bc56049 100644 --- a/src/components/core.py +++ b/src/components/core.py @@ -11,13 +11,13 @@ import json import logging -from langchain.callbacks.base import BaseCallbackHandler +from langchain_core.callbacks import BaseCallbackHandler # from langchain.errors import ChainError, LLMErrors from langchain.globals import set_debug, set_verbose from langchain.memory import ConversationBufferMemory -from langchain.prompts import PromptTemplate -from langchain.schema import SystemMessage +from langchain_core.prompts import PromptTemplate +from langchain_core.messages import SystemMessage from langchain_anthropic import ChatAnthropic from langchain_community.callbacks.manager import get_openai_callback from langchain_community.chat_message_histories import ChatMessageHistory @@ -47,7 +47,7 @@ class Core: "safety_property": None, "required_files": None, "generate_code_file": None, - + } def __init__(self, max_history_length=1000): @@ -64,12 +64,12 @@ def count_tokens(self, chain, query): # print(f'Spent a total of {cb.total_tokens} tokens') return result, cb.total_tokens - + def initialize_llm(self, model_config, api_config): model = model_config['model'] if api_config["lunary_api_key"] is not None: self.lunary_handler = LunaryCallbackHandler(app_id=api_config["lunary_api_key"]) - + if model == "gpt-4": return ChatOpenAI(model_name="gpt-4", temperature=model_config['temp'], openai_api_key=api_config['openai_api_key'], callbacks=[self.lunary_handler], verbose=True) @@ -79,15 +79,15 @@ def initialize_llm(self, model_config, api_config): if model == "claude": return ChatAnthropic(model="claude-3-opus-20240229", temperature=model_config['temp'], api_key=api_config['claude_api_key'], callbacks=[self.lunary_handler], verbose=True) - + # def get_session_history(self, session_id: str) -> BaseChatMessageHistory: # if session_id not in self.store: # self.store[session_id] = ChatMessageHistory() # return self.store[session_id] - - + + # def fix_code(self, api_config, code, error): - + # code_fix_template = """ # The following Python code has an error: @@ -113,7 +113,7 @@ def initialize_llm(self, model_config, api_config): # def safe_extract_history(self, x): # # Safely extract chat history, returning an empty list if not found # return x.get("chat_history", {}).get("chat_history", []) - + # def load_memory_debug(self, code_memory): # memory_data = code_memory.load_memory_variables({}) # print(f"Loaded memory data: {memory_data}") # Debug print @@ -122,12 +122,12 @@ def safe_extract_history(self, x): chat_history = x.get("chat_history", {}).get("chat_history", []) # print(f"Extracted chat history: {chat_history}") # Debug print return chat_history - + def add_error_to_memory(self, validation_result): error_feedback = f"Error occurred. Let's try again." self.code_memory.chat_memory.add_message(SystemMessage(content=validation_result)) return error_feedback - + def invoke_llm(self, api_config, model_config, fewshot_config, new_task, example_db_5_tasks, code_example_selector, @@ -158,7 +158,7 @@ def on_llm_error(self, error: Exception, **kwargs): logging.error(f"LLM error: {str(error)}", exc_info=True) - + # Required for similarity_example_selector without lanchain # spec_examples_ids = [] # for key, task_list in similar_tasks.items(): @@ -169,27 +169,27 @@ def on_llm_error(self, error: Exception, **kwargs): # print() # Add a blank line for better readability # spec_examples_ids.append(task['task_id']) # print(f"\n spec_examples_ids \n {spec_examples_ids}") - + # similar_tasks = spec_example_selector.select_examples(new_task) # print(f"\n vc_example_selector \n {vc_example_selector}") - + prompt_gen = prompt_generator.PromptGenerator() # specification_prompt = prompt_gen.create_few_shot_specification_prompts(spec_examples_ids, # example_db_5_tasks, # vc_prompt_template) - + # print("\n Is specification_prompt correct ??????????????//////////////////////") # print(specification_prompt) # Memory # specification_memory = ConversationBufferMemory(input_key='task', memory_key='chat_history') - + # specification_chain = LLMChain(llm=llm, prompt=specification_prompt, verbose=False, output_key='specifications', # memory=specification_memory) - - + + print("\n new_task_description \n", new_task['task_description']) # Debug: Print memory contents before running the chain @@ -201,7 +201,7 @@ def on_llm_error(self, error: Exception, **kwargs): # print(f'\n Spent a total of {cb_spec.total_tokens} tokens for verification \n') # print(f"\n specification_response: \n {specification_response} \n") # next_input_task_with_spec = utils.parse_specification_response(new_task, specification_response) - + # print(f"\n next_input_task_with_spec: \n {next_input_task_with_spec} \n") # spec_similar_code_tasks = code_example_selector.select_examples(next_input_task_with_spec) # print(f"\n spec_similar_code_tasks = \n {spec_similar_code_tasks} \n") @@ -222,7 +222,7 @@ def on_llm_error(self, error: Exception, **kwargs): # print(f"{code_prompt}") # print(f"\n ================================") # utils.write_to_file("/Users/pari/pcc-llms/output/code_prompt.txt", code_prompt) - + # print(f"\n base_output_path {env_config["base_output_path"]} \n") # prompt_path = os.path.join(env_config["base_output_path"], # "dynamic-few-shot-prompt-" + str(K) + ".txt") @@ -234,28 +234,28 @@ def on_llm_error(self, error: Exception, **kwargs): # print(f"Error: The file {prompt_path} does not exist.") # except IOError as e: # print(f"Error reading the file {prompt_path}: {str(e)}") - + # config = RunnableConfig({"callbacks": [handler]}) # ************************** langchain deprecated ************************** # code_memory = ConversationBufferMemory(input_key='task', memory_key='chat_history') # print (f"\n code_memory: {code_memory} \n") # code_chain = LLMChain(llm=llm, prompt=code_prompt, verbose=False, output_key='script', memory=self.code_memory) - - + + # ************************************************************************** # Create memory - + # code_memory = ConversationBufferMemory(input_key=['task', 'api_reference'], memory_key='chat_history', return_messages=True) set_debug(True) set_verbose(True) # code_chain = LLMChain(llm=llm, prompt=code_prompt, output_key='script', memory=code_memory) - + # # Compose the chain # config = RunnableConfig({"callbacks": [self.lunary_handler]}) # print(f"memory_initiates: {self.code_memory.load_memory_variables({})}") output = StrOutputParser() - + config = RunnableConfig({"callbacks": [self.lunary_handler]}) # print(f"config {config}") # code_memory.save_context({"task": new_task['task_description']}, {"output": code_response}) @@ -276,7 +276,7 @@ def on_llm_error(self, error: Exception, **kwargs): # "task": lambda x: x["task"], # "chat_history": self.safe_extract_history # } | code_prompt | llm | output - + # code_response = code_chain.run(method_signature=new_task['method_signature'], task=new_task['task_description']) try: @@ -303,10 +303,10 @@ def on_llm_error(self, error: Exception, **kwargs): # print(f"\n memory_contents: {memory_contents} \n") # print("Memory after saving:") # print(self.code_memory.load_memory_variables({})) - + # code_memory.save_context({"task": new_task['task_description']}, {"output": code_response}) # memory_contents = code_memory.load_memory_variables({}) - + # code_with_history = RunnableWithMessageHistory( # code_chain, # self.get_session_history, @@ -314,16 +314,16 @@ def on_llm_error(self, error: Exception, **kwargs): # history_messages_key="output", # ) # code_response = code_with_history.invoke({"method_signature": new_task['method_signature'], "task": new_task['task_description']}) - + # Set up logging # print(f"\n memory_contents: {memory_contents} \n") - + # with get_openai_callback() as cb_code: # set_verbose(True) # code_response = code_chain.invoke({"task": new_task['task_description']}, config= config) # conversation_history = code_memory.load_memory_variables({})["chat_history"] # code_memory.save_context({"task": new_task['task_description']}, {"output": code_response.content}) - + saved_map = { "temperature": temperature, "code_example_shots": fewshot_config["few_shot_examples_count"], diff --git a/src/components/prompt_generator.py b/src/components/prompt_generator.py index 5036f12..2dfb634 100644 --- a/src/components/prompt_generator.py +++ b/src/components/prompt_generator.py @@ -1,6 +1,6 @@ from langchain.output_parsers import ResponseSchema, StructuredOutputParser -from langchain.prompts.few_shot import FewShotPromptTemplate -from langchain.prompts.prompt import PromptTemplate +from langchain_core.prompts import FewShotPromptTemplate +from langchain_core.prompts import PromptTemplate class PromptGenerator: @@ -15,7 +15,7 @@ def create_few_shot_code_prompts(self, examples_task_ids, examples_db, prompt_te template=prompt_template ) print(f"example_prompt_template: \n {example_prompt_template}") - + prompt = FewShotPromptTemplate( prefix= f"SYSTEM:\nYou are an expert code assistant tasked with implementing Dafny code for filesystem operations. Your implementation should adhere to the following guidelines:\n- Must utilize given Safe APIs for file operations.\n- Generate Dafny code with appropriate preconditions to satisfy safe API preconditions.\n- Ensure that the code satisfies given safety properties for filesystem operations.\n- You are only limited to the provided method signatures and preconditions.\n\nAPI Reference:\n" + api_reference + "\n\n", examples=examples, @@ -46,7 +46,7 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # new_obj['verification_conditions'] = obj['spec']['verification_conditions'] # new_obj['verification_methods_signature'] = obj['spec']['verification_methods_signature'] # new_obj['fileIO_methods_signature'] = obj['fileIO_methods_signature'] - + similar_examples.append(new_obj) # print(f"simmilar_examples: {similar_examples}") return similar_examples @@ -95,7 +95,7 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # new_obj['fileIO_methods_signature'] = obj['fileIO_methods_signature'] # # new_obj['verification_method_description'] = obj['spec']['verification_method_description'] # similar_examples.append(new_obj) - + # return similar_examples @@ -128,15 +128,15 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # safety_properties_and_methods = self.format_safety_properties_and_methods(sp_json_data) # safety_properties_and_verifications = self.format_safety_properties_and_verifications(sp_json_data) # safety_property_explanations = self.create_safety_property_explanations(sp_json_data) - + # return safety_properties_and_methods, safety_properties_and_verifications,safety_property_explanations - + # # Define a function to format each example using the provided template # class PromptGenerator: # def __init__(self) -> None: # pass - + # def format_example(example, template): # return template.format( # task_description=example["task_description"], @@ -145,25 +145,25 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # postconditions=example["postconditions"], # code=example["code"] # ) - - + + # def create_few_shot_code_prompts(self, examples_task_ids, examples_db, prompt_template): # # Fetch similar tasks based on specifications # examples = self.get_similar_tasks_based_on_specs(examples_task_ids, examples_db) - - + + # # Format each example using the prompt template # formatted_examples = [self.format_example(ex, prompt_template) for ex in examples] - + # # Define the prefix and suffix # prefix = ("SYSTEM:\nYou are an expert AI assistant that writes Dafny programs. You are very good at writing " # "verifiable correct code in terms of preconditions and postconditions of methods, and at finding the " # "appropriate loop invariants for the pre/postconditions to hold.\n\n") - + # example_separator = "\n------------------------------------------------------\n" - + # suffix = "TASK:\n{{task}}\n\nAI ASSISTANT:\n\n" # # Combine prefix, formatted examples, and suffix to create the final prompt @@ -197,10 +197,10 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # def create_few_shot_specification_prompts(self, examples_task_ids, examples_db, prompt_template): # # Fetch similar tasks based on task descriptions # examples = self.get_similar_tasks_based_on_task_description(examples_task_ids, examples_db) - + # # Format each example using the prompt template # formatted_examples = [self.format_spec_example(ex, prompt_template) for ex in examples] - + # # Define the suffix # # suffix = "Task:\n{{task}}\n" @@ -209,7 +209,7 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # # Combine formatted examples and suffix to create the final prompt # combined_examples = example_separator.join(formatted_examples) # print(f"combined_examples: {combined_examples}") - + # # Append suffix only once at the end # final_prompt_template = combined_examples + example_separator @@ -235,15 +235,15 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # {"name": "postconditions", "description": "Postconditions"} # ] # parsed_output = {} - + # for schema in response_schemas: # field_name = schema["name"] # field_description = schema["description"] - + # # Simple heuristic-based parsing # start_marker = f"{field_description}:" # start_index = response_text.find(start_marker) - + # if start_index != -1: # start_index += len(start_marker) # end_index = response_text.find("\n", start_index) @@ -252,5 +252,5 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # parsed_output[field_name] = response_text[start_index:end_index].strip() # else: # parsed_output[field_name] = None - + # return parsed_output diff --git a/src/components/task_generator.py b/src/components/task_generator.py new file mode 100644 index 0000000..b03daa8 --- /dev/null +++ b/src/components/task_generator.py @@ -0,0 +1,99 @@ +import json +import openai +import os +import sys + +def load_config(config_path): + """ + Load configuration from a JSON file. + """ + try: + with open(config_path, 'r') as f: + config = json.load(f) + required_keys = ['model_name', 'api_key'] + for key in required_keys: + if key not in config: + raise KeyError(f"Missing '{key}' in configuration file.") + return config + except FileNotFoundError: + print(f"Configuration file '{config_path}' not found.") + sys.exit(1) + except json.JSONDecodeError: + print(f"Configuration file '{config_path}' is not valid JSON.") + sys.exit(1) + except KeyError as e: + print(e) + sys.exit(1) + +def load_template(template_path): + """ + Load task template from a text file. + """ + try: + with open(template_path, 'r') as f: + template = f.read() + return template + except FileNotFoundError: + print(f"Template file '{template_path}' not found.") + sys.exit(1) + +def generate_code(config, task_description): + """ + Send the task description to the LLM API and retrieve the generated code. + """ + openai.api_key = config['api_key'] + + try: + response = openai.ChatCompletion.create( + model=config['model_name'], + messages=[ + {"role": "system", "content": "You are an expert Python developer."}, + {"role": "user", "content": task_description} + ], + temperature=0, # Set to 0 for more deterministic output + max_tokens=1500, # Adjust based on expected code length + n=1, + stop=None + ) + code = response['choices'][0]['message']['content'].strip() + return code + except openai.error.OpenAIError as e: + print(f"An error occurred while communicating with the OpenAI API: {e}") + sys.exit(1) + +def save_code(code, output_path): + """ + Save the generated code to a file. + """ + try: + with open(output_path, 'w') as f: + f.write(code) + print(f"Generated code saved to '{output_path}'.") + except IOError as e: + print(f"Failed to write code to '{output_path}': {e}") + sys.exit(1) + +def main(): + # Define paths + config_path = 'config.json' + template_path = 'task_template.txt' + output_path = 'generated_code.py' + + # Load configuration and template + config = load_config(config_path) + task_description = load_template(template_path) + + # Generate code using the LLM + print("Generating code, please wait...") + code = generate_code(config, task_description) + + # Optional: Print the generated code + print("\n=== Generated Code ===\n") + print(code) + print("\n======================\n") + + # Save the generated code to a file + save_code(code, output_path) + +if __name__ == "__main__": + main() diff --git a/src/components/task_selector.py b/src/components/task_selector.py index 69437e4..9c3234d 100644 --- a/src/components/task_selector.py +++ b/src/components/task_selector.py @@ -1,5 +1,5 @@ -from langchain.prompts import MaxMarginalRelevanceExampleSelector -from langchain.prompts.example_selector import SemanticSimilarityExampleSelector +from langchain_core.example_selectors import MaxMarginalRelevanceExampleSelector +from langchain_core.example_selectors import SemanticSimilarityExampleSelector from langchain_community.vectorstores import FAISS from langchain_openai import OpenAIEmbeddings @@ -80,16 +80,16 @@ def get_max_marginal_relevance_based_example_selector(api_key, example_db_tasks, # # Get embeddings for all tasks # task_embeddings = get_embeddings(api_key, example_db_tasks) # index = build_faiss_index(task_embeddings) - + # # Get embedding for the target task description # target_embedding_response = client.embeddings.create(model="text-embedding-ada-002", input=target_task['task_description']) # target_embedding = target_embedding_response.data[0].embedding - + # if random.choice([True, False]): # # Find similar tasks with cosine similarity # similar_tasks = find_similar_tasks_cosine(task_embeddings, target_embedding, example_db_tasks, number_of_similar_tasks) # else: # # Find similar tasks with querying the Index # similar_tasks = find_similar_tasks(index, target_embedding, example_db_tasks, number_of_similar_tasks) - + # return {target_task['task_id']: similar_tasks} \ No newline at end of file diff --git a/src/prompts_template/COT_TEMPLATE.file b/src/prompts_template/COT_TEMPLATE.file index b6971eb..8c7db65 100644 --- a/src/prompts_template/COT_TEMPLATE.file +++ b/src/prompts_template/COT_TEMPLATE.file @@ -13,6 +13,8 @@ Step 1: Analyze and select the required APIs and their preconditions from the li For this task: {{api_with_preconditions}} + + Step 2: Implement the Dafny code for the described task, adhering to the provided structure for each API. Utilize the provided API list and their specifications. Provide the implementation in Dafny syntax as follows: @@ -20,4 +22,4 @@ Provide the implementation in Dafny syntax as follows: {{code}} -``` +``` \ No newline at end of file diff --git a/src/prompts_template/COT_template.txt b/src/prompts_template/COT_template.txt new file mode 100644 index 0000000..8b3d578 --- /dev/null +++ b/src/prompts_template/COT_template.txt @@ -0,0 +1,21 @@ +# Task Description +{task_description} + +## Method Signature +{method_signature} + +## AI Assistant Instructions + +Follow these steps to complete the task: + +1. **Analyze and select required APIs:** + Review the following API reference and their preconditions: + {api_with_preconditions} + +2. **Implement the Dafny code:** + Create the Dafny implementation for the described task, adhering to the provided structure for each API. Utilize the provided API list and their specifications. + + Provide your implementation in Dafny syntax as follows: + + ```dafny + {code} \ No newline at end of file diff --git a/src/prompts_template/COT_template_string.file b/src/prompts_template/COT_template_string.file new file mode 100644 index 0000000..9bdfd82 --- /dev/null +++ b/src/prompts_template/COT_template_string.file @@ -0,0 +1,23 @@ +Task Description: +{task_description} + +Method Signature: +{method_signature} + + +AI ASSISTANT: +Follow these steps to complete the task: + + +Step 1: Analyze and select the required APIs and their preconditions from the list of API reference. +For this task: +{api_with_preconditions} + +Step 2: Implement the Dafny code for the described task, adhering to the provided structure for each API. Utilize the provided API list and their specifications. +Provide the implementation in Dafny syntax as follows: + +```dafny + +{code} + +``` diff --git a/src/prompts_template/task_template.md b/src/prompts_template/task_template.md new file mode 100644 index 0000000..d0fd2e6 --- /dev/null +++ b/src/prompts_template/task_template.md @@ -0,0 +1,11 @@ +# Coding Task + +You are an expert Python developer. Below is the task description: + +--- + +{{ task_description }} + +--- + +Please provide the Python code that accomplishes the above task. Include appropriate function names, documentation, and ensure the code is well-structured and follows best practices. diff --git a/src/tasks/task-7.json b/src/tasks/task-7.json index b8f53a0..646e5fb 100644 --- a/src/tasks/task-7.json +++ b/src/tasks/task-7.json @@ -1,11 +1,9 @@ { - "6": { - "task_id": "6", - "task_description": "Your task is to implement a function which takes the filename as a parameter, which will then be used to create a full file path in a predetermined directory ( e.g.,'/home/user/documents').", - "method_signature": "method CreateFullPath(filename: seq)", + "7": { + "task_id": "7", + "task_description": "Your task is to implement a function which takes the filename as a parameter, which will then be used to create a full path in a predetermined directory ( e.g.,'/var/www/files/'), then reads from the file exists in the full path and returns data.", + "method_signature": "method GetFile(filename: seq) returns (data: array)", "all_api_with_preconditions": "- static method{:axiom} Open(name: seq) returns(ok:bool, f:FileStream)\n requires non_empty_string(name)\n requires !has_dangerous_pattern(name)\n requires has_absoloute_path(name)\n requires is_valid_path_name(name)\n ensures ok ==> fresh(f) && f.IsOpen() && f.Name() == name[..]\n\n- method{:axiom} Read(p: path, fileOffset:nat32, buffer:array, start:int32, end:int32) returns(ok:bool)\n requires non_empty_string(p)\n requires !has_dangerous_pattern(p)\n requires has_valid_path_length(p)\n requires has_absoloute_path(p)\n requires is_valid_file_extension(p)\n requires has_valid_content_length(buffer)\n requires is_valid_file_extension(p)\n requires is_valid_file_extension(p)\n requires IsOpen()\n requires 0 <= start as int <= end as int <= buffer.Length\n modifies buffer\n modifies this\n ensures Name() == old(Name())\n ensures ok ==> IsOpen()\n\n- method{:axiom} Write(p: path, fileOffset:nat32, buffer:array, start:int32, end:int32) returns(ok:bool)\n requires has_valid_path_length(p)\n requires has_absoloute_path(p)\n requires is_valid_path_name(p)\n requires has_valid_content_length(buffer)\n requires is_valid_file_extension(p)\n requires 0 <= start as int32 <= end as int32\n requires IsOpen()\n modifies this\n ensures Name() == old(Name())\n ensures ok ==> IsOpen() \n\n - method Join(p: path, f: file) returns(result: path)\n requires non_empty_string(f)\n requires non_empty_string(p)\n requires !has_dangerous_pattern(f)\n requires has_absoloute_path(f)\n requires is_valid_file_name(f)\n requires is_valid_path_name(p)\n requires has_valid_file_length(f)\n requires has_valid_path_length(p)\n requires has_valid_path_length(p+f)" } } - - diff --git a/src/utils/config_reader.py b/src/utils/config_reader.py index c825d9e..6077965 100644 --- a/src/utils/config_reader.py +++ b/src/utils/config_reader.py @@ -56,6 +56,8 @@ def get_config_values(section, keys): # Read Environment Variables env_keys = ['task_path', 'base_output_path', 'interface_path'] env_config = get_config_values('ENVIRONMENT', env_keys) + + #TODO: Check if all the paths are absolute paths # Read Few-Shot Prompting Config fewshot_keys = ['RAG_json_path', 'api_reference_path', 'few_shot_examples_count'] From a379138b4d2367c4a1e596f467fcec002faa3545 Mon Sep 17 00:00:00 2001 From: Parniaan Date: Tue, 24 Sep 2024 13:07:46 -0700 Subject: [PATCH 2/2] Prepare Benchmarks --- .../CWE-22/path-traversal-wtih-open.dfy | 34 +++++++ dataset/cwe-dafny/methods.txt | 3 + .../task_id_1_with_expect.dfy | 2 +- ...h-traversal-with-open.py => cwe22-safe.py} | 0 dataset/cwe-python/CWE-22/cwe22-unsafe.dfy | 0 dataset/cwe-python/CWE-22/cwe22-unsafe.py | 0 dataset/cwe-python/CWE-378/cwe-378.py | 3 +- .../CWE-59/{ => scenario1}/cwe-59.py | 0 .../CWE-59/scenario2/cwe59-unsafe.py | 0 .../CWE-59/scenario2/task-description.txt | 5 + dataset/test/passwd.txt | 1 + .../interface/effectful-interface.dfy | 2 - ..._6-gpt-4-temp_0.0-k_1_verification_log.txt | 2 - .../task_id_6-gpt-4-temp_0.75-k_1.dfy | 11 --- .../task_id_6-gpt-4-temp_0.75-k_1.dfy} | 3 +- ...6-gpt-4-temp_0.75-k_1_verification_log.txt | 0 .../task_id_7-gpt-4-temp_0.75-k_1.dfy | 17 ++++ ...7-gpt-4-temp_0.75-k_1_verification_log.txt | 11 +++ .../task_id_7-gpt-4-temp_0.75-k_2.dfy | 20 ++++ ...7-gpt-4-temp_0.75-k_2_verification_log.txt | 11 +++ .../task_id_7-gpt-4-temp_0.75-k_3.dfy | 18 ++++ ...7-gpt-4-temp_0.75-k_3_verification_log.txt | 42 ++++++++ .../task_id_7-gpt-4-temp_0.75-k_4.dfy | 18 ++++ ...7-gpt-4-temp_0.75-k_4_verification_log.txt | 42 ++++++++ .../task_id_7-gpt-4-temp_0.75-k_5.dfy | 18 ++++ ...7-gpt-4-temp_0.75-k_5_verification_log.txt | 42 ++++++++ requirements.txt | 34 +++++-- src/components/core.py | 68 ++++++------- src/components/prompt_generator.py | 44 ++++----- src/components/task_generator.py | 99 +++++++++++++++++++ src/components/task_selector.py | 10 +- src/prompts_template/COT_TEMPLATE.file | 4 +- src/prompts_template/COT_template.txt | 21 ++++ src/prompts_template/COT_template_string.file | 23 +++++ src/prompts_template/task_template.md | 11 +++ src/tasks/task-7.json | 10 +- src/utils/config_reader.py | 2 + 37 files changed, 538 insertions(+), 93 deletions(-) create mode 100644 dataset/cwe-dafny/CWE-22/path-traversal-wtih-open.dfy create mode 100644 dataset/cwe-dafny/methods.txt rename dataset/{cwe-python => cwe-dafny}/task_id_1_with_expect.dfy (92%) rename dataset/cwe-python/CWE-22/{path-traversal-with-open.py => cwe22-safe.py} (100%) create mode 100644 dataset/cwe-python/CWE-22/cwe22-unsafe.dfy create mode 100644 dataset/cwe-python/CWE-22/cwe22-unsafe.py rename dataset/cwe-python/CWE-59/{ => scenario1}/cwe-59.py (100%) create mode 100644 dataset/cwe-python/CWE-59/scenario2/cwe59-unsafe.py create mode 100644 dataset/cwe-python/CWE-59/scenario2/task-description.txt create mode 100644 dataset/test/passwd.txt delete mode 100644 output/task_id_6/task_id_6-gpt-4-temp_0.0-k_1_verification_log.txt delete mode 100644 output/task_id_6/task_id_6-gpt-4-temp_0.75-k_1.dfy rename output/{task_id_6/task_id_6-gpt-4-temp_0.0-k_1.dfy => task_id_6_generated@2024-09-18-01-14/task_id_6-gpt-4-temp_0.75-k_1.dfy} (71%) rename output/{task_id_6 => task_id_6_generated@2024-09-18-01-14}/task_id_6-gpt-4-temp_0.75-k_1_verification_log.txt (100%) create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1.dfy create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1_verification_log.txt create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2.dfy create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2_verification_log.txt create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3_verification_log.txt create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4_verification_log.txt create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy create mode 100644 output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5_verification_log.txt create mode 100644 src/components/task_generator.py create mode 100644 src/prompts_template/COT_template.txt create mode 100644 src/prompts_template/COT_template_string.file create mode 100644 src/prompts_template/task_template.md diff --git a/dataset/cwe-dafny/CWE-22/path-traversal-wtih-open.dfy b/dataset/cwe-dafny/CWE-22/path-traversal-wtih-open.dfy new file mode 100644 index 0000000..11dc2d6 --- /dev/null +++ b/dataset/cwe-dafny/CWE-22/path-traversal-wtih-open.dfy @@ -0,0 +1,34 @@ +include "../../../filesystems-api/interface/effectful-interface.dfy" +method GetFile(filename: seq) returns (data: array) +// requires non_empty_string(filename) +// requires !has_dangerous_pattern(filename) +// requires is_valid_file_name(filename) +// requires has_valid_file_length(filename) +// requires is_valid_file_extension(filename) +{ + + var f: FileStream; + var ok: bool; + var base_dir: seq := "/var/www/files/"; + data := new byte[100]; + var file_path := Join(base_dir, filename); + // if (!has_dangerous_pattern(file_path)) { + print "base_dir is safe"; + ok, f := FileStream.Open(file_path); + + // if !ok { print "open failed"; return data; } + // // if is_valid_file_extension(file_path) { + // print "file extension is valid"; + // ok := f.Read(file_path, 0, data, 0, data.Length as int32); + // print "Read operation terminated safely"; + // } else { + // print "file extension is invalid"; + // return data; + // } + + // } else { + // print "base_dir is unsafe"; + // return data; + // } + +} \ No newline at end of file diff --git a/dataset/cwe-dafny/methods.txt b/dataset/cwe-dafny/methods.txt new file mode 100644 index 0000000..8d9ba13 --- /dev/null +++ b/dataset/cwe-dafny/methods.txt @@ -0,0 +1,3 @@ +1. add preconditions to JoinFileToPath +2. use if (...) checks to guard the function call to FileStream.Open +3. use expect (...) checks to add runtime checks that the preconditions hold \ No newline at end of file diff --git a/dataset/cwe-python/task_id_1_with_expect.dfy b/dataset/cwe-dafny/task_id_1_with_expect.dfy similarity index 92% rename from dataset/cwe-python/task_id_1_with_expect.dfy rename to dataset/cwe-dafny/task_id_1_with_expect.dfy index 5833954..8fd1fd8 100644 --- a/dataset/cwe-python/task_id_1_with_expect.dfy +++ b/dataset/cwe-dafny/task_id_1_with_expect.dfy @@ -1,4 +1,4 @@ -include "/Users/pari/pcc-llms/dataset/filesystems/interface/effectful-interface.dfy" +include "../../filesystems-api/interface/effectful-interface.dfy" method JoinFileToPath(path: seq, fname: seq) returns (jointPath: path) diff --git a/dataset/cwe-python/CWE-22/path-traversal-with-open.py b/dataset/cwe-python/CWE-22/cwe22-safe.py similarity index 100% rename from dataset/cwe-python/CWE-22/path-traversal-with-open.py rename to dataset/cwe-python/CWE-22/cwe22-safe.py diff --git a/dataset/cwe-python/CWE-22/cwe22-unsafe.dfy b/dataset/cwe-python/CWE-22/cwe22-unsafe.dfy new file mode 100644 index 0000000..e69de29 diff --git a/dataset/cwe-python/CWE-22/cwe22-unsafe.py b/dataset/cwe-python/CWE-22/cwe22-unsafe.py new file mode 100644 index 0000000..e69de29 diff --git a/dataset/cwe-python/CWE-378/cwe-378.py b/dataset/cwe-python/CWE-378/cwe-378.py index b5f2bbe..8761fa8 100644 --- a/dataset/cwe-python/CWE-378/cwe-378.py +++ b/dataset/cwe-python/CWE-378/cwe-378.py @@ -4,7 +4,7 @@ def process_sensitive_data(data): # Create a temporary file with default permissions - temp_file = tempfile.NamedTemporaryFile(mode='w+t', delete=False) + temp_file = tempfile.NamedTemporaryFile(mode='w+t', delete=False) # Add a temp txt file temp_file.write(data) temp_file.close() @@ -21,6 +21,7 @@ def process_sensitive_data(data): sensitive_info = "password123" result = process_sensitive_data(sensitive_info) +#TODO separate the safe code from the unsafe code and task description and add safe dafny version and a code completion sample in Dafny # A program that creates a temporary file to store sensitive data # The temporary file is created with default permissions, which might be # too permissive and allow other users on the system to read the sensitive data diff --git a/dataset/cwe-python/CWE-59/cwe-59.py b/dataset/cwe-python/CWE-59/scenario1/cwe-59.py similarity index 100% rename from dataset/cwe-python/CWE-59/cwe-59.py rename to dataset/cwe-python/CWE-59/scenario1/cwe-59.py diff --git a/dataset/cwe-python/CWE-59/scenario2/cwe59-unsafe.py b/dataset/cwe-python/CWE-59/scenario2/cwe59-unsafe.py new file mode 100644 index 0000000..e69de29 diff --git a/dataset/cwe-python/CWE-59/scenario2/task-description.txt b/dataset/cwe-python/CWE-59/scenario2/task-description.txt new file mode 100644 index 0000000..f2e4366 --- /dev/null +++ b/dataset/cwe-python/CWE-59/scenario2/task-description.txt @@ -0,0 +1,5 @@ +File retrieval and file upload for a username + +1. Take a username as input +2. Construct a path to a file named "user_data.txt" in the user's home directory +3. If the file exists, read and return its contents \ No newline at end of file diff --git a/dataset/test/passwd.txt b/dataset/test/passwd.txt new file mode 100644 index 0000000..d5205a0 --- /dev/null +++ b/dataset/test/passwd.txt @@ -0,0 +1 @@ +uehfyJHD$73@0!j.Lz \ No newline at end of file diff --git a/filesystems-api/interface/effectful-interface.dfy b/filesystems-api/interface/effectful-interface.dfy index df6d9ef..b4215a8 100644 --- a/filesystems-api/interface/effectful-interface.dfy +++ b/filesystems-api/interface/effectful-interface.dfy @@ -119,8 +119,6 @@ class FileStream requires has_absoloute_path(p) requires is_valid_file_extension(p) requires has_valid_content_length(buffer) - requires is_valid_file_extension(p) - requires is_valid_file_extension(p) requires IsOpen() requires 0 <= start as int <= end as int <= buffer.Length modifies buffer diff --git a/output/task_id_6/task_id_6-gpt-4-temp_0.0-k_1_verification_log.txt b/output/task_id_6/task_id_6-gpt-4-temp_0.0-k_1_verification_log.txt deleted file mode 100644 index 823a60a..0000000 --- a/output/task_id_6/task_id_6-gpt-4-temp_0.0-k_1_verification_log.txt +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 1 verified, 0 errors diff --git a/output/task_id_6/task_id_6-gpt-4-temp_0.75-k_1.dfy b/output/task_id_6/task_id_6-gpt-4-temp_0.75-k_1.dfy deleted file mode 100644 index 0b995fe..0000000 --- a/output/task_id_6/task_id_6-gpt-4-temp_0.75-k_1.dfy +++ /dev/null @@ -1,11 +0,0 @@ -include "/Users/pari/pcc-llms/dataset/filesystems/interface/effectful-interface.dfy" - -method CreateFullPath(filename: seq) returns (fullPath: seq) - requires non_empty_string(filename) - requires !has_dangerous_pattern(filename) - requires is_valid_file_name(filename) - requires has_valid_file_length(filename) - { - var dir: seq := "/home/user/documents"; // The predetermined directory - fullPath := Join(dir, filename); - } \ No newline at end of file diff --git a/output/task_id_6/task_id_6-gpt-4-temp_0.0-k_1.dfy b/output/task_id_6_generated@2024-09-18-01-14/task_id_6-gpt-4-temp_0.75-k_1.dfy similarity index 71% rename from output/task_id_6/task_id_6-gpt-4-temp_0.0-k_1.dfy rename to output/task_id_6_generated@2024-09-18-01-14/task_id_6-gpt-4-temp_0.75-k_1.dfy index 6197130..a6d328b 100644 --- a/output/task_id_6/task_id_6-gpt-4-temp_0.0-k_1.dfy +++ b/output/task_id_6_generated@2024-09-18-01-14/task_id_6-gpt-4-temp_0.75-k_1.dfy @@ -1,6 +1,7 @@ -include "/Users/pari/pcc-llms/dataset/filesystems/interface/effectful-interface.dfy" +include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy" method CreateFullPath(filename: seq) returns (fullPath: seq) + requires non_empty_string(filename) requires !has_dangerous_pattern(filename) requires is_valid_file_name(filename) requires has_valid_file_length(filename) diff --git a/output/task_id_6/task_id_6-gpt-4-temp_0.75-k_1_verification_log.txt b/output/task_id_6_generated@2024-09-18-01-14/task_id_6-gpt-4-temp_0.75-k_1_verification_log.txt similarity index 100% rename from output/task_id_6/task_id_6-gpt-4-temp_0.75-k_1_verification_log.txt rename to output/task_id_6_generated@2024-09-18-01-14/task_id_6-gpt-4-temp_0.75-k_1_verification_log.txt diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1.dfy b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1.dfy new file mode 100644 index 0000000..fd3be72 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1.dfy @@ -0,0 +1,17 @@ +include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy" + +method GetFile(filename: seq) returns (data: array) + requires non_empty_string(filename) + requires !has_dangerous_pattern(filename) + requires is_valid_file_name(filename) + requires has_valid_file_length(filename) + { + var directory: seq := "/var/www/files/"; + var f: FileStream; + var fullpath := Join(directory, filename); + var ok: bool; + ok, f := Open(fullpath); + if !ok { print "open failed"; return new byte[0]; } + data := new byte[100]; + ok := f.Read(fullpath, 0, data, 0, data.Length as int32); + } \ No newline at end of file diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1_verification_log.txt b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1_verification_log.txt new file mode 100644 index 0000000..27aa516 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1_verification_log.txt @@ -0,0 +1,11 @@ +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1.dfy(13,14): Error: unresolved identifier: Open + | +13 | ok, f := Open(fullpath); + | ^^^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1.dfy(13,11): Error: the number of left-hand sides (2) and right-hand sides (1) must match for a multi-assignment + | +13 | ok, f := Open(fullpath); + | ^^ + +2 resolution/type errors detected in task_id_7-gpt-4-temp_0.75-k_1.dfy diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2.dfy b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2.dfy new file mode 100644 index 0000000..1500497 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2.dfy @@ -0,0 +1,20 @@ +include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy" + +method GetFile(filename: seq) returns (data: array) + requires !has_dangerous_pattern(filename) + requires is_valid_file_extension(filename) + requires is_valid_file_name(filename) + requires has_valid_file_length(filename) + requires has_absoloute_path(filename) + requires non_empty_string(filename) + { + var f: FileStream; + var ok: bool; + var path: array := "/var/www/files/"; + var fullPath := Join(path, filename); + ok, f := FileStream.Open(fullPath); + if !ok { print "open failed"; return new byte[0]; } + data := new byte[100]; + ok := f.Read(fullPath, 0, data, 0, data.Length as int32); + print "File read completed!\n"; + } \ No newline at end of file diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2_verification_log.txt b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2_verification_log.txt new file mode 100644 index 0000000..e483698 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2_verification_log.txt @@ -0,0 +1,11 @@ +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2.dfy(13,27): Error: RHS (of type string) not assignable to LHS (of type array) + | +13 | var path: array := "/var/www/files/"; + | ^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2.dfy(14,21): Error: incorrect argument type at index 0 for method in-parameter 'p' (expected path, found array) + | +14 | var fullPath := Join(path, filename); + | ^^^^^^^^^^^^^^^^^^^^ + +2 resolution/type errors detected in task_id_7-gpt-4-temp_0.75-k_2.dfy diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy new file mode 100644 index 0000000..a61e3c3 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy @@ -0,0 +1,18 @@ +include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy" + +method GetFile(filename: seq) returns (data: array) + requires !has_dangerous_pattern(filename) + requires is_valid_file_name(filename) + requires non_empty_string(filename) + requires has_valid_file_length(filename) + { + var folderPath: seq := "/var/www/files/"; + var fullPath: seq := Join(folderPath, filename); + var f: FileStream; + var ok: bool; + ok, f := FileStream.Open(fullPath); + if !ok { print "open failed\n"; return new byte[0]; } + data := new byte[100]; + ok := f.Read(fullPath, 0, data, 0, data.Length as int32); + print "File data loaded!\n"; + } \ No newline at end of file diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3_verification_log.txt b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3_verification_log.txt new file mode 100644 index 0000000..f2d23be --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3_verification_log.txt @@ -0,0 +1,42 @@ +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy(13,4): Error: a precondition for this call could not be proved + | +13 | ok, f := FileStream.Open(fullPath); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(104,13): Related location: this is the precondition that could not be proved + | +104 | requires !has_dangerous_pattern(name) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy(16,4): Error: a precondition for this call could not be proved + | +16 | ok := f.Read(fullPath, 0, data, 0, data.Length as int32); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved + | +120 | requires is_valid_file_extension(p) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(211,4): Related location: this proposition could not be proved + | +211 | lastDotIndex >= 0 && + | ^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy(16,4): Error: a precondition for this call could not be proved + | +16 | ok := f.Read(fullPath, 0, data, 0, data.Length as int32); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved + | +120 | requires is_valid_file_extension(p) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(212,4): Related location: this proposition could not be proved + | +212 | lastDotIndex < |filename| - 1 && + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + + +Dafny program verifier finished with 0 verified, 3 errors diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy new file mode 100644 index 0000000..6e17a76 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy @@ -0,0 +1,18 @@ +include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy" + +method GetFile(filename: seq) returns (data: array) + requires !has_dangerous_pattern(filename) + requires is_valid_file_name(filename) + requires non_empty_string(filename) + requires has_valid_file_length(filename) + { + var f: FileStream; + var ok: bool; + var dir: path := "/var/www/files/"; + var fullpath: path := Join(dir, filename); + ok, f := FileStream.Open(fullpath); + if !ok { print "open failed\n"; return new byte[0]; } + data := new byte[100]; + ok := f.Read(fullpath, 0, data, 0, data.Length as int32); + print "File data loaded!\n"; + } \ No newline at end of file diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4_verification_log.txt b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4_verification_log.txt new file mode 100644 index 0000000..4858da3 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4_verification_log.txt @@ -0,0 +1,42 @@ +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy(13,3): Error: a precondition for this call could not be proved + | +13 | ok, f := FileStream.Open(fullpath); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(104,13): Related location: this is the precondition that could not be proved + | +104 | requires !has_dangerous_pattern(name) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy(16,3): Error: a precondition for this call could not be proved + | +16 | ok := f.Read(fullpath, 0, data, 0, data.Length as int32); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved + | +120 | requires is_valid_file_extension(p) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(211,4): Related location: this proposition could not be proved + | +211 | lastDotIndex >= 0 && + | ^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy(16,3): Error: a precondition for this call could not be proved + | +16 | ok := f.Read(fullpath, 0, data, 0, data.Length as int32); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved + | +120 | requires is_valid_file_extension(p) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(212,4): Related location: this proposition could not be proved + | +212 | lastDotIndex < |filename| - 1 && + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + + +Dafny program verifier finished with 0 verified, 3 errors diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy new file mode 100644 index 0000000..e836ca8 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy @@ -0,0 +1,18 @@ +include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy" + +method GetFile(filename: seq) returns (data: array) + requires non_empty_string(filename) + requires !has_dangerous_pattern(filename) + requires is_valid_file_name(filename) + requires has_valid_file_length(filename) + { + var ok: bool; + var f: FileStream; + var directory: path := "/var/www/files/"; + var fullPath := Join(directory, filename); + ok, f := FileStream.Open(fullPath); + if !ok { print "open failed"; return new byte[0]; } + data := new byte[100]; + ok := f.Read(fullPath, 0, data, 0, data.Length as int32); + print "File data loaded!\n"; + } \ No newline at end of file diff --git a/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5_verification_log.txt b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5_verification_log.txt new file mode 100644 index 0000000..68872b5 --- /dev/null +++ b/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5_verification_log.txt @@ -0,0 +1,42 @@ +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy(13,5): Error: a precondition for this call could not be proved + | +13 | ok, f := FileStream.Open(fullPath); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(104,13): Related location: this is the precondition that could not be proved + | +104 | requires !has_dangerous_pattern(name) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy(16,5): Error: a precondition for this call could not be proved + | +16 | ok := f.Read(fullPath, 0, data, 0, data.Length as int32); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved + | +120 | requires is_valid_file_extension(p) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(211,4): Related location: this proposition could not be proved + | +211 | lastDotIndex >= 0 && + | ^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy(16,5): Error: a precondition for this call could not be proved + | +16 | ok := f.Read(fullPath, 0, data, 0, data.Length as int32); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved + | +120 | requires is_valid_file_extension(p) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(212,4): Related location: this proposition could not be proved + | +212 | lastDotIndex < |filename| - 1 && + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + + +Dafny program verifier finished with 0 verified, 3 errors diff --git a/requirements.txt b/requirements.txt index 4414d8e..6035b44 100644 --- a/requirements.txt +++ b/requirements.txt @@ -12,6 +12,8 @@ bleach==6.1.0 certifi==2024.6.2 charset-normalizer==3.3.2 chevron==0.14.0 +click==8.1.7 +colorama==0.4.6 dataclasses-json==0.6.7 decorator==5.1.1 defusedxml==0.7.1 @@ -19,10 +21,14 @@ distro==1.9.0 docopt==0.6.2 executing==2.0.1 faiss-cpu==1.8.0 +fastapi==0.115.0 fastjsonschema==2.20.0 filelock==3.15.4 frozenlist==1.4.1 fsspec==2024.6.1 +gitdb==4.0.11 +GitPython==3.1.43 +gritql==0.1.5 h11==0.14.0 httpcore==1.0.5 httpx==0.27.0 @@ -41,17 +47,22 @@ jsonschema-specifications==2023.12.1 jupyter_client==8.6.2 jupyter_core==5.7.2 jupyterlab_pygments==0.3.0 -langchain==0.2.7 +langchain==0.3.0 langchain-anthropic==0.1.23 -langchain-community==0.2.7 -langchain-core==0.2.39 +langchain-cli==0.0.31 +langchain-community==0.3.0 +langchain-core==0.3.5 +langchain-experimental==0.3.0 langchain-openai==0.1.14 -langchain-text-splitters==0.2.2 -langsmith==0.1.117 +langchain-text-splitters==0.3.0 +langserve==0.3.0 +langsmith==0.1.125 lunary==1.1.3 +markdown-it-py==3.0.0 MarkupSafe==2.1.5 marshmallow==3.21.3 matplotlib-inline==0.1.7 +mdurl==0.1.2 mistune==3.0.2 mpmath==1.3.0 multidict==6.0.5 @@ -74,8 +85,9 @@ platformdirs==4.2.2 prompt_toolkit==3.0.47 ptyprocess==0.7.0 pure-eval==0.2.2 -pydantic==2.7.3 -pydantic_core==2.18.4 +pydantic==2.9.2 +pydantic-settings==2.5.2 +pydantic_core==2.23.4 Pygments==2.18.0 pyhumps==3.8.0 python-dateutil==2.9.0.post0 @@ -85,31 +97,39 @@ pyzmq==26.0.3 referencing==0.35.1 regex==2024.5.15 requests==2.32.3 +rich==13.8.1 rpds-py==0.18.1 safetensors==0.4.3 scikit-learn==1.5.1 scipy==1.14.0 sentence-transformers==3.0.1 setuptools==67.8.0 +shellingham==1.5.4 six==1.16.0 +smmap==5.0.1 sniffio==1.3.1 soupsieve==2.5 SQLAlchemy==2.0.31 +sse-starlette==1.8.2 stack-data==0.6.3 +starlette==0.38.6 sympy==1.13.0 tenacity==8.5.0 threadpoolctl==3.5.0 tiktoken==0.7.0 tinycss2==1.3.0 tokenizers==0.19.1 +tomlkit==0.12.5 torch==2.3.1 tornado==6.4.1 tqdm==4.66.4 traitlets==5.14.3 transformers==4.42.3 +typer==0.9.4 typing-inspect==0.9.0 typing_extensions==4.12.1 urllib3==2.2.2 +uvicorn==0.23.2 wcwidth==0.2.13 webencodings==0.5.1 yarg==0.1.9 diff --git a/src/components/core.py b/src/components/core.py index a381542..bc56049 100644 --- a/src/components/core.py +++ b/src/components/core.py @@ -11,13 +11,13 @@ import json import logging -from langchain.callbacks.base import BaseCallbackHandler +from langchain_core.callbacks import BaseCallbackHandler # from langchain.errors import ChainError, LLMErrors from langchain.globals import set_debug, set_verbose from langchain.memory import ConversationBufferMemory -from langchain.prompts import PromptTemplate -from langchain.schema import SystemMessage +from langchain_core.prompts import PromptTemplate +from langchain_core.messages import SystemMessage from langchain_anthropic import ChatAnthropic from langchain_community.callbacks.manager import get_openai_callback from langchain_community.chat_message_histories import ChatMessageHistory @@ -47,7 +47,7 @@ class Core: "safety_property": None, "required_files": None, "generate_code_file": None, - + } def __init__(self, max_history_length=1000): @@ -64,12 +64,12 @@ def count_tokens(self, chain, query): # print(f'Spent a total of {cb.total_tokens} tokens') return result, cb.total_tokens - + def initialize_llm(self, model_config, api_config): model = model_config['model'] if api_config["lunary_api_key"] is not None: self.lunary_handler = LunaryCallbackHandler(app_id=api_config["lunary_api_key"]) - + if model == "gpt-4": return ChatOpenAI(model_name="gpt-4", temperature=model_config['temp'], openai_api_key=api_config['openai_api_key'], callbacks=[self.lunary_handler], verbose=True) @@ -79,15 +79,15 @@ def initialize_llm(self, model_config, api_config): if model == "claude": return ChatAnthropic(model="claude-3-opus-20240229", temperature=model_config['temp'], api_key=api_config['claude_api_key'], callbacks=[self.lunary_handler], verbose=True) - + # def get_session_history(self, session_id: str) -> BaseChatMessageHistory: # if session_id not in self.store: # self.store[session_id] = ChatMessageHistory() # return self.store[session_id] - - + + # def fix_code(self, api_config, code, error): - + # code_fix_template = """ # The following Python code has an error: @@ -113,7 +113,7 @@ def initialize_llm(self, model_config, api_config): # def safe_extract_history(self, x): # # Safely extract chat history, returning an empty list if not found # return x.get("chat_history", {}).get("chat_history", []) - + # def load_memory_debug(self, code_memory): # memory_data = code_memory.load_memory_variables({}) # print(f"Loaded memory data: {memory_data}") # Debug print @@ -122,12 +122,12 @@ def safe_extract_history(self, x): chat_history = x.get("chat_history", {}).get("chat_history", []) # print(f"Extracted chat history: {chat_history}") # Debug print return chat_history - + def add_error_to_memory(self, validation_result): error_feedback = f"Error occurred. Let's try again." self.code_memory.chat_memory.add_message(SystemMessage(content=validation_result)) return error_feedback - + def invoke_llm(self, api_config, model_config, fewshot_config, new_task, example_db_5_tasks, code_example_selector, @@ -158,7 +158,7 @@ def on_llm_error(self, error: Exception, **kwargs): logging.error(f"LLM error: {str(error)}", exc_info=True) - + # Required for similarity_example_selector without lanchain # spec_examples_ids = [] # for key, task_list in similar_tasks.items(): @@ -169,27 +169,27 @@ def on_llm_error(self, error: Exception, **kwargs): # print() # Add a blank line for better readability # spec_examples_ids.append(task['task_id']) # print(f"\n spec_examples_ids \n {spec_examples_ids}") - + # similar_tasks = spec_example_selector.select_examples(new_task) # print(f"\n vc_example_selector \n {vc_example_selector}") - + prompt_gen = prompt_generator.PromptGenerator() # specification_prompt = prompt_gen.create_few_shot_specification_prompts(spec_examples_ids, # example_db_5_tasks, # vc_prompt_template) - + # print("\n Is specification_prompt correct ??????????????//////////////////////") # print(specification_prompt) # Memory # specification_memory = ConversationBufferMemory(input_key='task', memory_key='chat_history') - + # specification_chain = LLMChain(llm=llm, prompt=specification_prompt, verbose=False, output_key='specifications', # memory=specification_memory) - - + + print("\n new_task_description \n", new_task['task_description']) # Debug: Print memory contents before running the chain @@ -201,7 +201,7 @@ def on_llm_error(self, error: Exception, **kwargs): # print(f'\n Spent a total of {cb_spec.total_tokens} tokens for verification \n') # print(f"\n specification_response: \n {specification_response} \n") # next_input_task_with_spec = utils.parse_specification_response(new_task, specification_response) - + # print(f"\n next_input_task_with_spec: \n {next_input_task_with_spec} \n") # spec_similar_code_tasks = code_example_selector.select_examples(next_input_task_with_spec) # print(f"\n spec_similar_code_tasks = \n {spec_similar_code_tasks} \n") @@ -222,7 +222,7 @@ def on_llm_error(self, error: Exception, **kwargs): # print(f"{code_prompt}") # print(f"\n ================================") # utils.write_to_file("/Users/pari/pcc-llms/output/code_prompt.txt", code_prompt) - + # print(f"\n base_output_path {env_config["base_output_path"]} \n") # prompt_path = os.path.join(env_config["base_output_path"], # "dynamic-few-shot-prompt-" + str(K) + ".txt") @@ -234,28 +234,28 @@ def on_llm_error(self, error: Exception, **kwargs): # print(f"Error: The file {prompt_path} does not exist.") # except IOError as e: # print(f"Error reading the file {prompt_path}: {str(e)}") - + # config = RunnableConfig({"callbacks": [handler]}) # ************************** langchain deprecated ************************** # code_memory = ConversationBufferMemory(input_key='task', memory_key='chat_history') # print (f"\n code_memory: {code_memory} \n") # code_chain = LLMChain(llm=llm, prompt=code_prompt, verbose=False, output_key='script', memory=self.code_memory) - - + + # ************************************************************************** # Create memory - + # code_memory = ConversationBufferMemory(input_key=['task', 'api_reference'], memory_key='chat_history', return_messages=True) set_debug(True) set_verbose(True) # code_chain = LLMChain(llm=llm, prompt=code_prompt, output_key='script', memory=code_memory) - + # # Compose the chain # config = RunnableConfig({"callbacks": [self.lunary_handler]}) # print(f"memory_initiates: {self.code_memory.load_memory_variables({})}") output = StrOutputParser() - + config = RunnableConfig({"callbacks": [self.lunary_handler]}) # print(f"config {config}") # code_memory.save_context({"task": new_task['task_description']}, {"output": code_response}) @@ -276,7 +276,7 @@ def on_llm_error(self, error: Exception, **kwargs): # "task": lambda x: x["task"], # "chat_history": self.safe_extract_history # } | code_prompt | llm | output - + # code_response = code_chain.run(method_signature=new_task['method_signature'], task=new_task['task_description']) try: @@ -303,10 +303,10 @@ def on_llm_error(self, error: Exception, **kwargs): # print(f"\n memory_contents: {memory_contents} \n") # print("Memory after saving:") # print(self.code_memory.load_memory_variables({})) - + # code_memory.save_context({"task": new_task['task_description']}, {"output": code_response}) # memory_contents = code_memory.load_memory_variables({}) - + # code_with_history = RunnableWithMessageHistory( # code_chain, # self.get_session_history, @@ -314,16 +314,16 @@ def on_llm_error(self, error: Exception, **kwargs): # history_messages_key="output", # ) # code_response = code_with_history.invoke({"method_signature": new_task['method_signature'], "task": new_task['task_description']}) - + # Set up logging # print(f"\n memory_contents: {memory_contents} \n") - + # with get_openai_callback() as cb_code: # set_verbose(True) # code_response = code_chain.invoke({"task": new_task['task_description']}, config= config) # conversation_history = code_memory.load_memory_variables({})["chat_history"] # code_memory.save_context({"task": new_task['task_description']}, {"output": code_response.content}) - + saved_map = { "temperature": temperature, "code_example_shots": fewshot_config["few_shot_examples_count"], diff --git a/src/components/prompt_generator.py b/src/components/prompt_generator.py index 5036f12..2dfb634 100644 --- a/src/components/prompt_generator.py +++ b/src/components/prompt_generator.py @@ -1,6 +1,6 @@ from langchain.output_parsers import ResponseSchema, StructuredOutputParser -from langchain.prompts.few_shot import FewShotPromptTemplate -from langchain.prompts.prompt import PromptTemplate +from langchain_core.prompts import FewShotPromptTemplate +from langchain_core.prompts import PromptTemplate class PromptGenerator: @@ -15,7 +15,7 @@ def create_few_shot_code_prompts(self, examples_task_ids, examples_db, prompt_te template=prompt_template ) print(f"example_prompt_template: \n {example_prompt_template}") - + prompt = FewShotPromptTemplate( prefix= f"SYSTEM:\nYou are an expert code assistant tasked with implementing Dafny code for filesystem operations. Your implementation should adhere to the following guidelines:\n- Must utilize given Safe APIs for file operations.\n- Generate Dafny code with appropriate preconditions to satisfy safe API preconditions.\n- Ensure that the code satisfies given safety properties for filesystem operations.\n- You are only limited to the provided method signatures and preconditions.\n\nAPI Reference:\n" + api_reference + "\n\n", examples=examples, @@ -46,7 +46,7 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # new_obj['verification_conditions'] = obj['spec']['verification_conditions'] # new_obj['verification_methods_signature'] = obj['spec']['verification_methods_signature'] # new_obj['fileIO_methods_signature'] = obj['fileIO_methods_signature'] - + similar_examples.append(new_obj) # print(f"simmilar_examples: {similar_examples}") return similar_examples @@ -95,7 +95,7 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # new_obj['fileIO_methods_signature'] = obj['fileIO_methods_signature'] # # new_obj['verification_method_description'] = obj['spec']['verification_method_description'] # similar_examples.append(new_obj) - + # return similar_examples @@ -128,15 +128,15 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # safety_properties_and_methods = self.format_safety_properties_and_methods(sp_json_data) # safety_properties_and_verifications = self.format_safety_properties_and_verifications(sp_json_data) # safety_property_explanations = self.create_safety_property_explanations(sp_json_data) - + # return safety_properties_and_methods, safety_properties_and_verifications,safety_property_explanations - + # # Define a function to format each example using the provided template # class PromptGenerator: # def __init__(self) -> None: # pass - + # def format_example(example, template): # return template.format( # task_description=example["task_description"], @@ -145,25 +145,25 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # postconditions=example["postconditions"], # code=example["code"] # ) - - + + # def create_few_shot_code_prompts(self, examples_task_ids, examples_db, prompt_template): # # Fetch similar tasks based on specifications # examples = self.get_similar_tasks_based_on_specs(examples_task_ids, examples_db) - - + + # # Format each example using the prompt template # formatted_examples = [self.format_example(ex, prompt_template) for ex in examples] - + # # Define the prefix and suffix # prefix = ("SYSTEM:\nYou are an expert AI assistant that writes Dafny programs. You are very good at writing " # "verifiable correct code in terms of preconditions and postconditions of methods, and at finding the " # "appropriate loop invariants for the pre/postconditions to hold.\n\n") - + # example_separator = "\n------------------------------------------------------\n" - + # suffix = "TASK:\n{{task}}\n\nAI ASSISTANT:\n\n" # # Combine prefix, formatted examples, and suffix to create the final prompt @@ -197,10 +197,10 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # def create_few_shot_specification_prompts(self, examples_task_ids, examples_db, prompt_template): # # Fetch similar tasks based on task descriptions # examples = self.get_similar_tasks_based_on_task_description(examples_task_ids, examples_db) - + # # Format each example using the prompt template # formatted_examples = [self.format_spec_example(ex, prompt_template) for ex in examples] - + # # Define the suffix # # suffix = "Task:\n{{task}}\n" @@ -209,7 +209,7 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # # Combine formatted examples and suffix to create the final prompt # combined_examples = example_separator.join(formatted_examples) # print(f"combined_examples: {combined_examples}") - + # # Append suffix only once at the end # final_prompt_template = combined_examples + example_separator @@ -235,15 +235,15 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # {"name": "postconditions", "description": "Postconditions"} # ] # parsed_output = {} - + # for schema in response_schemas: # field_name = schema["name"] # field_description = schema["description"] - + # # Simple heuristic-based parsing # start_marker = f"{field_description}:" # start_index = response_text.find(start_marker) - + # if start_index != -1: # start_index += len(start_marker) # end_index = response_text.find("\n", start_index) @@ -252,5 +252,5 @@ def get_similar_tasks_based_on_specs(self, ids, examples_db): # parsed_output[field_name] = response_text[start_index:end_index].strip() # else: # parsed_output[field_name] = None - + # return parsed_output diff --git a/src/components/task_generator.py b/src/components/task_generator.py new file mode 100644 index 0000000..b03daa8 --- /dev/null +++ b/src/components/task_generator.py @@ -0,0 +1,99 @@ +import json +import openai +import os +import sys + +def load_config(config_path): + """ + Load configuration from a JSON file. + """ + try: + with open(config_path, 'r') as f: + config = json.load(f) + required_keys = ['model_name', 'api_key'] + for key in required_keys: + if key not in config: + raise KeyError(f"Missing '{key}' in configuration file.") + return config + except FileNotFoundError: + print(f"Configuration file '{config_path}' not found.") + sys.exit(1) + except json.JSONDecodeError: + print(f"Configuration file '{config_path}' is not valid JSON.") + sys.exit(1) + except KeyError as e: + print(e) + sys.exit(1) + +def load_template(template_path): + """ + Load task template from a text file. + """ + try: + with open(template_path, 'r') as f: + template = f.read() + return template + except FileNotFoundError: + print(f"Template file '{template_path}' not found.") + sys.exit(1) + +def generate_code(config, task_description): + """ + Send the task description to the LLM API and retrieve the generated code. + """ + openai.api_key = config['api_key'] + + try: + response = openai.ChatCompletion.create( + model=config['model_name'], + messages=[ + {"role": "system", "content": "You are an expert Python developer."}, + {"role": "user", "content": task_description} + ], + temperature=0, # Set to 0 for more deterministic output + max_tokens=1500, # Adjust based on expected code length + n=1, + stop=None + ) + code = response['choices'][0]['message']['content'].strip() + return code + except openai.error.OpenAIError as e: + print(f"An error occurred while communicating with the OpenAI API: {e}") + sys.exit(1) + +def save_code(code, output_path): + """ + Save the generated code to a file. + """ + try: + with open(output_path, 'w') as f: + f.write(code) + print(f"Generated code saved to '{output_path}'.") + except IOError as e: + print(f"Failed to write code to '{output_path}': {e}") + sys.exit(1) + +def main(): + # Define paths + config_path = 'config.json' + template_path = 'task_template.txt' + output_path = 'generated_code.py' + + # Load configuration and template + config = load_config(config_path) + task_description = load_template(template_path) + + # Generate code using the LLM + print("Generating code, please wait...") + code = generate_code(config, task_description) + + # Optional: Print the generated code + print("\n=== Generated Code ===\n") + print(code) + print("\n======================\n") + + # Save the generated code to a file + save_code(code, output_path) + +if __name__ == "__main__": + main() diff --git a/src/components/task_selector.py b/src/components/task_selector.py index 69437e4..9c3234d 100644 --- a/src/components/task_selector.py +++ b/src/components/task_selector.py @@ -1,5 +1,5 @@ -from langchain.prompts import MaxMarginalRelevanceExampleSelector -from langchain.prompts.example_selector import SemanticSimilarityExampleSelector +from langchain_core.example_selectors import MaxMarginalRelevanceExampleSelector +from langchain_core.example_selectors import SemanticSimilarityExampleSelector from langchain_community.vectorstores import FAISS from langchain_openai import OpenAIEmbeddings @@ -80,16 +80,16 @@ def get_max_marginal_relevance_based_example_selector(api_key, example_db_tasks, # # Get embeddings for all tasks # task_embeddings = get_embeddings(api_key, example_db_tasks) # index = build_faiss_index(task_embeddings) - + # # Get embedding for the target task description # target_embedding_response = client.embeddings.create(model="text-embedding-ada-002", input=target_task['task_description']) # target_embedding = target_embedding_response.data[0].embedding - + # if random.choice([True, False]): # # Find similar tasks with cosine similarity # similar_tasks = find_similar_tasks_cosine(task_embeddings, target_embedding, example_db_tasks, number_of_similar_tasks) # else: # # Find similar tasks with querying the Index # similar_tasks = find_similar_tasks(index, target_embedding, example_db_tasks, number_of_similar_tasks) - + # return {target_task['task_id']: similar_tasks} \ No newline at end of file diff --git a/src/prompts_template/COT_TEMPLATE.file b/src/prompts_template/COT_TEMPLATE.file index b6971eb..8c7db65 100644 --- a/src/prompts_template/COT_TEMPLATE.file +++ b/src/prompts_template/COT_TEMPLATE.file @@ -13,6 +13,8 @@ Step 1: Analyze and select the required APIs and their preconditions from the li For this task: {{api_with_preconditions}} + + Step 2: Implement the Dafny code for the described task, adhering to the provided structure for each API. Utilize the provided API list and their specifications. Provide the implementation in Dafny syntax as follows: @@ -20,4 +22,4 @@ Provide the implementation in Dafny syntax as follows: {{code}} -``` +``` \ No newline at end of file diff --git a/src/prompts_template/COT_template.txt b/src/prompts_template/COT_template.txt new file mode 100644 index 0000000..8b3d578 --- /dev/null +++ b/src/prompts_template/COT_template.txt @@ -0,0 +1,21 @@ +# Task Description +{task_description} + +## Method Signature +{method_signature} + +## AI Assistant Instructions + +Follow these steps to complete the task: + +1. **Analyze and select required APIs:** + Review the following API reference and their preconditions: + {api_with_preconditions} + +2. **Implement the Dafny code:** + Create the Dafny implementation for the described task, adhering to the provided structure for each API. Utilize the provided API list and their specifications. + + Provide your implementation in Dafny syntax as follows: + + ```dafny + {code} \ No newline at end of file diff --git a/src/prompts_template/COT_template_string.file b/src/prompts_template/COT_template_string.file new file mode 100644 index 0000000..9bdfd82 --- /dev/null +++ b/src/prompts_template/COT_template_string.file @@ -0,0 +1,23 @@ +Task Description: +{task_description} + +Method Signature: +{method_signature} + + +AI ASSISTANT: +Follow these steps to complete the task: + + +Step 1: Analyze and select the required APIs and their preconditions from the list of API reference. +For this task: +{api_with_preconditions} + +Step 2: Implement the Dafny code for the described task, adhering to the provided structure for each API. Utilize the provided API list and their specifications. +Provide the implementation in Dafny syntax as follows: + +```dafny + +{code} + +``` diff --git a/src/prompts_template/task_template.md b/src/prompts_template/task_template.md new file mode 100644 index 0000000..d0fd2e6 --- /dev/null +++ b/src/prompts_template/task_template.md @@ -0,0 +1,11 @@ +# Coding Task + +You are an expert Python developer. Below is the task description: + +--- + +{{ task_description }} + +--- + +Please provide the Python code that accomplishes the above task. Include appropriate function names, documentation, and ensure the code is well-structured and follows best practices. diff --git a/src/tasks/task-7.json b/src/tasks/task-7.json index b8f53a0..646e5fb 100644 --- a/src/tasks/task-7.json +++ b/src/tasks/task-7.json @@ -1,11 +1,9 @@ { - "6": { - "task_id": "6", - "task_description": "Your task is to implement a function which takes the filename as a parameter, which will then be used to create a full file path in a predetermined directory ( e.g.,'/home/user/documents').", - "method_signature": "method CreateFullPath(filename: seq)", + "7": { + "task_id": "7", + "task_description": "Your task is to implement a function which takes the filename as a parameter, which will then be used to create a full path in a predetermined directory ( e.g.,'/var/www/files/'), then reads from the file exists in the full path and returns data.", + "method_signature": "method GetFile(filename: seq) returns (data: array)", "all_api_with_preconditions": "- static method{:axiom} Open(name: seq) returns(ok:bool, f:FileStream)\n requires non_empty_string(name)\n requires !has_dangerous_pattern(name)\n requires has_absoloute_path(name)\n requires is_valid_path_name(name)\n ensures ok ==> fresh(f) && f.IsOpen() && f.Name() == name[..]\n\n- method{:axiom} Read(p: path, fileOffset:nat32, buffer:array, start:int32, end:int32) returns(ok:bool)\n requires non_empty_string(p)\n requires !has_dangerous_pattern(p)\n requires has_valid_path_length(p)\n requires has_absoloute_path(p)\n requires is_valid_file_extension(p)\n requires has_valid_content_length(buffer)\n requires is_valid_file_extension(p)\n requires is_valid_file_extension(p)\n requires IsOpen()\n requires 0 <= start as int <= end as int <= buffer.Length\n modifies buffer\n modifies this\n ensures Name() == old(Name())\n ensures ok ==> IsOpen()\n\n- method{:axiom} Write(p: path, fileOffset:nat32, buffer:array, start:int32, end:int32) returns(ok:bool)\n requires has_valid_path_length(p)\n requires has_absoloute_path(p)\n requires is_valid_path_name(p)\n requires has_valid_content_length(buffer)\n requires is_valid_file_extension(p)\n requires 0 <= start as int32 <= end as int32\n requires IsOpen()\n modifies this\n ensures Name() == old(Name())\n ensures ok ==> IsOpen() \n\n - method Join(p: path, f: file) returns(result: path)\n requires non_empty_string(f)\n requires non_empty_string(p)\n requires !has_dangerous_pattern(f)\n requires has_absoloute_path(f)\n requires is_valid_file_name(f)\n requires is_valid_path_name(p)\n requires has_valid_file_length(f)\n requires has_valid_path_length(p)\n requires has_valid_path_length(p+f)" } } - - diff --git a/src/utils/config_reader.py b/src/utils/config_reader.py index c825d9e..6077965 100644 --- a/src/utils/config_reader.py +++ b/src/utils/config_reader.py @@ -56,6 +56,8 @@ def get_config_values(section, keys): # Read Environment Variables env_keys = ['task_path', 'base_output_path', 'interface_path'] env_config = get_config_values('ENVIRONMENT', env_keys) + + #TODO: Check if all the paths are absolute paths # Read Few-Shot Prompting Config fewshot_keys = ['RAG_json_path', 'api_reference_path', 'few_shot_examples_count']