• 如果您觉得本站非常有看点,那么赶紧使用Ctrl+D 收藏吧

Java BitvectorOperator类的典型用法和代码示例

java 3次浏览

本文整理汇总了Java中gov.nasa.jpf.constraints.expressions.BitvectorOperator的典型用法代码示例。如果您正苦于以下问题:Java BitvectorOperator类的具体用法?Java BitvectorOperator怎么用?Java BitvectorOperator使用的例子?那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。

BitvectorOperator类属于gov.nasa.jpf.constraints.expressions包,在下文中一共展示了BitvectorOperator类的17个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的Java代码示例。

示例1: execute

点赞 3

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
@Override
 public Instruction execute (ThreadInfo ti) {
	StackFrame sf = ti.getTopFrame();

   if (sf.getOperandAttr(1) == null && sf.getOperandAttr(3) == null) {
     return super.execute(ti);
   }
   
  ConcolicUtil.Pair<Long> right = ConcolicUtil.popLong(sf);
  ConcolicUtil.Pair<Long> left = ConcolicUtil.popLong(sf);

  BitvectorExpression<Long> symb = BitvectorExpression.create(
           left.symb, BitvectorOperator.XOR, right.symb);    
   
   long conc = left.conc ^ right.conc;    
   
   ConcolicUtil.Pair<Long> result = new ConcolicUtil.Pair<Long>(conc, symb);
   ConcolicUtil.pushLong(result, sf);

   if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute LXOR: " + result);		
   return getNext(ti);
}
 

开发者ID:psycopaths,
项目名称:jdart,
代码行数:23,
代码来源:LXOR.java

示例2: execute

点赞 3

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
@Override
public Instruction execute (ThreadInfo ti) {
StackFrame sf = ti.getTopFrame();

if(sf.getOperandAttr(0) ==null && sf.getOperandAttr(1)==null) {
	return super.execute(ti); 
  } 
  
 ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
 ConcolicUtil.Pair<Integer> left = ConcolicUtil.popInt(sf);

 BitvectorExpression<Integer> symb = BitvectorExpression.create(
          left.symb, BitvectorOperator.SHIFTUR, right.symb);    
  
  int conc = left.conc >>> right.conc;    
  
  ConcolicUtil.Pair<Integer> result = new ConcolicUtil.Pair<Integer>(conc, symb);
  ConcolicUtil.pushInt(result, sf);

  if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute IUSHR: " + result);		
  return getNext(ti);
}
 

开发者ID:psycopaths,
项目名称:jdart,
代码行数:23,
代码来源:IUSHR.java

示例3: execute

点赞 3

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
@Override
 public Instruction execute (ThreadInfo ti) {
	StackFrame sf = ti.getTopFrame();

   if (sf.getOperandAttr(1) == null && sf.getOperandAttr(3) == null) {
     return super.execute(ti);
   }
   
  ConcolicUtil.Pair<Long> right = ConcolicUtil.popLong(sf);
  ConcolicUtil.Pair<Long> left = ConcolicUtil.popLong(sf);

  BitvectorExpression<Long> symb = BitvectorExpression.create(
           left.symb, BitvectorOperator.OR, right.symb);    
   
   long conc = left.conc | right.conc;    
   
   ConcolicUtil.Pair<Long> result = new ConcolicUtil.Pair<Long>(conc, symb);
   ConcolicUtil.pushLong(result, sf);

   if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute LOR: " + result);		
   return getNext(ti);
}
 

开发者ID:psycopaths,
项目名称:jdart,
代码行数:23,
代码来源:LOR.java

示例4: execute

点赞 3

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
@Override
public Instruction execute (ThreadInfo ti) {
StackFrame sf = ti.getTopFrame();

if(sf.getOperandAttr(0) ==null && sf.getOperandAttr(1)==null) {
	return super.execute(ti); 
  } 
  
 ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
 ConcolicUtil.Pair<Integer> left = ConcolicUtil.popInt(sf);

  BitvectorExpression<Integer> symb = BitvectorExpression.create(
          left.symb, BitvectorOperator.OR, right.symb);    
  
  int conc = left.conc | right.conc;    
  
  ConcolicUtil.Pair<Integer> result = new ConcolicUtil.Pair<Integer>(conc, symb);
  ConcolicUtil.pushInt(result, sf);

  if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute IOR: " + result);		
  return getNext(ti);
}
 

开发者ID:psycopaths,
项目名称:jdart,
代码行数:23,
代码来源:IOR.java

示例5: execute

点赞 3

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
@Override
 public Instruction execute (ThreadInfo ti) {
	StackFrame sf = ti.getTopFrame();

   if (sf.getOperandAttr(1) == null && sf.getOperandAttr(3) == null) {
     return super.execute(ti);
   }
   
  ConcolicUtil.Pair<Long> right = ConcolicUtil.popLong(sf);
  ConcolicUtil.Pair<Long> left = ConcolicUtil.popLong(sf);

  BitvectorExpression<Long> symb = BitvectorExpression.create(
           left.symb, BitvectorOperator.AND, right.symb);    
   
   long conc = left.conc & right.conc;    
   
   ConcolicUtil.Pair<Long> result = new ConcolicUtil.Pair<Long>(conc, symb);
   ConcolicUtil.pushLong(result, sf);

   if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute LAND: " + result);		
   return getNext(ti);
}
 

开发者ID:psycopaths,
项目名称:jdart,
代码行数:23,
代码来源:LAND.java

示例6: execute

点赞 3

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
@Override
 public Instruction execute (ThreadInfo ti) {
	StackFrame sf = ti.getTopFrame();

   if (sf.getOperandAttr(0) == null && sf.getOperandAttr(2) == null) {
     return super.execute(ti);
   }
   
  ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
  ConcolicUtil.Pair<Long> left = ConcolicUtil.popLong(sf);

  BitvectorExpression<Long> symb = BitvectorExpression.create(
           left.symb, BitvectorOperator.SHIFTUR, new CastExpression<>(right.symb, BuiltinTypes.SINT64, NumericCastOperation.TO_SINT64));    
   
   long conc = left.conc >>> right.conc;    
   
   ConcolicUtil.Pair<Long> result = new ConcolicUtil.Pair<Long>(conc, symb);
   ConcolicUtil.pushLong(result, sf);

   if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute LUSHR: " + result);		
   return getNext(ti);
}
 

开发者ID:psycopaths,
项目名称:jdart,
代码行数:23,
代码来源:LUSHR.java

示例7: execute

点赞 3

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
@Override
public Instruction execute (ThreadInfo ti) {
StackFrame sf = ti.getTopFrame();

if(sf.getOperandAttr(0) ==null && sf.getOperandAttr(1)==null) {
	return super.execute(ti); 
  } 
  
 ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
 ConcolicUtil.Pair<Integer> left = ConcolicUtil.popInt(sf);

 BitvectorExpression<Integer> symb = BitvectorExpression.create(
          left.symb, BitvectorOperator.SHIFTL, right.symb);    
  
  int conc = left.conc << right.conc;    
  
  ConcolicUtil.Pair<Integer> result = new ConcolicUtil.Pair<Integer>(conc, symb);
  ConcolicUtil.pushInt(result, sf);

  if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute ISHL: " + result);		
  return getNext(ti);
}
 

开发者ID:psycopaths,
项目名称:jdart,
代码行数:23,
代码来源:ISHL.java

示例8: execute

点赞 3

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
@Override
public Instruction execute (ThreadInfo ti) {
StackFrame sf = ti.getTopFrame();

if(sf.getOperandAttr(0) ==null && sf.getOperandAttr(1)==null) {
	return super.execute(ti); 
  } 
  
 ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
 ConcolicUtil.Pair<Integer> left = ConcolicUtil.popInt(sf);

 BitvectorExpression<Integer> symb = BitvectorExpression.create(
          left.symb, BitvectorOperator.SHIFTR, right.symb);    
  
  int conc = left.conc >> right.conc;    
  
  ConcolicUtil.Pair<Integer> result = new ConcolicUtil.Pair<Integer>(conc, symb);
  ConcolicUtil.pushInt(result, sf);

  if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute ISHR: " + result);		
  return getNext(ti);
}
 

开发者ID:psycopaths,
项目名称:jdart,
代码行数:23,
代码来源:ISHR.java

示例9: execute

点赞 3

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
@Override
public Instruction execute (ThreadInfo ti) {
StackFrame sf = ti.getTopFrame();

if(sf.getOperandAttr(0) ==null && sf.getOperandAttr(1)==null) {
	return super.execute(ti); 
  } 
  
 ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
 ConcolicUtil.Pair<Integer> left = ConcolicUtil.popInt(sf);

 BitvectorExpression<Integer> symb = BitvectorExpression.create(
          left.symb, BitvectorOperator.XOR, right.symb);    
  
  int conc = left.conc ^ right.conc;    
  
  ConcolicUtil.Pair<Integer> result = new ConcolicUtil.Pair<Integer>(conc, symb);
  ConcolicUtil.pushInt(result, sf);

  if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute IXOR: " + result);		
  return getNext(ti);
}
 

开发者ID:psycopaths,
项目名称:jdart,
代码行数:23,
代码来源:IXOR.java

示例10: execute

点赞 3

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
@Override
 public Instruction execute (ThreadInfo ti) {
	StackFrame sf = ti.getTopFrame();

   if (sf.getOperandAttr(0) == null && sf.getOperandAttr(2) == null) {
     return super.execute(ti);
   }
   
  ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
  ConcolicUtil.Pair<Long> left = ConcolicUtil.popLong(sf);

  BitvectorExpression<Long> symb = BitvectorExpression.create(
           left.symb, BitvectorOperator.SHIFTL, new CastExpression<>(right.symb, BuiltinTypes.SINT64, NumericCastOperation.TO_SINT64));    
   
   long conc = left.conc << right.conc;    
   
   ConcolicUtil.Pair<Long> result = new ConcolicUtil.Pair<Long>(conc, symb);
   ConcolicUtil.pushLong(result, sf);

   if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute LSHL: " + result);		
   return getNext(ti);
}
 

开发者ID:psycopaths,
项目名称:jdart,
代码行数:23,
代码来源:LSHL.java

示例11: execute

点赞 3

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
@Override
public Instruction execute (ThreadInfo ti) {
StackFrame sf = ti.getTopFrame();

if(sf.getOperandAttr(0) ==null && sf.getOperandAttr(1)==null) {
	return super.execute(ti); 
  } 
  
 ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
 ConcolicUtil.Pair<Integer> left = ConcolicUtil.popInt(sf);

  BitvectorExpression<Integer> symb = BitvectorExpression.create(
          left.symb, BitvectorOperator.AND, right.symb);    
  
  int conc = left.conc & right.conc;    
  
  ConcolicUtil.Pair<Integer> result = new ConcolicUtil.Pair<Integer>(conc, symb);
  ConcolicUtil.pushInt(result, sf);

  if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute IAND: " + result);		
  return getNext(ti);
}
 

开发者ID:psycopaths,
项目名称:jdart,
代码行数:23,
代码来源:IAND.java

示例12: execute

点赞 3

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
@Override
 public Instruction execute (ThreadInfo ti) {
	StackFrame sf = ti.getTopFrame();

   if (sf.getOperandAttr(0) == null && sf.getOperandAttr(2) == null) {
     return super.execute(ti);
   }
   
  ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
  ConcolicUtil.Pair<Long> left = ConcolicUtil.popLong(sf);

  BitvectorExpression<Long> symb = BitvectorExpression.create(
           left.symb, BitvectorOperator.SHIFTR, new CastExpression<>(right.symb, BuiltinTypes.SINT64, NumericCastOperation.TO_SINT64));    
   
   long conc = left.conc >> right.conc;    
   
   ConcolicUtil.Pair<Long> result = new ConcolicUtil.Pair<Long>(conc, symb);
   ConcolicUtil.pushLong(result, sf);

   if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute LSHR: " + result);		
   return getNext(ti);
}
 

开发者ID:psycopaths,
项目名称:jdart,
代码行数:23,
代码来源:LSHR.java

示例13: parseBitVectorExpression

点赞 3

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
private BitvectorExpression parseBitVectorExpression() {
  currentLine = currentLine.substring(2);
  Expression left = parseNextExpression();
  currentLine = currentLine.substring(1);
  BitvectorOperator operator;
  if (nextTokenIs(TransitionEncoding.bitVectorOperator)) {
    currentLine = currentLine.substring(1);
    int operatorEnde = currentLine.indexOf(";");
    String readOperator = currentLine.substring(0, operatorEnde);
    operator = BitvectorOperator.valueOf(readOperator);
    currentLine = currentLine.substring(operatorEnde + 1);
  } else {
    throw new IllegalStateException(
            "The next token must be an BitVectorOperator");
  }
  currentLine = currentLine.substring(1);
  Expression right = parseNextExpression();
  return new BitvectorExpression(left, operator, right);
}
 

开发者ID:psycopaths,
项目名称:psyco,
代码行数:20,
代码来源:TransitionSystemLoader.java

示例14: parseBitVector

点赞 2

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
private Expression<Boolean> parseBitVector(Expr z3Expr, ArrayList<Expression<Boolean>> arguments) throws Exception {
  if (z3Expr.isBVAND()) {
    return new BitvectorExpression<>(arguments.get(0),
            BitvectorOperator.AND, arguments.get(1));
  }
  if (z3Expr.isBVSLT()) {
    return new NumericBooleanExpression(arguments.get(0),
            NumericComparator.LT, arguments.get(1));
  }
  if (z3Expr instanceof BitVecExpr) {
    if (z3Expr.isInt()) {
      return new Variable(BuiltinTypes.INTEGER, z3Expr.toString());
    }
    switch (z3Expr.getSort().getSortKind()) {
      case Z3_BOOL_SORT:
        return new Variable(BuiltinTypes.BOOL, z3Expr.toString());
      case Z3_INT_SORT:
        return new Variable(BuiltinTypes.INTEGER, z3Expr.toString());
      case Z3_REAL_SORT:
        return new Variable(BuiltinTypes.DECIMAL, z3Expr.toString());
      case Z3_BV_SORT:
        return new Variable(BuiltinTypes.INTEGER, z3Expr.toString());
      default:
        throw new Exception("Unknown Sort");
    }
  }
  return null;
}
 

开发者ID:psycopaths,
项目名称:jconstraints-z3,
代码行数:29,
代码来源:NativeZ3TojConstraintConverter.java

示例15: translateBitvectorOperator

点赞 2

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
public Expression<?> translateBitvectorOperator(Tree n) {
  BitvectorOperator op;
  switch(n.getType()) {
  case BVOR:
    op = BitvectorOperator.OR;
    break;
  case BVXOR:
    op = BitvectorOperator.XOR;
    break;
  case BVAND:
    op = BitvectorOperator.AND;
    break;
  case BVSHL:
    op = BitvectorOperator.SHIFTL;
    break;
  case BVSHR:
    op = BitvectorOperator.SHIFTR;
    break;
  case BVSHUR:
    op = BitvectorOperator.SHIFTUR;
    break;
  default:
    throw new UnexpectedTokenException(n, BVOR, BVXOR, BVAND, BVSHL, BVSHR, BVSHUR);
  }
  
  Expression<?> left = translateArithmeticExpression(n.getChild(0));
  Expression<?> right = translateArithmeticExpression(n.getChild(1));
  
  return BitvectorExpression.createCompatible(left, op, right, types);
}
 

开发者ID:psycopaths,
项目名称:jconstraints,
代码行数:31,
代码来源:ASTTranslator.java

示例16: convert

点赞 2

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
private String convert(BitvectorOperator operator) {
  return TransitionEncoding.bitVectorOperator + ":"
          + operator.toString() + ";";
}
 

开发者ID:psycopaths,
项目名称:psyco,
代码行数:5,
代码来源:ExpressionConverterVisitor.java

示例17: visit

点赞 2

import gov.nasa.jpf.constraints.expressions.BitvectorOperator; //导入依赖的package包/类
@Override
public <E> Object visit(BitvectorExpression<E> bv, Void data) {
	//int: xor, or, and, usr, sr, sl, cmp
	//long: xor, or, and, arithmeticshiftleft, arithmeticshiftright, logicalshiftright
	
	//TODO: Missing:
	//int: cmp
	//long: logicalshiftright
	
	Object left = visit(bv.getLeft());
	Object right = visit(bv.getRight());
	
	//Type checking
	if(!(left instanceof SymInt) && !(left instanceof SymLong))
		throw new IllegalArgumentException("First operand must be of type " + SymInt.class.getName() + " or " + SymLong.class.getName());				

	BitvectorOperator op = bv.getOperator();
	switch(op) {
	case AND:
		if(left instanceof SymInt) {
			if(right instanceof SymInt)
				return Util.and((SymInt)left, (SymInt)right);
			else
				throw new IllegalArgumentException("Second operand must be of type " + SymInt.class);
		} else if(left instanceof SymLong) {
			if(right instanceof SymLong)
				return Util.and((SymLong)left, (SymLong)right);
			else
				throw new IllegalArgumentException("Second operand must be of type " + SymLong.class);
		}
	case OR:
		if(left instanceof SymInt) {
			if(right instanceof SymInt)
				return Util.or((SymInt)left, (SymInt)right);
			else
				throw new IllegalArgumentException("Second operand must be of type " + SymInt.class);
		} else if(left instanceof SymLong) {
			if(right instanceof SymLong)
				return Util.or((SymLong)left, (SymLong)right);
			else
				throw new IllegalArgumentException("Second operand must be of type " + SymLong.class);
		}
	case XOR:
		if(left instanceof SymInt) {
			if(right instanceof SymInt)
				return Util.xor((SymInt)left, (SymInt)right);
			else
				throw new IllegalArgumentException("Second operand must be of type " + SymInt.class);
		} else if(left instanceof SymLong) {
			if(right instanceof SymLong)
				return Util.xor((SymLong)left, (SymLong)right);
			else
				throw new IllegalArgumentException("Second operand must be of type " + SymLong.class);
		}
	case SHIFTL:
		if((left instanceof SymLong) && (right instanceof SymInt))
			return Util.arithmeticShiftLeft((SymLong)left, (SymInt)right);
		else if((left instanceof SymInt) && (right instanceof SymInt))
			return Util.sl((SymInt)left, (SymInt)right);
		else
			throw new IllegalArgumentException("Incompatible types for " + BitvectorOperator.SHIFTL);
	case SHIFTR:
		if((left instanceof SymLong) && (right instanceof SymInt))
			return Util.arithmeticShiftRight((SymLong)left, (SymInt)right);
		else if((left instanceof SymInt) && (right instanceof SymInt))
			return Util.sr((SymInt)left, (SymInt)right);
		else
			throw new IllegalArgumentException("Incompatible types for " + BitvectorOperator.SHIFTR);
	case SHIFTUR:
		if((left instanceof SymInt) && (right instanceof SymInt))
			return Util.usr((SymInt)left, (SymInt)right);
		else
			throw new IllegalArgumentException("Incompatible types for " + BitvectorOperator.SHIFTUR);
	default:
		throw new UnsupportedOperationException(op.name() + " operator not supported");
	}
}
 

开发者ID:psycopaths,
项目名称:jconstraints-coral,
代码行数:78,
代码来源:CoralExpressionGenerator.java


版权声明:本文转自网络文章,转载此文章仅为分享知识,如有侵权,请联系管理员进行删除。
喜欢 (0)