From 3581723a7a7ba91af19831623d73e218ca8a74c7 Mon Sep 17 00:00:00 2001 From: Colin Eles Date: Thu, 11 Nov 2010 19:41:54 +0000 Subject: [PATCH] begnining of application of SMT solver, using CVC3 solver. only works for 1D vertical grids right now, although easy to add more dimensions, etc. ALOT faster than PVS. git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6519 57e6efec-57d4-0310-aeb1-a6c144bb1a8b --- @CVC_checker/CVC_checker.m | 30 +++++++ @CVC_checker/cvc_check.m | 52 ++++++++++++ @CVC_checker/cvc_parse_result.m | 7 ++ @CVC_checker/find_parents.m | 35 ++++++++ @CVC_checker/generate_cvc_grid.m | 83 +++++++++++++++++++ @CVC_checker/generate_file.m | 39 +++++++++ .../matlab_to_cvc_syntax_translation.m | 25 ++++++ @GUI/GUI.m | 1 + @GUI/init.m | 3 + 9 files changed, 275 insertions(+) create mode 100644 @CVC_checker/CVC_checker.m create mode 100644 @CVC_checker/cvc_check.m create mode 100644 @CVC_checker/cvc_parse_result.m create mode 100644 @CVC_checker/find_parents.m create mode 100644 @CVC_checker/generate_cvc_grid.m create mode 100644 @CVC_checker/generate_file.m create mode 100644 @CVC_checker/matlab_to_cvc_syntax_translation.m diff --git a/@CVC_checker/CVC_checker.m b/@CVC_checker/CVC_checker.m new file mode 100644 index 0000000..5a43591 --- /dev/null +++ b/@CVC_checker/CVC_checker.m @@ -0,0 +1,30 @@ +classdef CVC_checker + %CVC_CHECKER Summary of this class goes here + % Detailed explanation goes here + + properties + + command = 'cvc3' + data = []; + + end + + + methods(Static) + + [ code , query] = generate_cvc_grid( grid , level) + [ code ] = find_parents( grid ) + cvc_string = matlab_to_cvc_syntax_translation(matlab_string) + + + end + + methods + + function object = CVC_checker(data) + object.data = data; + end + end + +end + diff --git a/@CVC_checker/cvc_check.m b/@CVC_checker/cvc_check.m new file mode 100644 index 0000000..d4673e4 --- /dev/null +++ b/@CVC_checker/cvc_check.m @@ -0,0 +1,52 @@ +function [ check, seqs ] = cvc_check( object ) +%CVC_CHECK Summary of this function goes here +% Detailed explanation goes here + box = waitbar(0,'Generating Proof Script'); + +[filename, queries] = object.generate_file; + + waitbar(.10,box,'Running Proof'); + +[status, result] = system(['cvc3 ' filename]) + + waitbar(.70,box,'Parsing Results'); + +seqs = []; +for i = 1:size(queries,2) + asserts = []; + + % find results of individual queries, using regexp and notations in + % output begin1 ... end1 + query_result = regexp(result,['(?<=begin' num2str(i) ').*(?=end' num2str(i) ')'],'match'); + + invalid_found = regexp(char(query_result),'Invalid.'); + + if ~isempty(invalid_found) + % formula was found to be invalid + % look for a counter example + asserts = regexp(char(query_result),'(?<=ASSERT[ ]*\()[^\n]*(?==)|(?<==)[^\n]*(?=\);)','match'); +% for j = 1:size(asserts,2) +% splits = {splits regexp(asserts(j),'=','split')}; +% +% end + + seqs = [seqs struct('id', '1234a', 'TCC', 'test', 'seq', queries(i), 'ce', {asserts})]; + end + + + +end + +if isempty(seqs) + check = 1 +else + check = 0; +end + + waitbar(1,box,'Deleting Proof Script'); + + delete(box); + + +end + diff --git a/@CVC_checker/cvc_parse_result.m b/@CVC_checker/cvc_parse_result.m new file mode 100644 index 0000000..fe77bf9 --- /dev/null +++ b/@CVC_checker/cvc_parse_result.m @@ -0,0 +1,7 @@ +function [ output_args ] = cvc_parse_result( input_args ) +%CVC_PARSE_RESULT Summary of this function goes here +% Detailed explanation goes here + + +end + diff --git a/@CVC_checker/find_parents.m b/@CVC_checker/find_parents.m new file mode 100644 index 0000000..69061a1 --- /dev/null +++ b/@CVC_checker/find_parents.m @@ -0,0 +1,35 @@ +function [ code ] = find_parents( cell ) +% assumption, initial input will be grid we want to find parents for not +% parent cell itself + +code = ''; +if isempty(cell) + % current cell is empty + code = ''; +else + if isempty(cell.parent_grid.parent_cell) + % no parent cell + + else + % there is a parent cell + top = char(CVC_checker.find_parents(cell.parent_grid.parent_cell)); + code = char(cell.parent_grid.parent_cell.cond_text); + if isempty(top); + % there were no more above this cell + + else + % there were more above this cell + code = [code ' AND ' top]; + end + + + end + + +end + + + + +end + diff --git a/@CVC_checker/generate_cvc_grid.m b/@CVC_checker/generate_cvc_grid.m new file mode 100644 index 0000000..9e0e4e3 --- /dev/null +++ b/@CVC_checker/generate_cvc_grid.m @@ -0,0 +1,83 @@ +function [ code , query] = generate_cvc_grid( grid , level) +%GENERATE_CVC_GRID Summary of this function goes here +% Detailed explanation goes here + +% generate the formulas for the main grid + +parents = CVC_checker.find_parents(grid.cells(1)); +if isempty(parents); + disjoint = 'QUERY ('; + complete = 'QUERY ('; +else + disjoint = ['QUERY ' parents ' => (']; + complete = ['QUERY ' parents ' => (']; +end + +for i=1:size(grid.cells,2) + +% 1 +% 2 +% 3 +% +% 1 2 +% 1 3 +% 2 3 +% +% 1 2 3 4 +% 1 2 +% 1 3 +% 1 4 +% + + for j = i+1:size(grid.cells,2) + % compare i to j + disjoint = [disjoint 'NOT ( (' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text)) ') AND (' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(j).cond_text)) ') )']; + + if j~= size(grid.cells,2) + disjoint = [disjoint ' AND ' char(10)]; + + end + + end + % need to do pairwise disjointness + % otherwise doesn't work + + + + complete = [complete '(' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text)) ')']; + + if i < size(grid.cells,2) - 1 + disjoint = [disjoint ' AND ' char(10)]; + end + + if i < size(grid.cells,2) + complete = [complete ' OR ']; + end +end +disjoint = [disjoint ');']; +complete = [complete ');']; + +query = [{disjoint} {complete}]; + +code = ['ECHO "begin' num2str(level+1) '";' char(10) 'PUSH;' char(10) disjoint char(10) 'COUNTERMODEL;' char(10) 'POP;' char(10) 'ECHO "end' num2str(level+1) '";' char(10)]; +code = [code 'ECHO "begin' num2str(level+2) '";' char(10) 'PUSH;' char(10) complete char(10) 'COUNTERMODEL;' char(10) 'POP;' char(10) 'ECHO "end' num2str(level+2) '";' char(10)]; + + + +for i=1:size(grid.cells,2) + if ~isempty(grid.cells(i).subgrid) + [new_code,new_queries] = CVC_checker.generate_cvc_grid(grid.cells(i).subgrid,level+2); + code = [code new_code]; + query = [query new_queries]; + level = size(query,2) - 2; + end + +end + + + + + + +end + diff --git a/@CVC_checker/generate_file.m b/@CVC_checker/generate_file.m new file mode 100644 index 0000000..d05e555 --- /dev/null +++ b/@CVC_checker/generate_file.m @@ -0,0 +1,39 @@ +function [ filename, queries ] = generate_file( object ) +%GENERATE_FILE Summary of this function goes here +% Detailed explanation goes here + +function_names = EMLGenerator.parse_inputs(object.data.function_name); +function_name = char(function_names{1}(1)); + + +code = []; +% output the input variables +inputs = EMLGenerator.parse_inputs(object.data.function_inputs); +for i = 1:size(inputs,2) + code = [code char(inputs{i}(1)) ':INT;' char(10)]; +end + + +% call the recursive function to generate the queries + +%generate grid 1 +[new_code,queries] = CVC_checker.generate_cvc_grid(object.data.Grid2,0); +code = [code new_code]; + + +% generate grid 2 + + + +char(code) + +fileid = fopen([function_name '.cvc'],'w'); +fprintf(fileid,'%s',char(code)); +fclose(fileid); + + +filename = [function_name '.cvc']; + + +end + diff --git a/@CVC_checker/matlab_to_cvc_syntax_translation.m b/@CVC_checker/matlab_to_cvc_syntax_translation.m new file mode 100644 index 0000000..68462a6 --- /dev/null +++ b/@CVC_checker/matlab_to_cvc_syntax_translation.m @@ -0,0 +1,25 @@ +%% matlab_to_cvc_syntax_translation +%translate matlab syntax to cvc syntax, +% will be added to in the future +% will only work for functions in the prelude +% +% inputs: +% object:cvc_checker - cvc_checker object +% matlab_string:string - string to be converted from matlab +% syntax to cvc +% outputs; +% cvc_string:string - string converted to cvc syntax. +% Author: Colin Eles elesc@mcmaster.ca +% Organization: McMaster Centre for Software Certification +function cvc_string = matlab_to_cvc_syntax_translation(matlab_string) +cvc_string = regexprep(matlab_string,'&&',' AND '); +cvc_string = regexprep(cvc_string,'~(?!=)',' NOT '); +cvc_string = regexprep(cvc_string,'~=',' /= '); +cvc_string = regexprep(cvc_string,'==',' = '); +cvc_string = regexprep(cvc_string,'\|\|',' OR '); +cvc_string = regexprep(cvc_string,'ceil','ceiling'); +end + + + + diff --git a/@GUI/GUI.m b/@GUI/GUI.m index e82037b..fb0e394 100644 --- a/@GUI/GUI.m +++ b/@GUI/GUI.m @@ -50,6 +50,7 @@ classdef GUI < handle input_label = []; Data = []; PVS = []; + CVC = []; pvs_checked = []; mode = []; EMLGen = []; diff --git a/@GUI/init.m b/@GUI/init.m index baef490..3f42cfe 100644 --- a/@GUI/init.m +++ b/@GUI/init.m @@ -158,6 +158,7 @@ uimenu(pvsmenu,'Label','PVS Settings','Callback',@(src,event)settings_call(objec uimenu(pvsmenu,'Label','Check Status','Callback',@(src,event)prf_file_call(object,src,event)); uimenu(pvsmenu,'Label','Generate PVS file','Callback',@(src,event)pvs_file_call(object,src,event)); uimenu(pvsmenu,'Label','Typecheck SimTypes','Callback',@(src,event)pvs_ext_call_sim(object,src,event)); +uimenu(pvsmenu,'Label','CVC Solve','Callback',@(src,event)cvc_ext_call(object,src,event)); uimenu(helpmenu,'Label','Product Help','Callback',@(src,event)help_call(object,src,event)); uimenu(helpmenu,'Label','About Table Tool','Callback',@(src,event)about_call(object,src,event)); @@ -189,6 +190,8 @@ object.PVS = PVS_checker(object.Data); object.EMLGen = EMLGenerator(object.Data); +object.CVC = CVC_checker(object.Data); + object.initialized = 1; object.Data.open = 1; -- GitLab