Commit 7df7d7a4 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Push the new CheckerGenerator through the whole codebase. 

CVC3Generator is now tied to the CheckerGenerator interface, allowing for
PVS and SMTLIB to move in.  This caused a huge set of changes in other files,
to push the generator through various places.  Also, the matlab code needed
updating to work with the new functions and CheckerGenerator.  In theory it
should all be fine now.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10466 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent aae4765f

@CVC_checker/CVC_checker.m

+1 −2
Original line number Diff line number Diff line
@@ -6,15 +6,14 @@ classdef CVC_checker 
        

        command = 'cvc3';

        data = [];

        generator = ca.mcmaster.cas.matlab2smt.CVC3Generator();

        

    end

    

    

    methods(Static)

        

        [ code , query] = generate_cvc_grid( grid , level, var_def);

        [ code ] = find_parents( grid );

        cvc_string = matlab_to_cvc_syntax_translation(matlab_string, var_def);

        [ cvc_type ] = pvs_to_cvc_subtypes( pvs_type );

        

    end

@CVC_checker/generate_cvc_grid.m

+6 −6
Original line number Diff line number Diff line
@@ -14,7 +14,7 @@ 
% Author: Colin Eles elesc@mcmaster.ca

% Organization: McMaster Centre for Software Certification



function [ code , query] = generate_cvc_grid( grid , level, var_def)

function [ code , query] = generate_cvc_grid( object, grid , level, var_def)



% generate the formulas for the main grid
@@ -23,8 +23,8 @@ if isempty(parents); 
    disjoint = 'QUERY (';

    complete = 'QUERY (';

else

    disjoint = ['QUERY ' CVC_checker.matlab_to_cvc_syntax_translation(parents, var_def) ' => ('];

    complete = ['QUERY ' CVC_checker.matlab_to_cvc_syntax_translation(parents, var_def) ' => ('];

    disjoint = ['QUERY ' object.matlab_to_cvc_syntax_translation(parents, var_def) ' => ('];

    complete = ['QUERY ' object.matlab_to_cvc_syntax_translation(parents, var_def) ' => ('];

end



for i=1:size(grid.cells,2)
@@ -32,7 +32,7 @@ for i=1:size(grid.cells,2) 
  

    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), var_def) ') AND (' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(j).cond_text), var_def) ') )'];

        disjoint = [disjoint 'NOT ( (' object.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text), var_def) ') AND (' object.matlab_to_cvc_syntax_translation(char(grid.cells(j).cond_text), var_def) ') )'];



        if j~= size(grid.cells,2)

             disjoint = [disjoint ' AND ' char(10)];
@@ -45,7 +45,7 @@ for i=1:size(grid.cells,2) 
    

    

    

    complete = [complete '(' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text), var_def) ')'];

    complete = [complete '(' object.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text), var_def) ')'];

    

    if i < size(grid.cells,2) - 1

        disjoint = [disjoint ' AND ' char(10)];
@@ -67,7 +67,7 @@ code = [code 'ECHO "begin' num2str(level+2) '";' char(10) 'PUSH;' char(10) compl 


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, var_def);

        [new_code,new_queries] = object.generate_cvc_grid(grid.cells(i).subgrid,level+2, var_def);

        code = [code new_code];

        query = [query new_queries];

        level = size(query,2) - 2;

@CVC_checker/generate_file.m

+3 −3
Original line number Diff line number Diff line
@@ -20,7 +20,7 @@ function_name = char(function_names{1}(1)); 
code = [];

% output the input variables

inputs = ca.mcmaster.cas.matlab2smt.VariableParser(object.data.function_inputs);

code = char(inputs.getCVC3Output())

code = char(inputs.getCheckerOutput(object.generator))





% call the recursive function to generate the queries
@@ -28,12 +28,12 @@ new_code = ''; 
queries = [];

%generate grid 2

if size(object.data.Grid2.cells,2) > 1  

    [new_code,queries] = CVC_checker.generate_cvc_grid(object.data.Grid2,0, inputs);

    [new_code,queries] = object.generate_cvc_grid(object.data.Grid2,0, inputs);

end

code = [code new_code];



if object.data.multi_mode == 0 && size(object.data.Grid1.cells,2) > 1

    [new_code,new_queries] = CVC_checker.generate_cvc_grid(object.data.Grid1,size(queries,2), inputs);

    [new_code,new_queries] = object.generate_cvc_grid(object.data.Grid1,size(queries,2), inputs);

    queries = [queries new_queries];

    code = [code new_code];

@CVC_checker/matlab_to_cvc_syntax_translation.m

+2 −2
Original line number Diff line number Diff line
@@ -11,7 +11,7 @@ 
%   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, var_def)

function cvc_string = matlab_to_cvc_syntax_translation(object, matlab_string, var_def)



s = [matlab_string(1,:)];

for j = 2:size(matlab_string,1)
@@ -26,7 +26,7 @@ matlab_string = s; 


parser = ca.mcmaster.cas.matlab2smt.MatlabParser(var_def, matlab_string);

expr = parser.getRootExpression();

cvc_string = char(expr.getCVC3Output(expr.type()))

cvc_string = char(expr.getCheckerOutput(object.generator, expr.type()))



end

Matlab2SMT/src/main/java/ca/mcmaster/cas/matlab2smt/CVC3Generator.java

+12 −8
Original line number Diff line number Diff line
@@ -12,7 +12,7 @@ import org.apache.commons.lang3.StringUtils; 
 *

 * @author matthew

 */

final public class CVC3Generator {

final public class CVC3Generator implements CheckerGenerator{



    private static String GetSignedFixedPointFunctionFor(MatlabOperation op) {

        switch (op) {
@@ -56,7 +56,7 @@ final public class CVC3Generator { 
        throw new RuntimeException("Should never happen!");

    }



    public static String ConvertToOutputOp(MatlabOperation op, VariableType type) {

    protected static String ConvertToOutputOp(MatlabOperation op, VariableType type) {

        switch (OpTypeForVariableType(op, type)) {

            case Function:

                String func = GetSignedFixedPointFunctionFor(op);
@@ -76,7 +76,7 @@ final public class CVC3Generator { 
        }

    }



    public static OperationType OpTypeForVariableType(MatlabOperation op, VariableType type) {

    private static OperationType OpTypeForVariableType(MatlabOperation op, VariableType type) {

        if (type instanceof FixedPointVariableType && op != MatlabOperation.Equals) {

            return OperationType.Function;

        } else {
@@ -84,7 +84,8 @@ final public class CVC3Generator { 
        }

    }



    public static String GenerateOperation(MatlabOperation op, String lhsExp, String rhsExp, VariableType usedType) {

    @Override

    public String GenerateOperation(MatlabOperation op, String lhsExp, String rhsExp, VariableType usedType) {

        switch (CVC3Generator.OpTypeForVariableType(op, usedType)) {

            case CenterOp:

                return "(" + lhsExp + " " + CVC3Generator.ConvertToOutputOp(op, usedType) + " " + rhsExp + ")";
@@ -95,7 +96,8 @@ final public class CVC3Generator { 
        }

    }



    public static String GenerateVariableType(VariableType type) {

    @Override

    public String GenerateVariableType(VariableType type) {

        if (type instanceof RealVariableType) {

            return "REAL";

        } else if (type instanceof FixedPointVariableType) {
@@ -107,11 +109,13 @@ final public class CVC3Generator { 
        }

    }



    public static String GenerateVariableDecleration(String name, VariableType type) {

        return name + ":" + CVC3Generator.GenerateVariableType(type) + ";";

    @Override

    public String GenerateVariableDecleration(Variable var) {

        return var.name() + ":" + GenerateVariableType(var.type()) + ";";

    }



    public static String GenerateLiterlaValue(String value, VariableType requestedType) {

    @Override

    public String GenerateLiterlaValue(String value, VariableType requestedType) {

        if (requestedType instanceof RealVariableType || requestedType instanceof MatlabLiteral.LiteralNumberType) {

            return value;

        } else if (requestedType instanceof FixedPointVariableType) {