Project

General

Profile

Actions
Copy link

Bug #6159

closed

Checker produces the incorrect constraint for a memory access structure

Added by Alexander Kamkin over 9 years ago. Updated over 9 years ago.

Status:
Closed
Priority:
High
Assignee:
Alexander Kamkin
Category:
MMU Plugin
Target version:
2.2
Start date:
07/08/2015
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:
2.2.9

Description

Executions:

  1. LOAD, BYTE, isMapped=1, DTLB.Event=MISS, JTLB.Event=HIT, VA[12]=0, G=1, V=1, D=1, isHiMem=0, C[0:1]=2, STOP,
  2. LOAD, BYTE, isMapped=1, DTLB.Event=MISS, JTLB.Event=HIT, VA[12]=0, G=1, V=1, D=1, isHiMem=0, C[0:1]=2, STOP,

Dependencies:

  1. VAAddrNotEqualPAAddrNotEqualDTLBTagReplaced

Result:

  1. UNSAT

Constraint:

  1. [isMapped$0$[0, 0] = 1],
  2. [VA$0$[12, 12] = 0],
  3. [D$0$[0, 0] = D0$0$[0, 0]],
  4. [V$0$[0, 0] = V0$0$[0, 0]],
  5. [PFN$0$[0, 23] = PFN0$0$[0, 23]],
  6. [C$0$[0, 1] = C0$0$[0, 1]],
  7. [C$0$[2, 2] = C0$0$[2, 2]],
  8. [G$0$[0, 0] = 1],
  9. [V$0$[0, 0] = 1],
  10. [D$0$[0, 0] = 1],
  11. [isHiMem$0$[0, 0] = 0],
  12. [PA$0$[0, 11] = VA$0$[0, 11]],
  13. [PA$0$[12, 35] = PFN$0$[0, 23]],
  14. [C$0$[0, 1] = 2],
  15. [isMapped$1$[0, 0] = 1],
  16. [VA$1$[12, 12] = 0],
  17. [D$1$[0, 0] = D0$1$[0, 0]],
  18. [V$1$[0, 0] = V0$1$[0, 0]],
  19. [PFN$1$[0, 23] = PFN0$1$[0, 23]],
  20. [C$1$[0, 1] = C0$1$[0, 1]],
  21. [C$1$[2, 2] = C0$1$[2, 2]],
  22. [G$1$[0, 0] = 1],
  23. [V$1$[0, 0] = 1],
  24. [D$1$[0, 0] = 1],
  25. [isHiMem$1$[0, 0] = 0],
  26. [PA$1$[0, 11] = VA$1$[0, 11]],
  27. [PA$1$[12, 35] = PFN$1$[0, 23]],
  28. [C$1$[0, 1] = 2],
  29. [VA$0$[0, 11] = VA$1$[0, 11]],
  30. [VA$0$[12, 12] = VA$1$[12, 12]],
  31. [VA$0$[40, 63] = VA$1$[40, 63]],
  32. [PA$0$[0, 11] = PA$1$[0, 11]],
  33. [PA$0$[12, 35] = PA$1$[12, 35]],
  34. [VA$0$[13, 39] = VA$1$[13, 39]],
  35. [VA$0$[13, 39] != VA$1$[13, 39]]
    1. UNSAT
Actions
Copy link
 #1

Updated by Alexander Kamkin over 9 years ago

  • Description updated (diff)
Actions
Copy link
 #2

Updated by Alexander Kamkin over 9 years ago

  • Status changed from New to Resolved

Refactoring led to a typo:

  public static MmuCondition neq(final MmuExpression expression) {
    return new MmuCondition(MmuConditionAtom.eq(expression)); // eq -> neq
  }
Actions
Copy link
 #3

Updated by Andrei Tatarnikov over 9 years ago

  • Status changed from Resolved to Closed
  • Published in build set to 2.2.9
Actions
Copy link

Also available in: Atom PDF