diff --git a/backend/Dockerfile b/backend/Dockerfile index f89497b..3abf6bf 100644 --- a/backend/Dockerfile +++ b/backend/Dockerfile @@ -5,6 +5,9 @@ WORKDIR /backend COPY . /backend +RUN apt-get update && apt-get install -y +RUN apt-get install z3 -y + RUN pip install --no-cache-dir --upgrade pip setuptools RUN pip install --no-cache-dir -r requirements.txt diff --git a/backend/routes.py b/backend/routes.py index e200ab5..9d40dd7 100644 --- a/backend/routes.py +++ b/backend/routes.py @@ -3,7 +3,7 @@ from datetime import datetime, timedelta from flask import Blueprint, request, jsonify, session, make_response, abort from utils.db import db, Data -from utils import xmv +from utils import xmv, z3 from utils.permalink_generator import generate_passphrase from utils.db_query import * import pytz @@ -11,10 +11,17 @@ routes = Blueprint('routes', __name__) -TIME_WINDOW = 1 # time window within which multiple requests are not allowed +TIME_WINDOW = 1 -# Check if the code is too large def is_valid_size(code: str) -> bool: + """Check if the code is less than 1MB + + Parameters: + code (str): The code to be checked + + Returns: + bool: True if the code is less than 1MB, False otherwise + """ size_in_bytes = sys.getsizeof(code) size_in_mb = size_in_bytes / (1024*1024) return size_in_mb <= 1 @@ -22,13 +29,14 @@ def is_valid_size(code: str) -> bool: @routes.route('/api/') def index(): - current_time = datetime.now(pytz.utc) - last_request_time = session.get('last_request_time') - if last_request_time is not None and current_time - last_request_time < timedelta(seconds=TIME_WINDOW): - return abort(429) # HTTP status code for "Too Many Requests" + """Index page""" + current_time = datetime.now(pytz.utc) + last_request_time = session.get('last_request_time') + if last_request_time is not None and current_time - last_request_time < timedelta(seconds=TIME_WINDOW): + return abort(429) # Too Many Requests - session['last_request_time'] = current_time - return "Request accepted" + session['last_request_time'] = current_time + return "Request accepted" @@ -116,7 +124,29 @@ def run_nuxmv(): res = xmv.process_commands(code) response = make_response(jsonify({'result': res}), 200) except: - response = make_response(jsonify({'result': "Error running nuXmv. Server is busy. Please try again after"}), 503) + response = make_response(jsonify({'result': "Error running nuXmv. Server is busy. Please try again"}), 503) return response - \ No newline at end of file + +@routes.route('/api/run_z3', methods=['POST']) +def run_z3(): + data = request.get_json() + code = data['code'] + current_time = datetime.now(pytz.utc) + + # Check if the code is too large + if not is_valid_size(code): + return {'error': "The code is too large."}, 413 + + last_request_time = session.get('last_request_time') + + if last_request_time is not None and current_time - last_request_time < timedelta(seconds=TIME_WINDOW): + response = make_response(jsonify({'error': "You've already made a request recently."}), 429) + return response + try: + res = z3.process_commands(code) + response = make_response(jsonify({'result': res}), 200) + except: + response = make_response(jsonify({'result': "Error running Z3. Server is busy. Please try again"}), 503) + + return response \ No newline at end of file diff --git a/backend/utils/z3.py b/backend/utils/z3.py new file mode 100644 index 0000000..f2bdf1b --- /dev/null +++ b/backend/utils/z3.py @@ -0,0 +1,48 @@ +import os +import subprocess +import tempfile +import re +import queue +import concurrent.futures + +MAX_CONCURRENT_REQUESTS = 10 # Maximum number of concurrent subprocesses + +executor = concurrent.futures.ThreadPoolExecutor(max_workers=MAX_CONCURRENT_REQUESTS) #thread pool with a maximum of max_concurrent threads + +code_queue = queue.Queue() # to hold incoming commands + + +def run_z3(code: str): + tmp_file = tempfile.NamedTemporaryFile(mode='w', delete=False, suffix='.smt2') + tmp_file.write(code.strip()) + tmp_file.close() + print(tmp_file.name) + command = ["z3", "-smt2", tmp_file.name] + try: + result = subprocess.run(command, capture_output=True, text=True, timeout=5) + os.remove(tmp_file.name) + return result.stdout + except subprocess.TimeoutExpired: + os.remove(tmp_file.name) + return "Process timed out after {} seconds".format(5) + + +def prettify_output(stdout: str): + res = [line for line in stdout.split('\n') if '***' not in line.lower() and line.strip()] + return '\n'.join(res) + +def prettify_error(stderr: str): + pattern = r'^.*?:(?=\sline)' + res = [re.sub(pattern, 'error:', line) for line in stderr.split('\n') ] + res_clean = [item for item in res if item != ''] + return '\n'.join(res_clean[:-3]) + + +def process_commands(code: str): + code_queue.put(code) + while True: + code_command = code_queue.get() + if code_queue is None: + break + ex = executor.submit(run_z3, code_command) + return ex.result() diff --git a/frontend/main.js b/frontend/main.js index 29f6150..766e38f 100644 --- a/frontend/main.js +++ b/frontend/main.js @@ -456,7 +456,7 @@ function run_limboole(wrapper) { info.innerText = ""; let non_ascii = findNonASCII(window.input_textarea); - if(findNonASCII){ + if(non_ascii != null){ info.innerText += `:${non_ascii.position}:parse error at '${non_ascii.character}' expected ASCII character\n`; run_button_enable(); return; @@ -514,25 +514,67 @@ Module.print = (text) => { info.innerText += text + "\n"; }; + +/* ---------------Start z3 --------------- */ function run_z3(code) { const info = document.getElementById("info"); editor.getModel().setValue(code); - if (z3_loaded) { + fetch(apiUrl+'run_z3', { + method: 'POST', + headers: { + 'Content-Type': 'application/json', + }, + body: JSON.stringify({code: code}), + }) + .then(response => { + if (response.status === 200) { + return response.json(); + } else if(response.status === 413){ + alert("Code size is too large!"); + throw new Error('Request failed with status ' + response.status); + } else if(response.status === 429){ + alert("Slow Down! You've already made a request recently."); + throw new Error('Request failed with status ' + response.status); + }else { + throw new Error('Request failed with status ' + response.status); + } + }) + .then(data => { try { info.innerText = ""; + info.innerText += data.result; save_to_db(code); - let res = Z3.solve(code); - info.innerText += res; } catch (error) { console.error(error); - // info.innerText += error; + //info.innerText += error; } - } else { - info.innerText = "Wait for Z3 to load and try again." - } - run_button_enable() + }) + .catch((error) => { + console.error('Error:', error); + }); + run_button_enable(); + } +// function run_z3(code) { +// const info = document.getElementById("info"); +// editor.getModel().setValue(code); +// if (z3_loaded) { +// try { +// info.innerText = ""; +// save_to_db(code); +// let res = Z3.solve(code); +// info.innerText += res; +// } catch (error) { +// console.error(error); +// // info.innerText += error; +// } +// } else { +// info.innerText = "Wait for Z3 to load and try again." +// } +// run_button_enable() +// } + /* ---------------Start nuXmv --------------- */ function run_nuxmv(code) { @@ -829,7 +871,7 @@ function findNonASCII(input) { character: match[0], position: match.index }; + }else{ + return null; } - - return null; } \ No newline at end of file