int.go 10 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477
  1. package vrp
  2. import (
  3. "fmt"
  4. "go/token"
  5. "go/types"
  6. "math/big"
  7. "honnef.co/go/tools/ssa"
  8. )
  9. type Zs []Z
  10. func (zs Zs) Len() int {
  11. return len(zs)
  12. }
  13. func (zs Zs) Less(i int, j int) bool {
  14. return zs[i].Cmp(zs[j]) == -1
  15. }
  16. func (zs Zs) Swap(i int, j int) {
  17. zs[i], zs[j] = zs[j], zs[i]
  18. }
  19. type Z struct {
  20. infinity int8
  21. integer *big.Int
  22. }
  23. func NewZ(n int64) Z {
  24. return NewBigZ(big.NewInt(n))
  25. }
  26. func NewBigZ(n *big.Int) Z {
  27. return Z{integer: n}
  28. }
  29. func (z1 Z) Infinite() bool {
  30. return z1.infinity != 0
  31. }
  32. func (z1 Z) Add(z2 Z) Z {
  33. if z2.Sign() == -1 {
  34. return z1.Sub(z2.Negate())
  35. }
  36. if z1 == NInfinity {
  37. return NInfinity
  38. }
  39. if z1 == PInfinity {
  40. return PInfinity
  41. }
  42. if z2 == PInfinity {
  43. return PInfinity
  44. }
  45. if !z1.Infinite() && !z2.Infinite() {
  46. n := &big.Int{}
  47. n.Add(z1.integer, z2.integer)
  48. return NewBigZ(n)
  49. }
  50. panic(fmt.Sprintf("%s + %s is not defined", z1, z2))
  51. }
  52. func (z1 Z) Sub(z2 Z) Z {
  53. if z2.Sign() == -1 {
  54. return z1.Add(z2.Negate())
  55. }
  56. if !z1.Infinite() && !z2.Infinite() {
  57. n := &big.Int{}
  58. n.Sub(z1.integer, z2.integer)
  59. return NewBigZ(n)
  60. }
  61. if z1 != PInfinity && z2 == PInfinity {
  62. return NInfinity
  63. }
  64. if z1.Infinite() && !z2.Infinite() {
  65. return Z{infinity: z1.infinity}
  66. }
  67. if z1 == PInfinity && z2 == PInfinity {
  68. return PInfinity
  69. }
  70. panic(fmt.Sprintf("%s - %s is not defined", z1, z2))
  71. }
  72. func (z1 Z) Mul(z2 Z) Z {
  73. if (z1.integer != nil && z1.integer.Sign() == 0) ||
  74. (z2.integer != nil && z2.integer.Sign() == 0) {
  75. return NewBigZ(&big.Int{})
  76. }
  77. if z1.infinity != 0 || z2.infinity != 0 {
  78. return Z{infinity: int8(z1.Sign() * z2.Sign())}
  79. }
  80. n := &big.Int{}
  81. n.Mul(z1.integer, z2.integer)
  82. return NewBigZ(n)
  83. }
  84. func (z1 Z) Negate() Z {
  85. if z1.infinity == 1 {
  86. return NInfinity
  87. }
  88. if z1.infinity == -1 {
  89. return PInfinity
  90. }
  91. n := &big.Int{}
  92. n.Neg(z1.integer)
  93. return NewBigZ(n)
  94. }
  95. func (z1 Z) Sign() int {
  96. if z1.infinity != 0 {
  97. return int(z1.infinity)
  98. }
  99. return z1.integer.Sign()
  100. }
  101. func (z1 Z) String() string {
  102. if z1 == NInfinity {
  103. return "-∞"
  104. }
  105. if z1 == PInfinity {
  106. return "∞"
  107. }
  108. return fmt.Sprintf("%d", z1.integer)
  109. }
  110. func (z1 Z) Cmp(z2 Z) int {
  111. if z1.infinity == z2.infinity && z1.infinity != 0 {
  112. return 0
  113. }
  114. if z1 == PInfinity {
  115. return 1
  116. }
  117. if z1 == NInfinity {
  118. return -1
  119. }
  120. if z2 == NInfinity {
  121. return 1
  122. }
  123. if z2 == PInfinity {
  124. return -1
  125. }
  126. return z1.integer.Cmp(z2.integer)
  127. }
  128. func MaxZ(zs ...Z) Z {
  129. if len(zs) == 0 {
  130. panic("Max called with no arguments")
  131. }
  132. if len(zs) == 1 {
  133. return zs[0]
  134. }
  135. ret := zs[0]
  136. for _, z := range zs[1:] {
  137. if z.Cmp(ret) == 1 {
  138. ret = z
  139. }
  140. }
  141. return ret
  142. }
  143. func MinZ(zs ...Z) Z {
  144. if len(zs) == 0 {
  145. panic("Min called with no arguments")
  146. }
  147. if len(zs) == 1 {
  148. return zs[0]
  149. }
  150. ret := zs[0]
  151. for _, z := range zs[1:] {
  152. if z.Cmp(ret) == -1 {
  153. ret = z
  154. }
  155. }
  156. return ret
  157. }
  158. var NInfinity = Z{infinity: -1}
  159. var PInfinity = Z{infinity: 1}
  160. var EmptyIntInterval = IntInterval{true, PInfinity, NInfinity}
  161. func InfinityFor(v ssa.Value) IntInterval {
  162. if b, ok := v.Type().Underlying().(*types.Basic); ok {
  163. if (b.Info() & types.IsUnsigned) != 0 {
  164. return NewIntInterval(NewZ(0), PInfinity)
  165. }
  166. }
  167. return NewIntInterval(NInfinity, PInfinity)
  168. }
  169. type IntInterval struct {
  170. known bool
  171. Lower Z
  172. Upper Z
  173. }
  174. func NewIntInterval(l, u Z) IntInterval {
  175. if u.Cmp(l) == -1 {
  176. return EmptyIntInterval
  177. }
  178. return IntInterval{known: true, Lower: l, Upper: u}
  179. }
  180. func (i IntInterval) IsKnown() bool {
  181. return i.known
  182. }
  183. func (i IntInterval) Empty() bool {
  184. return i.Lower == PInfinity && i.Upper == NInfinity
  185. }
  186. func (i IntInterval) IsMaxRange() bool {
  187. return i.Lower == NInfinity && i.Upper == PInfinity
  188. }
  189. func (i1 IntInterval) Intersection(i2 IntInterval) IntInterval {
  190. if !i1.IsKnown() {
  191. return i2
  192. }
  193. if !i2.IsKnown() {
  194. return i1
  195. }
  196. if i1.Empty() || i2.Empty() {
  197. return EmptyIntInterval
  198. }
  199. i3 := NewIntInterval(MaxZ(i1.Lower, i2.Lower), MinZ(i1.Upper, i2.Upper))
  200. if i3.Lower.Cmp(i3.Upper) == 1 {
  201. return EmptyIntInterval
  202. }
  203. return i3
  204. }
  205. func (i1 IntInterval) Union(other Range) Range {
  206. i2, ok := other.(IntInterval)
  207. if !ok {
  208. i2 = EmptyIntInterval
  209. }
  210. if i1.Empty() || !i1.IsKnown() {
  211. return i2
  212. }
  213. if i2.Empty() || !i2.IsKnown() {
  214. return i1
  215. }
  216. return NewIntInterval(MinZ(i1.Lower, i2.Lower), MaxZ(i1.Upper, i2.Upper))
  217. }
  218. func (i1 IntInterval) Add(i2 IntInterval) IntInterval {
  219. if i1.Empty() || i2.Empty() {
  220. return EmptyIntInterval
  221. }
  222. l1, u1, l2, u2 := i1.Lower, i1.Upper, i2.Lower, i2.Upper
  223. return NewIntInterval(l1.Add(l2), u1.Add(u2))
  224. }
  225. func (i1 IntInterval) Sub(i2 IntInterval) IntInterval {
  226. if i1.Empty() || i2.Empty() {
  227. return EmptyIntInterval
  228. }
  229. l1, u1, l2, u2 := i1.Lower, i1.Upper, i2.Lower, i2.Upper
  230. return NewIntInterval(l1.Sub(u2), u1.Sub(l2))
  231. }
  232. func (i1 IntInterval) Mul(i2 IntInterval) IntInterval {
  233. if i1.Empty() || i2.Empty() {
  234. return EmptyIntInterval
  235. }
  236. x1, x2 := i1.Lower, i1.Upper
  237. y1, y2 := i2.Lower, i2.Upper
  238. return NewIntInterval(
  239. MinZ(x1.Mul(y1), x1.Mul(y2), x2.Mul(y1), x2.Mul(y2)),
  240. MaxZ(x1.Mul(y1), x1.Mul(y2), x2.Mul(y1), x2.Mul(y2)),
  241. )
  242. }
  243. func (i1 IntInterval) String() string {
  244. if !i1.IsKnown() {
  245. return "[⊥, ⊥]"
  246. }
  247. if i1.Empty() {
  248. return "{}"
  249. }
  250. return fmt.Sprintf("[%s, %s]", i1.Lower, i1.Upper)
  251. }
  252. type IntArithmeticConstraint struct {
  253. aConstraint
  254. A ssa.Value
  255. B ssa.Value
  256. Op token.Token
  257. Fn func(IntInterval, IntInterval) IntInterval
  258. }
  259. type IntAddConstraint struct{ *IntArithmeticConstraint }
  260. type IntSubConstraint struct{ *IntArithmeticConstraint }
  261. type IntMulConstraint struct{ *IntArithmeticConstraint }
  262. type IntConversionConstraint struct {
  263. aConstraint
  264. X ssa.Value
  265. }
  266. type IntIntersectionConstraint struct {
  267. aConstraint
  268. ranges Ranges
  269. A ssa.Value
  270. B ssa.Value
  271. Op token.Token
  272. I IntInterval
  273. resolved bool
  274. }
  275. type IntIntervalConstraint struct {
  276. aConstraint
  277. I IntInterval
  278. }
  279. func NewIntArithmeticConstraint(a, b, y ssa.Value, op token.Token, fn func(IntInterval, IntInterval) IntInterval) *IntArithmeticConstraint {
  280. return &IntArithmeticConstraint{NewConstraint(y), a, b, op, fn}
  281. }
  282. func NewIntAddConstraint(a, b, y ssa.Value) Constraint {
  283. return &IntAddConstraint{NewIntArithmeticConstraint(a, b, y, token.ADD, IntInterval.Add)}
  284. }
  285. func NewIntSubConstraint(a, b, y ssa.Value) Constraint {
  286. return &IntSubConstraint{NewIntArithmeticConstraint(a, b, y, token.SUB, IntInterval.Sub)}
  287. }
  288. func NewIntMulConstraint(a, b, y ssa.Value) Constraint {
  289. return &IntMulConstraint{NewIntArithmeticConstraint(a, b, y, token.MUL, IntInterval.Mul)}
  290. }
  291. func NewIntConversionConstraint(x, y ssa.Value) Constraint {
  292. return &IntConversionConstraint{NewConstraint(y), x}
  293. }
  294. func NewIntIntersectionConstraint(a, b ssa.Value, op token.Token, ranges Ranges, y ssa.Value) Constraint {
  295. return &IntIntersectionConstraint{
  296. aConstraint: NewConstraint(y),
  297. ranges: ranges,
  298. A: a,
  299. B: b,
  300. Op: op,
  301. }
  302. }
  303. func NewIntIntervalConstraint(i IntInterval, y ssa.Value) Constraint {
  304. return &IntIntervalConstraint{NewConstraint(y), i}
  305. }
  306. func (c *IntArithmeticConstraint) Operands() []ssa.Value { return []ssa.Value{c.A, c.B} }
  307. func (c *IntConversionConstraint) Operands() []ssa.Value { return []ssa.Value{c.X} }
  308. func (c *IntIntersectionConstraint) Operands() []ssa.Value { return []ssa.Value{c.A} }
  309. func (s *IntIntervalConstraint) Operands() []ssa.Value { return nil }
  310. func (c *IntArithmeticConstraint) String() string {
  311. return fmt.Sprintf("%s = %s %s %s", c.Y().Name(), c.A.Name(), c.Op, c.B.Name())
  312. }
  313. func (c *IntConversionConstraint) String() string {
  314. return fmt.Sprintf("%s = %s(%s)", c.Y().Name(), c.Y().Type(), c.X.Name())
  315. }
  316. func (c *IntIntersectionConstraint) String() string {
  317. return fmt.Sprintf("%s = %s %s %s (%t branch)", c.Y().Name(), c.A.Name(), c.Op, c.B.Name(), c.Y().(*ssa.Sigma).Branch)
  318. }
  319. func (c *IntIntervalConstraint) String() string { return fmt.Sprintf("%s = %s", c.Y().Name(), c.I) }
  320. func (c *IntArithmeticConstraint) Eval(g *Graph) Range {
  321. i1, i2 := g.Range(c.A).(IntInterval), g.Range(c.B).(IntInterval)
  322. if !i1.IsKnown() || !i2.IsKnown() {
  323. return IntInterval{}
  324. }
  325. return c.Fn(i1, i2)
  326. }
  327. func (c *IntConversionConstraint) Eval(g *Graph) Range {
  328. s := &types.StdSizes{
  329. // XXX is it okay to assume the largest word size, or do we
  330. // need to be platform specific?
  331. WordSize: 8,
  332. MaxAlign: 1,
  333. }
  334. fromI := g.Range(c.X).(IntInterval)
  335. toI := g.Range(c.Y()).(IntInterval)
  336. fromT := c.X.Type().Underlying().(*types.Basic)
  337. toT := c.Y().Type().Underlying().(*types.Basic)
  338. fromB := s.Sizeof(c.X.Type())
  339. toB := s.Sizeof(c.Y().Type())
  340. if !fromI.IsKnown() {
  341. return toI
  342. }
  343. if !toI.IsKnown() {
  344. return fromI
  345. }
  346. // uint<N> -> sint/uint<M>, M > N: [max(0, l1), min(2**N-1, u2)]
  347. if (fromT.Info()&types.IsUnsigned != 0) &&
  348. toB > fromB {
  349. n := big.NewInt(1)
  350. n.Lsh(n, uint(fromB*8))
  351. n.Sub(n, big.NewInt(1))
  352. return NewIntInterval(
  353. MaxZ(NewZ(0), fromI.Lower),
  354. MinZ(NewBigZ(n), toI.Upper),
  355. )
  356. }
  357. // sint<N> -> sint<M>, M > N; [max(-∞, l1), min(2**N-1, u2)]
  358. if (fromT.Info()&types.IsUnsigned == 0) &&
  359. (toT.Info()&types.IsUnsigned == 0) &&
  360. toB > fromB {
  361. n := big.NewInt(1)
  362. n.Lsh(n, uint(fromB*8))
  363. n.Sub(n, big.NewInt(1))
  364. return NewIntInterval(
  365. MaxZ(NInfinity, fromI.Lower),
  366. MinZ(NewBigZ(n), toI.Upper),
  367. )
  368. }
  369. return fromI
  370. }
  371. func (c *IntIntersectionConstraint) Eval(g *Graph) Range {
  372. xi := g.Range(c.A).(IntInterval)
  373. if !xi.IsKnown() {
  374. return c.I
  375. }
  376. return xi.Intersection(c.I)
  377. }
  378. func (c *IntIntervalConstraint) Eval(*Graph) Range { return c.I }
  379. func (c *IntIntersectionConstraint) Futures() []ssa.Value {
  380. return []ssa.Value{c.B}
  381. }
  382. func (c *IntIntersectionConstraint) Resolve() {
  383. r, ok := c.ranges[c.B].(IntInterval)
  384. if !ok {
  385. c.I = InfinityFor(c.Y())
  386. return
  387. }
  388. switch c.Op {
  389. case token.EQL:
  390. c.I = r
  391. case token.GTR:
  392. c.I = NewIntInterval(r.Lower.Add(NewZ(1)), PInfinity)
  393. case token.GEQ:
  394. c.I = NewIntInterval(r.Lower, PInfinity)
  395. case token.LSS:
  396. // TODO(dh): do we need 0 instead of NInfinity for uints?
  397. c.I = NewIntInterval(NInfinity, r.Upper.Sub(NewZ(1)))
  398. case token.LEQ:
  399. c.I = NewIntInterval(NInfinity, r.Upper)
  400. case token.NEQ:
  401. c.I = InfinityFor(c.Y())
  402. default:
  403. panic("unsupported op " + c.Op.String())
  404. }
  405. }
  406. func (c *IntIntersectionConstraint) IsKnown() bool {
  407. return c.I.IsKnown()
  408. }
  409. func (c *IntIntersectionConstraint) MarkUnresolved() {
  410. c.resolved = false
  411. }
  412. func (c *IntIntersectionConstraint) MarkResolved() {
  413. c.resolved = true
  414. }
  415. func (c *IntIntersectionConstraint) IsResolved() bool {
  416. return c.resolved
  417. }