pvmjac.c

一个开源的JAVA虚拟机

      case J_OPC_iload_2:
      case J_OPC_iload_3:
      case J_OPC_lload_0:
      case J_OPC_lload_1:
      case J_OPC_lload_2:
      case J_OPC_lload_3:
      case J_OPC_fload_0:
      case J_OPC_fload_1:
      case J_OPC_fload_2:
      case J_OPC_fload_3:
      case J_OPC_dload_0:
      case J_OPC_dload_1:
      case J_OPC_dload_2:
      case J_OPC_dload_3:
      case J_OPC_aload_0:
      case J_OPC_aload_1:
      case J_OPC_aload_2:
      case J_OPC_aload_3:
      case J_OPC_iaload:
      case J_OPC_laload:
      case J_OPC_faload:
      case J_OPC_daload:
      case J_OPC_aaload:
      case J_OPC_baload:
      case J_OPC_caload:
      case J_OPC_saload:
      case J_OPC_istore:
      case J_OPC_lstore:
      case J_OPC_fstore:
      case J_OPC_dstore:
      case J_OPC_astore:
      case J_OPC_istore_0:
      case J_OPC_istore_1:
      case J_OPC_istore_2:
      case J_OPC_istore_3:
      case J_OPC_lstore_0:
      case J_OPC_lstore_1:
      case J_OPC_lstore_2:
      case J_OPC_lstore_3:
      case J_OPC_fstore_0:
      case J_OPC_fstore_1:
      case J_OPC_fstore_2:
      case J_OPC_fstore_3:
      case J_OPC_dstore_0:
      case J_OPC_dstore_1:
      case J_OPC_dstore_2:
      case J_OPC_dstore_3:
      case J_OPC_astore_0:
      case J_OPC_astore_1:
      case J_OPC_astore_2:
      case J_OPC_astore_3:
      case J_OPC_iastore:
      case J_OPC_lastore:
      case J_OPC_fastore:
      case J_OPC_dastore:
      case J_OPC_aastore:
      case J_OPC_bastore:
      case J_OPC_castore:
      case J_OPC_sastore:
      case J_OPC_pop:
      case J_OPC_pop2:
      case J_OPC_dup:
      case J_OPC_dup_x1:
      case J_OPC_dup_x2:
      case J_OPC_dup2:
      case J_OPC_dup2_x1:
      case J_OPC_dup2_x2:
      case J_OPC_swap:
      case J_OPC_iadd:
      case J_OPC_isub:
      case J_OPC_imul:
      case J_OPC_idiv:
      case J_OPC_irem:
      case J_OPC_ishl:
      case J_OPC_ishr:
      case J_OPC_iushr:
      case J_OPC_iand:
      case J_OPC_ior:
      case J_OPC_ixor:
      case J_OPC_ladd:
      case J_OPC_lsub:
      case J_OPC_lmul:
      case J_OPC_ldiv:
      case J_OPC_lrem:
      case J_OPC_land:
      case J_OPC_lor:
      case J_OPC_lxor:
      case J_OPC_fadd:
      case J_OPC_fsub:
      case J_OPC_fmul:
      case J_OPC_fdiv:
      case J_OPC_frem:
      case J_OPC_dadd:
      case J_OPC_dsub:
      case J_OPC_dmul:
      case J_OPC_ddiv:
      case J_OPC_drem:
      case J_OPC_ineg:
      case J_OPC_i2b:
      case J_OPC_i2c:
      case J_OPC_i2s:
      case J_OPC_lneg:
      case J_OPC_fneg:
      case J_OPC_dneg:
      case J_OPC_lshl:
      case J_OPC_lshr:
      case J_OPC_lushr:
      case J_OPC_iinc:
      case J_OPC_i2l:
      case J_OPC_i2f:
      case J_OPC_i2d:
      case J_OPC_l2i:
      case J_OPC_l2f:
      case J_OPC_l2d:
      case J_OPC_f2i:
      case J_OPC_f2l:
      case J_OPC_f2d:
      case J_OPC_d2i:
      case J_OPC_d2l:
      case J_OPC_d2f:
      case J_OPC_lcmp:
      case J_OPC_fcmpl:
      case J_OPC_fcmpg:
      case J_OPC_dcmpl:
      case J_OPC_dcmpg:
      case J_OPC_getfield:
      case J_OPC_getstatic:
      case J_OPC_putstatic:
      case J_OPC_putfield:
      case J_OPC_invokestatic:
      case J_OPC_invokevirtual:
      case J_OPC_invokespecial:
      case J_OPC_invokeinterface:
      case J_OPC_new:
      case J_OPC_newarray:
      case J_OPC_anewarray:
      case J_OPC_arraylength:
      case J_OPC_checkcast:
      case J_OPC_instanceof:
      case J_OPC_monitorenter:
      case J_OPC_monitorexit:
      case J_OPC_multianewarray:
      COMMON_non_branching:
	k = j + pre_instr_len(instr);
	if (! jac_compute_state_meet(arena, states + k, S, &flag))
	  return false;
	if (! jac_compute_handler_meet(arena, attr, states, k, &flag))
	  return false;
	break;
      case J_OPC_goto:
	k = j + pre_instr_branch_offset(instr);
      COMMON_unconditional_branching:
	if (! jac_compute_state_meet(arena, states + k, S, &flag))
	  return false;
	if (! jac_compute_handler_meet(arena, attr, states, k, &flag))
	  return false;
	break;
      case J_OPC_goto_w:
	k = j + pre_instr_branch_wide_offset(instr);
	goto COMMON_unconditional_branching;
      case J_OPC_ifeq:
      case J_OPC_ifne:
      case J_OPC_iflt:
      case J_OPC_ifge:
      case J_OPC_ifgt:
      case J_OPC_ifle:
      case J_OPC_if_icmpeq:
      case J_OPC_if_icmpne:
      case J_OPC_if_icmplt:
      case J_OPC_if_icmpge:
      case J_OPC_if_icmpgt:
      case J_OPC_if_icmple:
      case J_OPC_if_acmpeq:
      case J_OPC_if_acmpne:
      case J_OPC_ifnull:
      case J_OPC_ifnonnull:
	k = j + pre_instr_len(instr);
	if (! jac_compute_state_meet(arena, states + k, S, &flag))
	  return false;
	if (! jac_compute_handler_meet(arena, attr, states, k, &flag))
	  return false;
	k = j + pre_instr_branch_offset(instr);
	if (! jac_compute_state_meet(arena, states + k, S, &flag))
	  return false;
	if (! jac_compute_handler_meet(arena, attr, states, k, &flag))
	  return false;
	break;
      case J_OPC_tableswitch:
	{
	  ji4 i, low, high;
	  k = j + pre_instr_tableswitch_default_offset(instr);
	  if (! jac_compute_state_meet(arena, states + k, S, &flag))
	    return false;
	  if (! jac_compute_handler_meet(arena, attr, states, k, &flag))
	    return false;
	  low = pre_instr_tableswitch_low(instr);
	  high = pre_instr_tableswitch_high(instr);
	  i = pre_instr_tableswitch_low(instr);
	  for (;;) {
	    k = j + pre_instr_tableswitch_offset(instr, i);
	    if (! jac_compute_state_meet(arena, states + k, S, &flag))
	      return false;
	    if (! jac_compute_handler_meet(arena, attr, states, k, &flag))
	      return false;
	    if (i == high)
	      break;
	    i++;
	  }
	}
	break;
      case J_OPC_lookupswitch:
	{
	  ji4 i, npairs;
	  k = j + pre_instr_lookupswitch_default_offset(instr);
	  if (! jac_compute_state_meet(arena, states + k, S, &flag))
	    return false;
	  if (! jac_compute_handler_meet(arena, attr, states, k, &flag))
	    return false;
	  npairs = pre_instr_lookupswitch_npairs(instr);
	  for (i = 0; i < npairs; i++) {
	    k = j + pre_instr_lookupswitch_offset(instr, i);
	    if (! jac_compute_state_meet(arena, states + k, S, &flag))
	      return false;
	    if (! jac_compute_handler_meet(arena, attr, states, k, &flag))
	      return false;
	  }
	}
	break;
      case J_OPC_jsr_w:
	k = j + pre_instr_branch_wide_offset(instr);
	goto COMMON_jsr_branching;
      case J_OPC_jsr:
	k = j + pre_instr_branch_offset(instr);
      COMMON_jsr_branching:
	{
	  if (! jac_compute_state_meet(arena, states + k, S, &flag))
	    return false;
	  if (! jac_compute_handler_meet(arena, attr, states, k, &flag))
	    return false;
	  const PREState *target = pre_analysis_state(analysis, k);
	  const void *type = pre_state_stack_top(target, 0);
	  const PRERoutine *routine = pre_type_address_routine(type);
	  ju4 ret = pre_routine_ret(routine);
	  k = j + pre_instr_len(instr);
	  if (! jac_compute_routine_meet(arena, states + k, states[j],
					 states[ret], routine, &flag))
	    return false;
	  if (! jac_compute_handler_meet(arena, attr, states, k, &flag))
	    return false;
	}
	break;
      case J_OPC_ret:
	index = pre_instr_locals_index(instr);
      COMMON_ret_branching:
	{
	  const PREState *from = pre_analysis_state(analysis, j);
	  const void *type = pre_state_locals_read(from, index);
	  const PRERoutine *routine = pre_type_address_routine(type);
	  const PRECallSites *sites;
	  for (sites = pre_routine_call_sites(routine);
	       sites != 0;
	       sites = pre_call_sites_rest(sites)) {
	    ju4 jsr_addr = pre_call_sites_first(sites);
	    if (states[jsr_addr] != 0) {
	      k = jsr_addr + pre_instr_len(pre_attribute_code_code(attr,
								   jsr_addr));
	      if (! jac_compute_routine_meet(arena, states + k,
					     states[jsr_addr], states[j],
					     routine, &flag))
		return false;
	      if (! jac_compute_handler_meet(arena, attr, states, k, &flag))
		return false;
	    }
	  }
	}
	break;
      case J_OPC_ireturn:
      case J_OPC_lreturn:
      case J_OPC_freturn:
      case J_OPC_dreturn:
      case J_OPC_areturn:
      case J_OPC_return:
      case J_OPC_athrow:
	/* no natural successor */
	break;
      case J_OPC_wide:
	switch (pre_instr_locals_wide_widened_opcode(instr)) {
	case J_OPC_iload:
	case J_OPC_fload:
	case J_OPC_aload:
	case J_OPC_lload:
	case J_OPC_dload:
	case J_OPC_istore:
	case J_OPC_fstore:
	case J_OPC_astore:
	case J_OPC_lstore:
	case J_OPC_dstore:
	case J_OPC_iinc:
	  goto COMMON_non_branching;
	case J_OPC_ret:
	  index = pre_instr_locals_wide_index(instr);
	  goto COMMON_ret_branching;
	default:
	  j_assert_not_reached();
	}
      default:
	j_assert_not_reached();
      } /* switch */


    } /* for */
  } /* while */

  return true;
}

bool
jac_typecheck_method(const PREAnalysis *analysis,
		     const struct jac_commitments *commitments) {
  const PREClassFile *classfile = pre_analysis_classfile(analysis);
  ju2 method_index = pre_analysis_method_index(analysis);
  const PREMethod *method = pre_classfile_method(classfile, method_index);
  const void *attr = pre_method_code(method);
  ju4 code_length = pre_attribute_code_length(attr);
  ju2 max_locals = pre_attribute_code_max_locals(attr);
  ju2 max_stack = pre_attribute_code_max_stack(attr);
#ifdef JAC_PVM_DEBUG
  fprintf(stderr, "================\nTypechecking method %s.%s%s\n",
	  pre_classfile_this_class_name(classfile),
	  pre_classfile_method_name(classfile, method_index),
	  pre_classfile_method_descriptor(classfile, method_index));
#endif
  /* Create arena for holding temporary data struct */
  JArena *arena;
  arena = j_arena_new();
  if (arena == 0)
    return false;
  /* Create array of type states*/
  JACState **states =
    j_arena_alloc_array(arena, code_length, sizeof(JACState *));
  if (states == 0)
    goto ErrorExit;
  /* Clear all state pointers */
  j_memset(states, 0, code_length * sizeof(JACState *));
  /* Create first state */
  states[0] = jac_allocate_state(arena, max_locals, max_stack);
  if (states[0] == 0)
    goto ErrorExit;
  /* Initialize first state */
  jac_initialize_first_state(analysis, commitments, states[0]);
#ifdef JAC_PVM_DEBUG
  fprintf(stderr, "First state:\n");
  jac_print_state(stderr, states[0]);
#endif
  /* Run dataflow analysis */
#ifdef JAC_PVM_DEBUG
  fprintf(stderr, "Dataflow analysis begins:\n");
#endif
  if (! jac_run_flow_analysis(arena, analysis, commitments, states))
    goto ErrorExit;
  /* Validation succeeds */
#ifdef JAC_PVM_DEBUG
  fprintf(stderr, "Dataflow analysis completed successfully\n");
#endif
  /* Return results */
  j_arena_delete(arena);
  return true;
 ErrorExit:  
  j_arena_delete(arena);
#ifdef JAC_PVM_DEBUG
  fprintf(stderr, "Typechecking failed\n");
#endif
  return false;
}

bool
jac_typecheck_methods(const PREClassFile *classfile,
		      const PREAnalysis **analyses,
		      const struct jac_commitments *commitments) {
  const PREConstantPool *constant_pool =
    pre_classfile_constant_pool(classfile);
  ju2 methods_count = pre_classfile_methods_count(classfile);
  ju2 i;
  if (commitments == 0) {
    return true;
  } /* if */
  if (commitments->constant_annotations == 0) {
    if (commitments->method_annotations != 0) {
      for (i = 0; i < methods_count; i++) {
	if (commitments->method_annotations[i] != 0) {
	  if (analyses[i] != 0 &&
	      ! jac_typecheck_method(analyses[i], commitments))
	    return false;
	} /* if */
      } /* for */
    } /* if */
  } else {
    for (i = 0; i < methods_count; i++) {
      if (analyses[i] != 0 &&
	  ! jac_typecheck_method(analyses[i], commitments))
	return false;
    } /* for */
  } /* if */
  return true;
}

const PREVI *
jac_formulate_obligations(JArena *arena,
			  const PREClassFile *classfile,
			  struct jac_commitments *commitments) {
  /* Create temporary arena */
  JArena *tmp;
  tmp = j_arena_new();
  if (tmp == 0)
    return 0;
  /* Create working verification environment */
  PREWorkingVI *vi = pre_working_vi_new(tmp, classfile);
  if (vi == 0)
    goto ErrorExit;
  /* Post debugging obligation */
#ifdef JAC_PVM_DEBUG
  {
    PREArgument arg;
    pre_argument_set_this(&arg);
    if (! pre_working_vi_formulate_class_obligation(vi, JAC_PRED_debug_commitments, 1, &arg))
      goto ErrorExit;
  }
#endif
  /* Post method override safety obligation */
 {
   PREArgument arg;
   pre_argument_set_this(&arg);
   if (! pre_working_vi_formulate_class_obligation(vi, JAC_PRED_safe_method_override, 1, &arg))
     goto ErrorExit;
 }
  /* Post import safety obligations */
  const PREConstantPool *constant_pool =
    pre_classfile_constant_pool(classfile);
  ju2 constant_pool_count = pre_constant_pool_count(constant_pool);
  ju2 i;
  for (i = 1; i < constant_pool_count; i++) {
    const void *cp = pre_constant_pool_entry(constant_pool, i);
    if (cp == 0)
      continue;
    switch (pre_cp_tag(cp)) {
    case J_CONSTANT_Fieldref:
      {
	PREArgument arg[2];
	pre_argument_set_constant(&(arg[0]), i);
	ju2 index = jac_get_constant_annotation_index(commitments, i);
	if (index != 0)
	  pre_argument_set_constant(&(arg[1]), index);
	else
	  pre_argument_set_global_constant(&(arg[1]), 0);
	if (! pre_working_vi_formulate_constant_obligation(vi, i, JAC_PRED_safe_field_import, 2, &(arg[0])))
	  goto ErrorExit;
      }
      break;
    case J_CONSTANT_Methodref:
    case J_CONSTANT_InterfaceMethodref:
      {
	PREArgument arg[2];
	pre_argument_set_constant(&(arg[0]), i);
	ju2 index = jac_get_constant_annotation_index(commitments, i);
	if (index != 0)
	  pre_argument_set_constant(&(arg[1]), index);
	else
	  pre_argument_set_global_constant(&(arg[1]), 0);
	if (! pre_working_vi_formulate_constant_obligation(vi, i, JAC_PRED_safe_method_import, 2, &(arg[0])))
	  goto ErrorExit;
      }
      break;
    }
  }
  /* Deposit result in a permenant data structure */ 
  const PREVI *V = pre_vi_new(arena, vi, commitments);
  if (V == 0)
    goto ErrorExit;
  /* Return result */
  j_arena_delete(tmp);
  return V;
 ErrorExit:
  j_arena_delete(tmp);
  return 0;
}

const PREVI *
jac_pvm_verify(JArena *arena,
	       const PREClassFile *classfile,
	       const PREAnalysis **analyses) {
  /* Mark state of arena */
  const void *check_point;
  check_point = j_arena_check_point(arena);
  /* Parse commitments */
  struct jac_commitments *commitments;
  const void *attr = jac_find_jac_attribute(classfile);
  if (attr == 0) {
    /* No commitments are attached */
    commitments = 0;
  } else {
    /* Parse commitments */
    if (! jac_parse_jac_attribute(arena, classfile, attr, &commitments))
      return 0;
  }
  /* Perform typechecking for the methods */
  if (! jac_typecheck_methods(classfile, analyses, commitments))
    goto ErrorExit;
  /* Formulate obligations */
  const PREVI *E = jac_formulate_obligations(arena, classfile, commitments);
  if (E == 0)
    goto ErrorExit;
  /* Return result */
  return E;
 ErrorExit:
  j_arena_free(arena, check_point);
  return 0;
}

pvm_profile_t pvm_profile = {
  "JAC",
  &jac_pvm_init,
  &jac_pvm_finish,
  &jac_pvm_verify
};