infer.cxx

ecos实时嵌入式操作系统

        if (CdlInfer::subexpr_bool(sub_transaction, expr, lhs, false, level) &&
            CdlInfer::subexpr_bool(sub_transaction, expr, rhs, false, level)) {
            sub_transaction->commit();
            result = true;
        } else {
            sub_transaction->cancel();
        }
        delete sub_transaction;
    }
    
    CYG_REPORT_RETVAL(result);
    return result;
}

// ----------------------------------------------------------------------------

static bool
infer_handle_IMPLIES_bool(CdlTransaction transaction, CdlExpression expr, unsigned int lhs, unsigned int rhs,
                     bool goal, int level)
{
    CYG_REPORT_FUNCNAMETYPE("infer_handle_implies_bool", "result %d");
    CYG_REPORT_FUNCARG4XV(transaction, expr, lhs, rhs);
    CYG_PRECONDITION_CLASSC(transaction);
    CYG_PRECONDITION_CLASSC(expr);
    CYG_PRECONDITIONC(lhs != rhs);


    bool result = false;
    
    if (goal) {
        // A implies B -> !A || B
        // Given a choice between !A or B, arguably the "implies"
        // operator has the connotation that B is preferred. All other
        // things being equal, infer_choose2() will prefer the rhs
        // over the lhs so this is achieved automagically.
        
        CdlTransaction lhs_transaction = transaction->make(transaction->get_conflict());
        CdlTransaction rhs_transaction = transaction->make(transaction->get_conflict());
        bool lhs_result = CdlInfer::subexpr_bool(lhs_transaction, expr, lhs, false, level);
        bool rhs_result = CdlInfer::subexpr_bool(rhs_transaction, expr, rhs, true, level);

        result = infer_choose2(lhs_transaction, lhs_result, rhs_transaction, rhs_result);
        
    } else {
        
        // !(A implies B) -> !(!A || B) -> (A && !B)
        CdlTransaction sub_transaction = transaction->make(transaction->get_conflict());
        if (CdlInfer::subexpr_bool(sub_transaction, expr, lhs, true, level) &&
            CdlInfer::subexpr_bool(sub_transaction, expr, rhs, false, level)) {
            sub_transaction->commit();
            result = true;
        } else {
            sub_transaction->cancel();
        }
        delete sub_transaction;
    }
    
    CYG_REPORT_RETVAL(result);
    return result;
}

// ----------------------------------------------------------------------------

static bool
infer_handle_XOR_bool(CdlTransaction transaction, CdlExpression expr, unsigned int lhs, unsigned int rhs,
                     bool goal, int level)
{
    CYG_REPORT_FUNCNAMETYPE("infer_handle_XOR_bool", "result %d");
    CYG_REPORT_FUNCARG4XV(transaction, expr, lhs, rhs);
    CYG_PRECONDITION_CLASSC(transaction);
    CYG_PRECONDITION_CLASSC(expr);
    CYG_PRECONDITIONC(lhs != rhs);


    bool result = false;
    
    if (goal) {
        // (A xor B) -> (A && !B) || (!A && B)

        CdlTransaction sub1 = transaction->make(transaction->get_conflict());
        CdlTransaction sub2 = transaction->make(transaction->get_conflict());
        bool result1 = (CdlInfer::subexpr_bool(sub1, expr, lhs, true, level) &&
                        CdlInfer::subexpr_bool(sub1, expr, rhs, false, level));
        bool result2 = (CdlInfer::subexpr_bool(sub2, expr, lhs, false, level) &&
                        CdlInfer::subexpr_bool(sub2, expr, rhs, true, level));
                           
        result = infer_choose2(sub1, result1, sub2, result2);
        
    } else {
        
        // !(A xor B) -> (!A && !B) || (A && B)
        CdlTransaction sub1 = transaction->make(transaction->get_conflict());
        CdlTransaction sub2 = transaction->make(transaction->get_conflict());
        bool result1 = (CdlInfer::subexpr_bool(sub1, expr, lhs, false, level) &&
                        CdlInfer::subexpr_bool(sub1, expr, rhs, false, level));
        bool result2 = (CdlInfer::subexpr_bool(sub2, expr, lhs, true, level) &&
                        CdlInfer::subexpr_bool(sub2, expr, rhs, true, level));
                           
        result = infer_choose2(sub1, result1, sub2, result2);
    }
    
    CYG_REPORT_RETVAL(result);
    return result;
}

// ----------------------------------------------------------------------------

static bool
infer_handle_EQV_bool(CdlTransaction transaction, CdlExpression expr, unsigned int lhs, unsigned int rhs,
                     bool goal, int level)
{
    CYG_REPORT_FUNCNAMETYPE("infer_handle_EQV_bool", "result %d");
    CYG_REPORT_FUNCARG4XV(transaction, expr, lhs, rhs);
    CYG_PRECONDITION_CLASSC(transaction);
    CYG_PRECONDITION_CLASSC(expr);
    CYG_PRECONDITIONC(lhs != rhs);


    bool result = false;
    
    if (goal) {
        // (A eqv B) -> (A && B) || (!A && !B)

        CdlTransaction sub1 = transaction->make(transaction->get_conflict());
        CdlTransaction sub2 = transaction->make(transaction->get_conflict());
        bool result1 = (CdlInfer::subexpr_bool(sub1, expr, lhs, true, level) &&
                        CdlInfer::subexpr_bool(sub1, expr, rhs, true, level));
        bool result2 = (CdlInfer::subexpr_bool(sub2, expr, lhs, false, level) &&
                        CdlInfer::subexpr_bool(sub2, expr, rhs, false, level));
                           
        result = infer_choose2(sub1, result1, sub2, result2);
    } else {
        // !(A eqv B) -> (A && !B) || (!A && B)

        CdlTransaction sub1 = transaction->make(transaction->get_conflict());
        CdlTransaction sub2 = transaction->make(transaction->get_conflict());
        bool result1 = (CdlInfer::subexpr_bool(sub1, expr, lhs, true, level) &&
                        CdlInfer::subexpr_bool(sub1, expr, rhs, false, level));
        bool result2 = (CdlInfer::subexpr_bool(sub2, expr, lhs, false, level) &&
                        CdlInfer::subexpr_bool(sub2, expr, rhs, true, level));
                           
        result = infer_choose2(sub1, result1, sub2, result2);
    }
    
    CYG_REPORT_RETVAL(result);
    return result;
}

//}}}
//{{{  infer_handle_Equal()                     

// ----------------------------------------------------------------------------
// Handle expressions of the form A == B. This can be achieved either by
// evaluating B and trying to assign the result to A, or vice versa. There
// is a problem if assigning to one side has a side effect on the other, e.g.
//
//   requires { xyzzy == (xyzzy + 3) }
//
// This has to be guarded against by reevaluating the expression.
//
// At present this code only copes with equality, not inequality.

static bool
infer_handle_equal_bool(CdlTransaction transaction, CdlExpression expr, unsigned int lhs, unsigned int rhs, bool goal, int level)
{
    CYG_REPORT_FUNCNAMETYPE("infer_handle_equal_bool", "result %d");
    CYG_REPORT_FUNCARG4XV(transaction, expr, lhs, rhs);
    CYG_PRECONDITION_CLASSC(transaction);
    CYG_PRECONDITION_CLASSC(expr);
    CYG_PRECONDITIONC(lhs != rhs);

    bool result = false;
    if (goal) {
        
        // We need two sub-transactions, The lhs_transaction is for evaluating the lhs
        // and trying to update the rhs. 
        CdlTransaction  lhs_transaction = transaction->make(transaction->get_conflict());
        bool            lhs_result = false;
        try {
            CdlSimpleValue  lhs_value;
            CdlEvalContext  lhs_context(lhs_transaction);
            expr->eval_subexpression(lhs_context, lhs, lhs_value);
            lhs_result = CdlInfer::subexpr_value(lhs_transaction, expr, rhs, lhs_value, level);
            if (lhs_result) {
                CdlSimpleValue check;
                expr->eval_subexpression(lhs_context, lhs, check);
                if (lhs_value != check) {
                    lhs_result = false;
                }
            }
        } catch (...) {
            lhs_result = false;
        }
        
        CdlTransaction  rhs_transaction = transaction->make(transaction->get_conflict());
        bool            rhs_result = false;
        try {
            CdlSimpleValue  rhs_value;
            CdlEvalContext  rhs_context(rhs_transaction);
            expr->eval_subexpression(rhs_context, rhs, rhs_value);
            rhs_result = CdlInfer::subexpr_value(rhs_transaction, expr, lhs, rhs_value, level);
            if (rhs_result) {
                CdlSimpleValue check;
                expr->eval_subexpression(rhs_context, rhs, check);
                if (rhs_value != check) {
                    rhs_result = false;
                }
            }
        } catch (...) {
            rhs_result = false;
        }

        result = infer_choose2(lhs_transaction, lhs_result, rhs_transaction, rhs_result);
    }
    
    CYG_REPORT_RETVAL(result);
    return result;
}

//}}}
//{{{  infer_handle_numerical_equal()           

// ----------------------------------------------------------------------------
// Handle expressions of the form A == B, where the comparison has to be
// numerical in basis. This is used primarily for operators like <=
// and >.

static bool
infer_handle_numerical_equal_bool(CdlTransaction transaction, CdlExpression expr, unsigned int lhs, unsigned int rhs, bool goal, int level)
{
    CYG_REPORT_FUNCNAMETYPE("infer_handle_numerical_equal_bool", "result %d");
    CYG_REPORT_FUNCARG4XV(transaction, expr, lhs, rhs);
    CYG_PRECONDITION_CLASSC(transaction);
    CYG_PRECONDITION_CLASSC(expr);
    CYG_PRECONDITIONC(lhs != rhs);

    bool result = false;
    if (goal) {
        
        // We need two sub-transactions, The lhs_transaction is for evaluating the lhs
        // and trying to update the rhs. 
        CdlTransaction  lhs_transaction = transaction->make(transaction->get_conflict());
        bool            lhs_result = false;
        try {
            CdlSimpleValue  lhs_value;
            CdlEvalContext  lhs_context(lhs_transaction);
            expr->eval_subexpression(lhs_context, lhs, lhs_value);
            if (lhs_value.has_integer_value() || lhs_value.has_double_value()) {
                lhs_result = CdlInfer::subexpr_value(lhs_transaction, expr, rhs, lhs_value, level);
                if (lhs_result) {
                    CdlSimpleValue check;
                    expr->eval_subexpression(lhs_context, lhs, check);
                    if (lhs_value != check) {
                        lhs_result = false;
                    }
                }
            }
        } catch (...) {
            lhs_result = false;
        }
        
        CdlTransaction  rhs_transaction = transaction->make(transaction->get_conflict());
        bool            rhs_result = false;
        try {
            CdlSimpleValue  rhs_value;
            CdlEvalContext  rhs_context(rhs_transaction);
            expr->eval_subexpression(rhs_context, rhs, rhs_value);
            if (rhs_value.has_integer_value() || rhs_value.has_double_value()) {
                rhs_result = CdlInfer::subexpr_value(rhs_transaction, expr, lhs, rhs_value, level);
                if (rhs_result) {
                    CdlSimpleValue check;
                    expr->eval_subexpression(rhs_context, rhs, check);
                    if (rhs_value != check) {
                        rhs_result = false;
                    }
                }
            }
        } catch (...) {
            rhs_result = false;
        }

        result = infer_choose2(lhs_transaction, lhs_result, rhs_transaction, rhs_result);
    }
    
    CYG_REPORT_RETVAL(result);
    return result;
}

//}}}
//{{{  CdlInfer::subexpr_bool()                 

// ----------------------------------------------------------------------------
bool
CdlInfer::subexpr_bool(CdlTransaction transaction, CdlExpression expr, unsigned int index, bool goal, int level)
{
    CYG_REPORT_FUNCNAMETYPE("CdlInfer::subexpr_bool", "result %d");
    CYG_REPORT_FUNCARG5XV(transaction, expr, index, goal, level);
    CYG_PRECONDITION_CLASSC(transaction);
    CYG_PRECONDITION_CLASSC(expr);
    CYG_PRECONDITIONC((0 <= index) && (index < expr->sub_expressions.size()));
    
    bool result = false;
    CdlSubexpression& subexpr = expr->sub_expressions[index];

    switch(subexpr.op) {
        
      case CdlExprOp_Reference :
          // The most common case. Follow the reference, and call the appropriate function.
          // Note that the reference may be unbound.
          {
              CdlNode node = expr->references[subexpr.reference_index].get_destination();
              CdlValuable valuable = 0;
              if (0 != node) {
                  valuable = dynamic_cast<CdlValuable>(node);
              }
              result = infer_handle_reference_bool(transaction, valuable, goal, level);
              break;
          }
          
      case CdlExprOp_StringConstant :
          result = infer_handle_string_constant_bool(subexpr.constants, goal);
          break;
                                                
      case CdlExprOp_IntegerConstant :
          result = infer_handle_integer_constant_bool(subexpr.constants, goal);
          break;
          
      case CdlExprOp_DoubleConstant :
          result = infer_handle_double_constant_bool(subexpr.constants, goal);
          break;