Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 1053


Synopsis:        tuple not simplified
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Fri Apr 16 12:10:01 -0700 2010
Originator:      Hendrik Tews
Release:         PVS 4.2
Organization:    os.inf.tu-dresden.de
Environment: 
 System:          
 Architecture: 

Description: 
  
  --05ufjLfGhX
  Content-Type: text/plain; charset=us-ascii
  Content-Description: message body text
  Content-Transfer-Encoding: 7bit
  
  Hi,
  
  in the appended spec an expression 
  
    (thread_state_1, memory(ss!1))`2
  
  is not simplified by assert. To reproduce, install the following
  proof
  
      ;;; Proof invariant-1 for formula System.invariant
      ;;; developed with shostak decision procedures
      (""
       (expand "invariant?")
       (skosimp* :preds? t)
       (expand "spin_lock_invariant" -1)
       (flatten)
       (expand "system_step")
       (inst?)
       (assert)
       (typepred "scheduler(ss!1)")
       (expand "ready_thread?")
       (expand "thread_running?")
       (assert)
       (expand "all_thread_states")
       (smash)
       (("1" (replace -3 * LR) (rewrite "thread_step_0") (assert) (postpone))
        ("2" (postpone)) ("3" (postpone)) ("4" (postpone)) ("5" (postpone))
        ("6" (postpone)) ("7" (postpone))))
  
  on the last lemma invariant. After running the proof the
  non-simplifying tuple is in sequent number {1}. When doing
  
    (case "(thread_state_1, memory(ss!1))`2 = memory(ss!1)")
  
  the tuple is simplified in branch 1.2 when it is in the
  consequent but not in 1.1 when it is in the antisequent.
  
  Bye,
  
  Hendrik
  
  
  --05ufjLfGhX
  Content-Type: application/octet-stream; name="tuple-simplification.pvs"
  Content-Disposition: attachment;
  	filename="tuple-simplification.pvs"
  Content-Transfer-Encoding: base64
  
  Ck1vcmVTZXRzW0EgOiBUeXBlXSA6IFRoZW9yeQpCZWdpbgogIFAgOiBWYXIgUFJFRFtBXQoKICBh
  dF9tb3N0X29uZShQKSA6IGJvb2wgPSBlbXB0eT8oUCkgb3Igc2luZ2xldG9uPyhQKQoKICBhdF9t
  b3N0X29uZV9pbXBsaWVzKFAgOiBQUkVEW0FdLCBiIDogYm9vbCkgOiBib29sID0KICAgIGVtcHR5
  PyhQKSBvcgogICAgKHNpbmdsZXRvbj8oUCkgYW5kIGIpCgpFbmQgTW9yZVNldHMKCgpFeHByZXNz
  aW9uIDogRGF0YXR5cGUKQmVnaW4KICB0cnlfbG9ja19mdW4gOiB0cnlfbG9ja19mdW4/CiAgdHJ1
  ZV9leHByIDogdHJ1ZV9leHByPwpFbmQgRXhwcmVzc2lvbgoKClN0YXRlbWVudCA6IERhdGF0eXBl
  CkJlZ2luCiAgSW1wb3J0aW5nIEV4cHJlc3Npb24KCiAgbm90aGluZyA6IG5vdGhpbmc/CiAgY3Jp
  dGljYWwgOiBjcml0aWNhbD8KICB1bmNyaXRpY2FsIDogdW5jcml0aWNhbD8KICByZWxlYXNlX3N0
  bSA6IHJlbGVhc2Vfc3RtPwogIHNlcXVlbmNlKHN0bV8xIDogU3RhdGVtZW50LCBzdG1fMiA6IFN0
  YXRlbWVudCkgOiBzZXF1ZW5jZT8KICBkb193aGlsZShzdG0gOiBTdGF0ZW1lbnQsIGNvbmRpdGlv
  biA6IEV4cHJlc3Npb24pIDogZG9fd2hpbGU/CiAgaWZfc3RtKGNvbmRpdGlvbiA6IEV4cHJlc3Np
  b24sIHN0bSA6IFN0YXRlbWVudCkgOiBpZl9zdG0/CkVuZCBTdGF0ZW1lbnQKCgpFeGVjdXRpb24g
  OiBUaGVvcnkKQmVnaW4KICBJbXBvcnRpbmcgU3RhdGVtZW50CgogIE1lbW9yeSA6IFR5cGUgPSBi
  b29sZWFuCgogIGV4ZWN1dGVfZXgoZSA6IEV4cHJlc3Npb24sIG0gOiBNZW1vcnkpIDogW2Jvb2ws
  IE1lbW9yeV0gPQogICAgQ2FzZXMgZSBvZgogICAgICB0cnVlX2V4cHIgOiAodHJ1ZSwgbSksCiAg
  ICAgIHRyeV9sb2NrX2Z1biA6IChtLCB0cnVlKQogICAgRW5kQ2FzZXMKCiAgZXhlY3V0ZV9yZWNf
  ZGVwdGgocyA6IFN0YXRlbWVudCkgOiBSZWN1cnNpdmUgbmF0ID0KICAgIENhc2VzIHMgT0YKICAg
  ICAgbm90aGluZyA6IDAsCiAgICAgIGNyaXRpY2FsIDogMCwKICAgICAgdW5jcml0aWNhbCA6IDAs
  CiAgICAgIHJlbGVhc2Vfc3RtIDogMCwKICAgICAgc2VxdWVuY2UoczEsIHMyKSA6IGV4ZWN1dGVf
  cmVjX2RlcHRoKHMxKSArIDEsCiAgICAgIGRvX3doaWxlKHMxLCBjKSA6IGV4ZWN1dGVfcmVjX2Rl
  cHRoKHMxKSArIDIsCiAgICAgIGlmX3N0bShjLCBzMSkgOiAwCiAgICBFbmRDYXNlcwogIE1lYXN1
  cmUgcyBieSA8PAoKICBleGVjdXRlX3N0bShzIDogU3RhdGVtZW50LCBtIDogTWVtb3J5KSA6IFJl
  Y3Vyc2l2ZSBbbGlzdFtTdGF0ZW1lbnRdLCBNZW1vcnldID0KICAgIENhc2VzIHMgT0YKICAgICAg
  bm90aGluZyA6IChudWxsLCBtKSwKICAgICAgY3JpdGljYWwgOiAobnVsbCwgbSksCiAgICAgIHVu
  Y3JpdGljYWwgOiAobnVsbCwgbSksCiAgICAgIHJlbGVhc2Vfc3RtIDogKG51bGwsIGZhbHNlKSwK
  ICAgICAgc2VxdWVuY2UoczEsIHMyKSA6IAogICAgICAgIExldCAocmVzdCwgbmV4dF9tZW0pID0g
  ZXhlY3V0ZV9zdG0oczEsIG0pCiAgICAgICAgSU4KICAgICAgICAgICAoYXBwZW5kKHJlc3QsICg6
  IHMyIDopKSwgbmV4dF9tZW0pLAogICAgICBkb193aGlsZShzMSwgYykgOiBleGVjdXRlX3N0bShz
  ZXF1ZW5jZShzMSwgaWZfc3RtKGMsIHMpKSwgbSksCiAgICAgIGlmX3N0bShjLCBzMSkgOgogICAg
  ICAgIExldCAoY19yZXMsIG5leHRfbWVtKSA9IGV4ZWN1dGVfZXgoYywgbSkKICAgICAgICBJTiAK
  ICAgICAgICAgIElGIGNfcmVzIAogICAgICAgICAgVGhlbiAoICg6IHMxIDopLCBuZXh0X21lbSkK
  ICAgICAgICAgIEVsc2UgKCBudWxsLCBuZXh0X21lbSkKICAgICAgICAgIEVuZElGCiAgICBFbmRD
  YXNlcwogIE1lYXN1cmUgZXhlY3V0ZV9yZWNfZGVwdGgocykKCgogIFRocmVhZF9zdGF0ZSA6IFR5
  cGUgPSBsaXN0W1N0YXRlbWVudF0KCiAgdGhyZWFkX3J1bm5pbmc/KHQgOiBUaHJlYWRfc3RhdGUp
  IDogYm9vbCA9IGNvbnM/KHQpCgogICUgdGhyZWFkX3N0YXRlX3RvX3N0YXRlbWVudCh0IDogKHRo
  cmVhZF9ydW5uaW5nPykpIDogUmVjdXJzaXZlIFN0YXRlbWVudCA9CiAgJSAgIElGIGNkcih0KSA9
  IG51bGwgVGhlbiBjYXIodCkKICAlICAgRWxzZSBzZXF1ZW5jZShjYXIodCksIHRocmVhZF9zdGF0
  ZV90b19zdGF0ZW1lbnQoY2RyKHQpKSkKICAlICAgRW5kaWYKICAlIE1lYXN1cmUgbGVuZ3RoKHQp
  CgogIHRocmVhZF9zdGVwKHQgOiAodGhyZWFkX3J1bm5pbmc/KSwgbSA6IE1lbW9yeSkgOiBbVGhy
  ZWFkX3N0YXRlLCBNZW1vcnldID0KICAgIExldCAocmVzdCwgbmV4dF9tZW0pID0gZXhlY3V0ZV9z
  dG0oY2FyKHQpLCBtKQogICAgSU4KICAgICAgKGFwcGVuZChyZXN0LCBjZHIodCkpLCBuZXh0X21l
  bSkKCgogIFN5c3RlbV9zdGF0ZSA6IFR5cGUgPSBbIwogICAgY291bnQgOiBuYXQsCiAgICB0aHJl
  YWRzIDogW25hdCAtPiBUaHJlYWRfc3RhdGVdLAogICAgbWVtb3J5IDogTWVtb3J5CiAgI10KCgog
  IHJlYWR5X3RocmVhZD8oc3MgOiBTeXN0ZW1fc3RhdGUpKG4gOiBuYXQpIDogYm9vbCA9IAogICAg
  dGhyZWFkX3J1bm5pbmc/KHRocmVhZHMoc3MpKG4pKQoKICBydW5uaW5nPyhzcyA6IFN5c3RlbV9z
  dGF0ZSkgOiBib29sID0KICAgIEV4aXN0cyhuIDogbmF0KSA6IHJlYWR5X3RocmVhZD8oc3MpKG4p
  CgogIHNjaGVkdWxlcihzcyA6IChydW5uaW5nPykpIDogKHJlYWR5X3RocmVhZD8oc3MpKSA9CiAg
  ICBQcm9qXzEoY2hvb3NlKExhbWJkYShuIDogbmF0LCBjb3VudCA6IG5hdCkgOiAKICAgICAgICAg
  ICAgICAgICAgICAgICAgICAgcmVhZHlfdGhyZWFkPyhzcykobikgQW5kIGNvdW50ID0gY291bnQo
  c3MpKSkKCiAgc3lzdGVtX3N0ZXAoc3MgOiAocnVubmluZz8pKSA6IFN5c3RlbV9zdGF0ZSA9CiAg
  ICBsZXQgbiA9IHNjaGVkdWxlcihzcyksCiAgICAgICAgKG50LCBuZXh0X21lbSkgPSB0aHJlYWRf
  c3RlcCh0aHJlYWRzKHNzKShuKSwgbWVtb3J5KHNzKSkKICAgIElOCiAgICAgICgjIGNvdW50IDo9
  IGNvdW50KHNzKSArIDEsCiAgICAgICAgIHRocmVhZHMgOj0gdGhyZWFkcyhzcykgV0lUSCBbIChu
  KSA6PSBudCBdLAogICAgICAgICBtZW1vcnkgOj0gbmV4dF9tZW0KICAgICAgIykKCgogIGludmFy
  aWFudD8oUSA6IFBSRURbU3lzdGVtX3N0YXRlXSkgOiBib29sID0KICAgIEZvcmFsbChzcyA6IFN5
  c3RlbV9zdGF0ZSkgOiBRKHNzKSBBbmQgcnVubmluZz8oc3MpIEltcGxpZXMKICAgICAgICBRKHN5
  c3RlbV9zdGVwKHNzKSkKCgpFbmQgRXhlY3V0aW9uCgoKU3lzdGVtIDogVGhlb3J5CkJlZ2luCiAg
  SW1wb3J0aW5nIEV4ZWN1dGlvbiwgTW9yZVNldHMKCiAgZXhjbHVzaXZlX3Byb2MgOiBTdGF0ZW1l
  bnQgPQogICAgc2VxdWVuY2UoCiAgICAgIGRvX3doaWxlKG5vdGhpbmcsIHRyeV9sb2NrX2Z1biks
  CiAgICAgIHNlcXVlbmNlKAogICAgICAgIGNyaXRpY2FsLAogICAgICAgIHJlbGVhc2Vfc3RtKSkK
  CiAgdGhyZWFkX2luaXQgOiBTdGF0ZW1lbnQgPQogICAgZG9fd2hpbGUoCiAgICAgIHNlcXVlbmNl
  KHVuY3JpdGljYWwsIGV4Y2x1c2l2ZV9wcm9jKSwKICAgICAgdHJ1ZV9leHByKQoKICAlIHN0YXJ0
  IHN0YXRlCiAgJSAwLT4xIDogdW5jcml0aWNhbCBzdGVwCiAgdGhyZWFkX3N0YXRlXzAgOiBUaHJl
  YWRfc3RhdGUgPSAoOiB0aHJlYWRfaW5pdCA6KQoKICAlIDEtPjIgOiBidXN5IHdhaXQgaW4gbG9j
  ayBsb29wCiAgdGhyZWFkX3N0YXRlXzEgOiBUaHJlYWRfc3RhdGUgPSAoOgogICAgZXhjbHVzaXZl
  X3Byb2MsCiAgICBpZl9zdG0odHJ1ZV9leHByLCB0aHJlYWRfaW5pdCkKICA6KQoKICAlIDItPjMg
  OiBsb2NrIG5vdCBmcmVlLCByZXRyeQogICUgMi0+NCA6IGxvY2sgb2J0YWluZWQKICB0aHJlYWRf
  c3RhdGVfMiA6IFRocmVhZF9zdGF0ZSA9ICg6CiAgICBpZl9zdG0odHJ5X2xvY2tfZnVuLCBkb193
  aGlsZShub3RoaW5nLCB0cnlfbG9ja19mdW4pKSwKICAgIHNlcXVlbmNlKGNyaXRpY2FsLCByZWxl
  YXNlX3N0bSksCiAgICBpZl9zdG0odHJ1ZV9leHByLCB0aHJlYWRfaW5pdCkKICA6KQoKICAlIDMt
  PjIgOiBidXN5IHdhaXQgaW4gbG9jayBsb29wCiAgdGhyZWFkX3N0YXRlXzMgOiBUaHJlYWRfc3Rh
  dGUgPSAoOgogICAgZG9fd2hpbGUobm90aGluZywgdHJ5X2xvY2tfZnVuKSwKICAgIHNlcXVlbmNl
  KGNyaXRpY2FsLCByZWxlYXNlX3N0bSksCiAgICBpZl9zdG0odHJ1ZV9leHByLCB0aHJlYWRfaW5p
  dCkKICA6KQoKICAlIDQtPjUgOiBjcml0aWNhbCBzZWN0aW9uIHN0ZXAKICB0aHJlYWRfc3RhdGVf
  NCA6IFRocmVhZF9zdGF0ZSA9ICg6CiAgICBzZXF1ZW5jZShjcml0aWNhbCwgcmVsZWFzZV9zdG0p
  LAogICAgaWZfc3RtKHRydWVfZXhwciwgdGhyZWFkX2luaXQpCiAgOikKCiAgJSA1LT42IDogcmVs
  ZWFzZSBsb2NrCiAgdGhyZWFkX3N0YXRlXzUgOiBUaHJlYWRfc3RhdGUgPSAoOgogICAgcmVsZWFz
  ZV9zdG0sCiAgICBpZl9zdG0odHJ1ZV9leHByLCB0aHJlYWRfaW5pdCkKICA6KQoKICAlIDYtPjAg
  OiBiYWNrIHRvIHN0YXJ0CiAgdGhyZWFkX3N0YXRlXzYgOiBUaHJlYWRfc3RhdGUgPSAoOgogICAg
  aWZfc3RtKHRydWVfZXhwciwgdGhyZWFkX2luaXQpCiAgOikKCgogIHRocmVhZF9zdGVwXzAgOiBM
  ZW1tYSBGb3JhbGwobSA6IE1lbW9yeSkgOiAKICAgIHRocmVhZF9zdGVwKHRocmVhZF9zdGF0ZV8w
  LCBtKSA9ICh0aHJlYWRfc3RhdGVfMSwgbSkKCiAgYWxsX3RocmVhZF9zdGF0ZXModCA6IFRocmVh
  ZF9zdGF0ZSkgOiBib29sID0KICAgIHQgPSB0aHJlYWRfc3RhdGVfMCBPUgogICAgdCA9IHRocmVh
  ZF9zdGF0ZV8xIE9SCiAgICB0ID0gdGhyZWFkX3N0YXRlXzIgT1IKICAgIHQgPSB0aHJlYWRfc3Rh
  dGVfMyBPUgogICAgdCA9IHRocmVhZF9zdGF0ZV80IE9SCiAgICB0ID0gdGhyZWFkX3N0YXRlXzUg
  T1IKICAgIHQgPSB0aHJlYWRfc3RhdGVfNgoKICBjcml0aWNhbF9zZWN0aW9uPyh0IDogVGhyZWFk
  X3N0YXRlKSA6IGJvb2wgPQogICAgdCA9IHRocmVhZF9zdGF0ZV80IE9SCiAgICB0ID0gdGhyZWFk
  X3N0YXRlXzUgCgoKICBjcml0aWNhbF9zZWN0aW9uX2luZGV4KHNzIDogU3lzdGVtX3N0YXRlKShu
  IDogbmF0KSA6IGJvb2wgPQogICAgY3JpdGljYWxfc2VjdGlvbj8odGhyZWFkcyhzcykobikpCgog
  IHNwaW5fbG9ja19pbnZhcmlhbnQoc3MgOiBTeXN0ZW1fc3RhdGUpIDogYm9vbCA9CiAgICBhdF9t
  b3N0X29uZV9pbXBsaWVzKGNyaXRpY2FsX3NlY3Rpb25faW5kZXgoc3MpLCBtZW1vcnkoc3MpID0g
  dHJ1ZSkgQW5kCiAgICBGb3JhbGwobiA6IG5hdCkgOiB0aHJlYWRzKHNzKShuKSA9IG51bGwgT1Ig
  CiAgICAgICBhbGxfdGhyZWFkX3N0YXRlcyh0aHJlYWRzKHNzKShuKSkKCiAgaW52YXJpYW50IDog
  TGVtbWEgaW52YXJpYW50PyhzcGluX2xvY2tfaW52YXJpYW50KQoKRW5kIFN5c3RlbQo=
  --05ufjLfGhX--

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools