<commit_before>/*
 * ProgramFunctionExpWalker.java
 * ---------------------------------
 * Copyright (c) 2017
 * RESOLVE Software Research Group
 * School of Computing
 * Clemson University
 * All rights reserved.
 * ---------------------------------
 * This file is subject to the terms and conditions defined in
 * file 'LICENSE.txt', which is part of this source code package.
 */
package edu.clemson.cs.rsrg.vcgeneration.utilities.treewalkers;

import edu.clemson.cs.rsrg.absyn.declarations.operationdecl.OperationDec;
import edu.clemson.cs.rsrg.absyn.declarations.variabledecl.ParameterVarDec;
import edu.clemson.cs.rsrg.absyn.expressions.Exp;
import edu.clemson.cs.rsrg.absyn.expressions.mathexpr.EqualsExp;
import edu.clemson.cs.rsrg.absyn.expressions.mathexpr.EqualsExp.Operator;
import edu.clemson.cs.rsrg.absyn.expressions.mathexpr.InfixExp;
import edu.clemson.cs.rsrg.absyn.expressions.mathexpr.OldExp;
import edu.clemson.cs.rsrg.absyn.expressions.mathexpr.VarExp;
import edu.clemson.cs.rsrg.absyn.expressions.programexpr.ProgramExp;
import edu.clemson.cs.rsrg.absyn.expressions.programexpr.ProgramFunctionExp;
import edu.clemson.cs.rsrg.parsing.data.Location;
import edu.clemson.cs.rsrg.parsing.data.PosSymbol;
import edu.clemson.cs.rsrg.statushandling.exception.MiscErrorException;
import edu.clemson.cs.rsrg.treewalk.TreeWalkerVisitor;
import edu.clemson.cs.rsrg.typeandpopulate.entry.OperationEntry;
import edu.clemson.cs.rsrg.typeandpopulate.entry.ProgramParameterEntry.ParameterMode;
import edu.clemson.cs.rsrg.typeandpopulate.programtypes.PTType;
import edu.clemson.cs.rsrg.typeandpopulate.symboltables.ModuleScope;
import edu.clemson.cs.rsrg.typeandpopulate.typereasoning.TypeGraph;
import edu.clemson.cs.rsrg.vcgeneration.utilities.Utilities;
import java.util.*;

/**
 * <p>This class extracts ensures clauses (with the appropriate substitutions)
 * from walking potentially nested {@link ProgramFunctionExp}. This visitor logic
 * is implemented as a {@link TreeWalkerVisitor}.</p>
 *
 * @author <NAME>
 * @version 2.0
 */
public class ProgramFunctionExpWalker extends TreeWalkerVisitor {

    // ===========================================================
    // Member Fields
    // ===========================================================

    /**
     * <p>The module scope for the file we are generating
     * {@code VCs} for.</p>
     */
    private final ModuleScope myCurrentModuleScope;

    /** <p>The current procedure declaration we are processing.</p> */
    private final OperationEntry myCurrentOperationEntry;

    /**
     * <p>If this is a {@code Recursive Procedure}, then this will contain
     * the {@code decreasing} clause.</p>
     */
    private final Exp myDecreasingExp;

    /**
     * <p>A map that contains the modified ensures clause with the formal
     * replaced with the actuals for each of the nested function calls.</p>
     */
    private final Map<ProgramFunctionExp, Exp> myEnsuresClauseMap;

    /**
     * <p>A map that stores all the details associated with
     * a particular {@link Location}.</p>
     */
    private final Map<Location, String> myLocationDetails;

    /**
     * <p>A list that contains the modified requires clauses with the formal
     * replaced with the actuals for each of the nested function calls.</p>
     */
    private final List<Exp> myRequiresClauseList;

    /** <p>A list that contains all the restores parameter ensures clauses</p> */
    private final List<Exp> myRestoresParamEnsuresClauses;

    /**
     * <p>This is the math type graph that indicates relationship
     * between different math types.</p>
     */
    private final TypeGraph myTypeGraph;

    // ===========================================================
    // Constructors
    // ===========================================================

    /**
     * <p>This creates a {@link TreeWalkerVisitor} that visits
     * and generates {@code requires} and {@code ensures} clauses
     * for potentially nested function calls.</p>
     *
     * <p>Note that this constructor is used by non-procedure declarations,
     * where there isn't a current {@link OperationEntry} or a
     * {@code decreasing} clause.</p>
     *
     * @param moduleScope The current module scope we are visiting.
     * @param g The current type graph.
     */
    public ProgramFunctionExpWalker(ModuleScope moduleScope, TypeGraph g) {
        this(null, null, moduleScope, g);
    }

    /**
     * <p>This creates a {@link TreeWalkerVisitor} that visits
     * and generates {@code requires} and {@code ensures} clauses
     * for potentially nested function calls.</p>
     *
     * @param moduleScope The current module scope we are visiting.
     * @param g The current type graph.
     */
    public ProgramFunctionExpWalker(OperationEntry entry, Exp decreasingExp, ModuleScope moduleScope, TypeGraph g) {
        myCurrentModuleScope = moduleScope;
        myCurrentOperationEntry = entry;
        myDecreasingExp = decreasingExp;
        myEnsuresClauseMap = new HashMap<>();
        myRequiresClauseList = new LinkedList<>();
        myRestoresParamEnsuresClauses = new LinkedList<>();
        myLocationDetails = new HashMap<>();
        myTypeGraph = g;
    }

    // ===========================================================
    // Visitor Methods
    // ===========================================================

    // -----------------------------------------------------------
    // Program Expression-Related
    // -----------------------------------------------------------

    /**
     * <p>Code that gets executed after visiting a {@link ProgramFunctionExp}.</p>
     *
     * @param exp A program function expression.
     */
    @Override
    public final void postProgramFunctionExp(ProgramFunctionExp exp) {
        // Create a string with the qualifier (if any) and the operation name
        String fullOperationName = exp.getName().getName();
        if (exp.getQualifier() != null) {
            fullOperationName = exp.getQualifier() + "::" + fullOperationName;
        }

        // Call a method to locate the operation entry for this call
        OperationEntry operationEntry = getOperationEntry(exp);
        OperationDec operationDec =
                (OperationDec) operationEntry.getDefiningElement();

        // Only need to do something if it is not "requires true"
        if (!VarExp.isLiteralTrue(operationDec.getRequires().getAssertionExp())) {
            // Replace formals in the original requires clause with the
            // actuals from the function call.
            Exp requiresExp =
                    replaceFormalWithActualReq(operationDec.getRequires()
                            .getAssertionExp(), operationDec.getParameters(),
                            exp.getArguments());

            // TODO: Replace any facility declaration actuals in the requires clause.

            // Store the location detail for the function call's requires clause
            myLocationDetails.put(requiresExp.getLocation(),
                    "Requires Clause of " + fullOperationName);

            // Store the modified requires clause in our list
            myRequiresClauseList.add(requiresExp);
        }

        // YS: The ensures clause was sanity checked already, so no need to do it here.
        // Replace formals in the original ensures clause with the actuals
        // from the function call.
        Exp ensuresExp =
                replaceFormalWithActualEns(operationDec.getEnsures()
                        .getAssertionExp(), operationDec.getParameters(), exp
                        .getArguments());

        // TODO: Replace any facility declaration actuals in the ensures clause.

        // Store the location detail for the function call's ensures clause
        myLocationDetails.put(ensuresExp.getLocation(), "Ensures Clause of "
                + fullOperationName);

        // Store the modified ensures clause in our map
        myEnsuresClauseMap.put(exp, ensuresExp);

        // Add any ensures clauses for restores parameter to our restores parameter
        // ensures clause list.
        generateRestoresParamEnsuresClause(fullOperationName, operationDec
                .getParameters(), exp.getArguments());

        // Check to see if this function is calling itself recursively
    }

    // ===========================================================
    // Public Methods
    // ===========================================================

    /**
     * <p>This method returns the final modified ensures clause
     * after all the necessary replacement/substitutions have been made.</p>
     *
     * <p>Note that the return value is removed from the class and
     * subsequent calls to this method with the same {@code exp}<commit_msg>Make sure we have a decreasing clause<commit_after>/*
 * ProgramFunctionExpWalker.java
 * ---------------------------------
 * Copyright (c) 2017
 * RESOLVE Software Research Group
 * School of Computing
 * Clemson University
 * All rights reserved.
 * ---------------------------------
 * This file is subject to the terms and conditions defined in
 * file 'LICENSE.txt', which is part of this source code package.
 */
package edu.clemson.cs.rsrg.vcgeneration.utilities.treewalkers;

import edu.clemson.cs.rsrg.absyn.declarations.operationdecl.OperationDec;
import edu.clemson.cs.rsrg.absyn.declarations.variabledecl.ParameterVarDec;
import edu.clemson.cs.rsrg.absyn.expressions.Exp;
import edu.clemson.cs.rsrg.absyn.expressions.mathexpr.EqualsExp;
import edu.clemson.cs.rsrg.absyn.expressions.mathexpr.EqualsExp.Operator;
import edu.clemson.cs.rsrg.absyn.expressions.mathexpr.InfixExp;
import edu.clemson.cs.rsrg.absyn.expressions.mathexpr.OldExp;
import edu.clemson.cs.rsrg.absyn.expressions.mathexpr.VarExp;
import edu.clemson.cs.rsrg.absyn.expressions.programexpr.ProgramExp;
import edu.clemson.cs.rsrg.absyn.expressions.programexpr.ProgramFunctionExp;
import edu.clemson.cs.rsrg.parsing.data.Location;
import edu.clemson.cs.rsrg.parsing.data.PosSymbol;
import edu.clemson.cs.rsrg.statushandling.exception.MiscErrorException;
import edu.clemson.cs.rsrg.statushandling.exception.SourceErrorException;
import edu.clemson.cs.rsrg.treewalk.TreeWalkerVisitor;
import edu.clemson.cs.rsrg.typeandpopulate.entry.OperationEntry;
import edu.clemson.cs.rsrg.typeandpopulate.entry.ProgramParameterEntry.ParameterMode;
import edu.clemson.cs.rsrg.typeandpopulate.programtypes.PTType;
import edu.clemson.cs.rsrg.typeandpopulate.symboltables.ModuleScope;
import edu.clemson.cs.rsrg.typeandpopulate.typereasoning.TypeGraph;
import edu.clemson.cs.rsrg.vcgeneration.utilities.Utilities;
import java.util.*;

/**
 * <p>This class extracts ensures clauses (with the appropriate substitutions)
 * from walking potentially nested {@link ProgramFunctionExp}. This visitor logic
 * is implemented as a {@link TreeWalkerVisitor}.</p>
 *
 * @author <NAME>
 * @version 2.0
 */
public class ProgramFunctionExpWalker extends TreeWalkerVisitor {

    // ===========================================================
    // Member Fields
    // ===========================================================

    /**
     * <p>The module scope for the file we are generating
     * {@code VCs} for.</p>
     */
    private final ModuleScope myCurrentModuleScope;

    /** <p>The current procedure declaration we are processing.</p> */
    private final OperationEntry myCurrentOperationEntry;

    /**
     * <p>If this is a {@code Recursive Procedure}, then this will contain
     * the {@code decreasing} clause.</p>
     */
    private final Exp myDecreasingExp;

    /**
     * <p>A map that contains the modified ensures clause with the formal
     * replaced with the actuals for each of the nested function calls.</p>
     */
    private final Map<ProgramFunctionExp, Exp> myEnsuresClauseMap;

    /**
     * <p>A map that stores all the details associated with
     * a particular {@link Location}.</p>
     */
    private final Map<Location, String> myLocationDetails;

    /**
     * <p>A list that contains the modified requires clauses with the formal
     * replaced with the actuals for each of the nested function calls.</p>
     */
    private final List<Exp> myRequiresClauseList;

    /** <p>A list that contains all the restores parameter ensures clauses</p> */
    private final List<Exp> myRestoresParamEnsuresClauses;

    /**
     * <p>This is the math type graph that indicates relationship
     * between different math types.</p>
     */
    private final TypeGraph myTypeGraph;

    // ===========================================================
    // Constructors
    // ===========================================================

    /**
     * <p>This creates a {@link TreeWalkerVisitor} that visits
     * and generates {@code requires} and {@code ensures} clauses
     * for potentially nested function calls.</p>
     *
     * <p>Note that this constructor is used by non-procedure declarations,
     * where there isn't a current {@link OperationEntry} or a
     * {@code decreasing} clause.</p>
     *
     * @param moduleScope The current module scope we are visiting.
     * @param g The current type graph.
     */
    public ProgramFunctionExpWalker(ModuleScope moduleScope, TypeGraph g) {
        this(null, null, moduleScope, g);
    }

    /**
     * <p>This creates a {@link TreeWalkerVisitor} that visits
     * and generates {@code requires} and {@code ensures} clauses
     * for potentially nested function calls.</p>
     *
     * @param moduleScope The current module scope we are visiting.
     * @param g The current type graph.
     */
    public ProgramFunctionExpWalker(OperationEntry entry, Exp decreasingExp, ModuleScope moduleScope, TypeGraph g) {
        myCurrentModuleScope = moduleScope;
        myCurrentOperationEntry = entry;
        myDecreasingExp = decreasingExp;
        myEnsuresClauseMap = new HashMap<>();
        myRequiresClauseList = new LinkedList<>();
        myRestoresParamEnsuresClauses = new LinkedList<>();
        myLocationDetails = new HashMap<>();
        myTypeGraph = g;
    }

    // ===========================================================
    // Visitor Methods
    // ===========================================================

    // -----------------------------------------------------------
    // Program Expression-Related
    // -----------------------------------------------------------

    /**
     * <p>Code that gets executed after visiting a {@link ProgramFunctionExp}.</p>
     *
     * @param exp A program function expression.
     */
    @Override
    public final void postProgramFunctionExp(ProgramFunctionExp exp) {
        // Create a string with the qualifier (if any) and the operation name
        String fullOperationName = exp.getName().getName();
        if (exp.getQualifier() != null) {
            fullOperationName = exp.getQualifier() + "::" + fullOperationName;
        }

        // Call a method to locate the operation entry for this call
        OperationEntry operationEntry = getOperationEntry(exp);
        OperationDec operationDec =
                (OperationDec) operationEntry.getDefiningElement();

        // Only need to do something if it is not "requires true"
        if (!VarExp.isLiteralTrue(operationDec.getRequires().getAssertionExp())) {
            // Replace formals in the original requires clause with the
            // actuals from the function call.
            Exp requiresExp =
                    replaceFormalWithActualReq(operationDec.getRequires()
                            .getAssertionExp(), operationDec.getParameters(),
                            exp.getArguments());

            // TODO: Replace any facility declaration actuals in the requires clause.

            // Store the location detail for the function call's requires clause
            myLocationDetails.put(requiresExp.getLocation(),
                    "Requires Clause of " + fullOperationName);

            // Store the modified requires clause in our list
            myRequiresClauseList.add(requiresExp);
        }

        // YS: The ensures clause was sanity checked already, so no need to do it here.
        // Replace formals in the original ensures clause with the actuals
        // from the function call.
        Exp ensuresExp =
                replaceFormalWithActualEns(operationDec.getEnsures()
                        .getAssertionExp(), operationDec.getParameters(), exp
                        .getArguments());

        // TODO: Replace any facility declaration actuals in the ensures clause.

        // Store the location detail for the function call's ensures clause
        myLocationDetails.put(ensuresExp.getLocation(), "Ensures Clause of "
                + fullOperationName);

        // Store the modified ensures clause in our map
        myEnsuresClauseMap.put(exp, ensuresExp);

        // Add any ensures clauses for restores parameter to our restores parameter
        // ensures clause list.
        generateRestoresParamEnsuresClause(fullOperationName, operationDec
                .getParameters(), exp.getArguments());

        // Check to see if this function is calling itself recursively
        if (myCurrentOperationEntry != null
                && myCurrentOperationEntry.equals(operationEntry)) {
            // Make sure we have a decreasing clause
            if (myDecreasingExp == null) {
                throw new MiscErrorException(
                        "[VCGenerator] Cannot locate the decreasing clause for: "
                                + exp.toString(), new RuntimeException());
            }
        }
    }

    // ===========================================================
    // Public Methods
    // ===========================================================

    /**
     * <p>This method returns the final modified ensures clause
     * after all the necessary replacement/substitutions have been made.</p>
     *
     * <p>Note that the return value is removed from the class and
     * subsequent calls to this method with the same {@code exp}
{'fraction_non_alphanumeric': 0.15570151230820178, 'fraction_numerical': 0.0006623247599072745, 'mean_word_length': 2.75445503522586, 'pattern_counts': {'":': 2, '<': 79, '<?xml version=': 0, '>': 79, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1225118', 'n_tokens_mistral': 4758, 'n_tokens_neox': 4536, 'n_words': 1363}