Lines Matching defs:Env
317 const Formula &forceBoolValue(Environment &Env, const Expr &Expr) {
318 auto *Value = Env.get<BoolValue>(Expr);
322 Value = &Env.makeAtomicBoolValue();
323 Env.setValue(Expr, *Value);
338 Environment &Env) {
339 Env.setValue(locForHasValue(OptionalLoc), HasValueVal);
344 BoolValue *getHasValue(Environment &Env, RecordStorageLocation *OptionalLoc) {
348 auto *HasValueVal = Env.get<BoolValue>(HasValueLoc);
350 HasValueVal = &Env.makeAtomicBoolValue();
351 Env.setValue(HasValueLoc, *HasValueVal);
376 const Environment &Env) {
378 if (auto *PointerVal = dyn_cast_or_null<PointerValue>(Env.getValue(E)))
382 return Env.getStorageLocation(E);
388 getLocBehindPossiblePointer(*ObjectExpr, State.Env))) {
389 if (State.Env.getStorageLocation(*UnwrapExpr) == nullptr)
390 State.Env.setStorageLocation(*UnwrapExpr, locForValue(*OptionalLoc));
397 getLocBehindPossiblePointer(*ObjectExpr, State.Env)))
398 State.Env.setValue(
399 *UnwrapExpr, State.Env.create<PointerValue>(locForValue(*OptionalLoc)));
405 setHasValue(State.Env.getResultObjectLocation(*E),
406 State.Env.getBoolLiteralValue(true), State.Env);
413 State.Env, getImplicitObjectLocation(*CallExpr, State.Env))) {
414 State.Env.setValue(*CallExpr, *HasValueVal);
423 const Formula &(*ModelPred)(Environment &Env, const Formula &ExprVal,
425 auto &Env = State.Env;
431 getHasValue(State.Env, getImplicitObjectLocation(*MCE, State.Env));
435 Env.assume(ModelPred(Env, forceBoolValue(Env, *ValueOrPredExpr),
443 [](Environment &Env, const Formula &ExprVal,
445 auto &A = Env.arena();
461 [](Environment &Env, const Formula &ExprVal,
463 auto &A = Env.arena();
476 Loc = &State.Env.getResultObjectLocation(*E);
478 Loc = State.Env.get<RecordStorageLocation>(*E);
480 Loc = &cast<RecordStorageLocation>(State.Env.createStorageLocation(*E));
481 State.Env.setStorageLocation(*E, *Loc);
485 if (State.Env.getValue(locForHasValue(*Loc)) != nullptr)
488 setHasValue(*Loc, State.Env.makeAtomicBoolValue(), State.Env);
491 void constructOptionalValue(const Expr &E, Environment &Env,
493 RecordStorageLocation &Loc = Env.getResultObjectLocation(E);
494 setHasValue(Loc, HasValueVal, Env);
514 return State.Env.getBoolLiteralValue(true);
520 auto *Loc = State.Env.get<RecordStorageLocation>(E);
521 if (auto *HasValueVal = getHasValue(State.Env, Loc))
523 return State.Env.makeAtomicBoolValue();
532 *E, State.Env,
542 if (auto *Loc = State.Env.get<RecordStorageLocation>(*E->getArg(0))) {
543 setHasValue(*Loc, HasValueVal, State.Env);
546 State.Env.setStorageLocation(*E, *Loc);
564 transferAssignment(E, State.Env.getBoolLiteralValue(false), State);
568 Environment &Env) {
575 setHasValue(*Loc2, Env.makeAtomicBoolValue(), Env);
579 setHasValue(*Loc1, Env.makeAtomicBoolValue(), Env);
589 BoolValue *BoolVal1 = getHasValue(Env, Loc1);
591 BoolVal1 = &Env.makeAtomicBoolValue();
593 BoolValue *BoolVal2 = getHasValue(Env, Loc2);
595 BoolVal2 = &Env.makeAtomicBoolValue();
597 setHasValue(*Loc1, *BoolVal2, Env);
598 setHasValue(*Loc2, *BoolVal1, Env);
605 auto *OtherLoc = State.Env.get<RecordStorageLocation>(*E->getArg(0));
606 transferSwap(getImplicitObjectLocation(*E, State.Env), OtherLoc, State.Env);
612 auto *Arg0Loc = State.Env.get<RecordStorageLocation>(*E->getArg(0));
613 auto *Arg1Loc = State.Env.get<RecordStorageLocation>(*E->getArg(1));
614 transferSwap(Arg0Loc, Arg1Loc, State.Env);
621 if (auto *Loc = State.Env.getStorageLocation(*E->getArg(0)))
622 State.Env.setStorageLocation(*E, *Loc);
650 Environment &Env = State.Env;
651 auto &A = Env.arena();
652 auto *CmpValue = &forceBoolValue(Env, *CmpExpr);
653 auto *Arg0Loc = Env.get<RecordStorageLocation>(*CmpExpr->getArg(0));
654 if (auto *LHasVal = getHasValue(Env, Arg0Loc)) {
655 auto *Arg1Loc = Env.get<RecordStorageLocation>(*CmpExpr->getArg(1));
656 if (auto *RHasVal = getHasValue(Env, Arg1Loc)) {
659 Env.assume(evaluateEquality(A, *CmpValue, LHasVal->formula(),
666 const clang::Expr *E, Environment &Env) {
667 auto &A = Env.arena();
668 auto *CmpValue = &forceBoolValue(Env, *CmpExpr);
669 auto *Loc = Env.get<RecordStorageLocation>(*E);
670 if (auto *HasVal = getHasValue(Env, Loc)) {
673 Env.assume(
679 const clang::Expr *E, Environment &Env) {
680 auto &A = Env.arena();
681 auto *CmpValue = &forceBoolValue(Env, *CmpExpr);
682 auto *Loc = Env.get<RecordStorageLocation>(*E);
683 if (auto *HasVal = getHasValue(Env, Loc)) {
686 Env.assume(evaluateEquality(A, *CmpValue, HasVal->formula(),
728 constructOptionalValue(*E, State.Env,
729 State.Env.getBoolLiteralValue(true));
736 constructOptionalValue(*E, State.Env,
737 State.Env.getBoolLiteralValue(false));
793 getImplicitObjectLocation(*E, State.Env)) {
794 setHasValue(*Loc, State.Env.getBoolLiteralValue(true), State.Env);
804 getImplicitObjectLocation(*E, State.Env)) {
805 setHasValue(*Loc, State.Env.getBoolLiteralValue(false),
806 State.Env);
836 transferOptionalAndNulloptCmp(Cmp, Cmp->getArg(0), State.Env);
842 transferOptionalAndNulloptCmp(Cmp, Cmp->getArg(1), State.Env);
850 transferOptionalAndValueCmp(Cmp, Cmp->getArg(0), State.Env);
858 transferOptionalAndValueCmp(Cmp, Cmp->getArg(1), State.Env);
869 const Environment &Env) {
871 getLocBehindPossiblePointer(*ObjectExpr, Env))) {
872 auto *Prop = Env.getValue(locForHasValue(*OptionalLoc));
874 if (Env.proves(HasValueVal->formula()))
897 const Environment &Env) {
898 return diagnoseUnwrapCall(E->getImplicitObjectArgument(), Env);
905 const Environment &Env) {
906 return diagnoseUnwrapCall(E->getArg(0), Env);
919 Environment &Env)
922 Env.getDataflowAnalysisContext().setSyntheticFieldCallback(
934 NoopLattice &L, Environment &Env) {
935 LatticeTransferState State(L, Env);