diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Binaries/boogie boogie-2.4.1+dfsg/Binaries/boogie
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Binaries/boogie 1970-01-01 00:00:00.000000000 +0000
+++ boogie-2.4.1+dfsg/Binaries/boogie 2019-10-25 18:17:05.000000000 +0000
@@ -0,0 +1,30 @@
+#!/usr/bin/env bash
+
+# Wrapper script to run Boogie.exe on non-Windows systems using Mono
+#
+# Adapted from https://github.com/Microsoft/dafny/blob/master/Binaries/dafny
+
+MONO=$(which mono)
+
+# find the source directory for this script even if it's been symlinked
+# from https://stackoverflow.com/questions/59895/
+SOURCE="${BASH_SOURCE[0]}"
+while [ -h "$SOURCE" ]; do
+ DIR="$( cd -P "$( dirname "$SOURCE" )" && pwd )"
+ SOURCE="$(readlink "$SOURCE")"
+ [[ $SOURCE != /* ]] && SOURCE="$DIR/$SOURCE"
+done
+BOOGIE_ROOT="$( cd -P "$( dirname "$SOURCE" )" && pwd )"
+BOOGIE="$BOOGIE_ROOT/Boogie.exe"
+
+if [[ ! -x "$MONO" ]]; then
+ echo "Error: Boogie requires Mono to run on non-Windows systems."
+ exit 1
+fi
+
+if [[ ! -e "$BOOGIE" ]]; then
+ echo "Error: Boogie.exe not found at $BOOGIE."
+ exit 1
+fi
+
+"$MONO" "$BOOGIE" "$@"
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Binaries/Boogie.vshost.exe.manifest boogie-2.4.1+dfsg/Binaries/Boogie.vshost.exe.manifest
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Binaries/Boogie.vshost.exe.manifest 2016-10-30 01:53:09.000000000 +0000
+++ boogie-2.4.1+dfsg/Binaries/Boogie.vshost.exe.manifest 1970-01-01 00:00:00.000000000 +0000
@@ -1,11 +0,0 @@
-
-
-
-
-
-
-
-
-
-
-
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/boogie.1 boogie-2.4.1+dfsg/debian/boogie.1
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/boogie.1 2016-10-30 01:52:14.000000000 +0000
+++ boogie-2.4.1+dfsg/debian/boogie.1 2019-12-16 13:25:20.000000000 +0000
@@ -1,16 +1,21 @@
-.\" © 2013, 2015-2016 Benjamin Barenblat
+.\" © 2013, 2015-2016 Benjamin Barenblat. Licensed under the Expat license:
.\"
-.\" Licensed under the Apache License, Version 2.0 (the "License"); you may not
-.\" use this file except in compliance with the License. You may obtain a copy
-.\" of the License at
-.\"
-.\" http://www.apache.org/licenses/LICENSE-2.0
-.\"
-.\" Unless required by applicable law or agreed to in writing, software
-.\" distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
-.\" WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
-.\" License for the specific language governing permissions and limitations
-.\" under the License.
+.\" Permission is hereby granted, free of charge, to any person obtaining a copy of
+.\" this software and associated documentation files (the ""Software""), to deal in
+.\" the Software without restriction, including without limitation the rights to
+.\" use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+.\" the Software, and to permit persons to whom the Software is furnished to do so,
+.\" subject to the following conditions:
+.\" .
+.\" The above copyright notice and this permission notice shall be included in all
+.\" copies or substantial portions of the Software.
+.\" .
+.\" THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+.\" IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+.\" FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+.\" COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+.\" IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+.\" CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
.pc
.TH boogie 1 "2016-08-17" "Git snapshot 1f2d6c1" Boogie
.SH NAME
@@ -755,6 +760,6 @@
.SH SEE ALSO
.BR dot (1)
.SH COPYRIGHT
-Boogie is copyright \(co 2003-2015 Microsoft Corporation and licensed under the Microsoft Public License .
+Boogie is copyright \(co 2003-2015 Microsoft Corporation and licensed under the Expat license.
-This manual page is copyright \(co 2013, 2015-2016 Benjamin Barenblat and licensed under the Apache License, Version 2.0.
+This manual page is copyright \(co 2013, 2015-2016 Benjamin Barenblat and licensed under the Expat license.
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/bvd.1 boogie-2.4.1+dfsg/debian/bvd.1
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/bvd.1 2016-10-30 01:52:14.000000000 +0000
+++ boogie-2.4.1+dfsg/debian/bvd.1 2019-12-16 13:25:20.000000000 +0000
@@ -1,16 +1,21 @@
-.\" © 2013, 2015-2016 Benjamin Barenblat
+.\" © 2013, 2015-2016 Benjamin Barenblat. Licensed under the Expat license:
.\"
-.\" Licensed under the Apache License, Version 2.0 (the "License"); you may not
-.\" use this file except in compliance with the License. You may obtain a copy
-.\" of the License at
-.\"
-.\" http://www.apache.org/licenses/LICENSE-2.0
-.\"
-.\" Unless required by applicable law or agreed to in writing, software
-.\" distributed under the License is distributed on an "AS IS" BASIS, W.TPOUT
-.\" WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
-.\" License for the specific language governing permissions and limitations
-.\" under the License.
+.\" Permission is hereby granted, free of charge, to any person obtaining a copy of
+.\" this software and associated documentation files (the ""Software""), to deal in
+.\" the Software without restriction, including without limitation the rights to
+.\" use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+.\" the Software, and to permit persons to whom the Software is furnished to do so,
+.\" subject to the following conditions:
+.\" .
+.\" The above copyright notice and this permission notice shall be included in all
+.\" copies or substantial portions of the Software.
+.\" .
+.\" THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+.\" IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+.\" FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+.\" COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+.\" IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+.\" CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
.pc
.TH bvd 1 "2016-08-17" "Git snapshot 1f2d6c1" Boogie
.SH NAME
@@ -24,6 +29,6 @@
.B bvd
is a graphical program and accepts no options on the command line.
.SH COPYRIGHT
-Boogie is copyright \(co 2003-2015 Microsoft Corporation and licensed under the Microsoft Public License .
+Boogie is copyright \(co 2003-2015 Microsoft Corporation and licensed under the Expat license.
-This manual page is copyright \(co 2013, 2015-2016 Benjamin Barenblat and licensed under the Apache License, Version 2.0.
+This manual page is copyright \(co 2013, 2015-2016 Benjamin Barenblat and licensed under the Expat license.
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/changelog boogie-2.4.1+dfsg/debian/changelog
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/changelog 2016-10-30 01:52:24.000000000 +0000
+++ boogie-2.4.1+dfsg/debian/changelog 2019-12-16 13:25:20.000000000 +0000
@@ -1,3 +1,24 @@
+boogie (2.4.1+dfsg-0.1) unstable; urgency=medium
+
+ * Non-maintainer upload.
+ * New upstream release.
+ * Update debian/watch file.
+ * Update debian/copyright:
+ - New upstream license.
+ - Relicense debian/* to match new upstream license (Expat)
+ (see https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=944876#20).
+ - Exclude prebuilt Windows binary from the source tree.
+ * Update licenses in debian/{boogie,bvd}.1.
+ * Change Priority to optional in debian/control.
+ * Upgrade to debhelper compat level 12.
+ * Update build dependencies (Closes: #927171).
+ * Upgrade to Standards-Version 4.4.1.
+ * Fix debian/rules to make the new version build.
+ * Enable autopkgtest package testing, and add mccarthy-{91,92} tests.
+ * Update Vcs-Git and Vcs-Browser fields in debian/control.
+
+ -- Fabian Wolff Mon, 16 Dec 2019 14:25:20 +0100
+
boogie (2.3.0.61016+dfsg+3.gbp1f2d6c1-1) unstable; urgency=medium
** SNAPSHOT build @1f2d6c15cc587e9e1b91be70186ee9a26d5e1928 **
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/compat boogie-2.4.1+dfsg/debian/compat
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/compat 2016-10-29 21:40:41.000000000 +0000
+++ boogie-2.4.1+dfsg/debian/compat 1970-01-01 00:00:00.000000000 +0000
@@ -1 +0,0 @@
-9
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/control boogie-2.4.1+dfsg/debian/control
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/control 2016-10-30 01:52:15.000000000 +0000
+++ boogie-2.4.1+dfsg/debian/control 2019-12-08 06:34:31.000000000 +0000
@@ -1,18 +1,15 @@
Source: boogie
Section: cli-mono
-Priority: extra
+Priority: optional
Maintainer: Benjamin Barenblat
-Build-Depends:
- debhelper (>= 9),
-Build-Depends-Indep:
- cli-common-dev (>= 0.8),
- mono-devel (>= 2.4.2.3),
- mono-reference-assemblies-4.0,
- tzdata,
-Standards-Version: 3.9.8
+Build-Depends: debhelper-compat (= 12),
+ cli-common-dev,
+ mono-devel,
+ tzdata
+Standards-Version: 4.4.1
Homepage: http://research.microsoft.com/en-us/projects/boogie/
-Vcs-Browser: https://benjamin.barenblat.name/gitweb/?p=debian-boogie.git
-Vcs-Git: git://benjamin.barenblat.name/debian-boogie.git
+Vcs-Browser: https://salsa.debian.org/debian/boogie
+Vcs-Git: https://salsa.debian.org/debian/boogie.git
Package: boogie
Architecture: all
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/copyright boogie-2.4.1+dfsg/debian/copyright
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/copyright 2016-10-29 21:40:41.000000000 +0000
+++ boogie-2.4.1+dfsg/debian/copyright 2019-12-16 13:25:20.000000000 +0000
@@ -1,91 +1,34 @@
-Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
+Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
Upstream-Name: Boogie
-Upstream-Contact: boogie-dev@imperial.ac.uk
Source: https://github.com/boogie-org/boogie
-Copyright: 2003-2014 Microsoft
-License: Ms-PL
+Files-Excluded: Util/VS2010/Boogie/BoogieLanguageService/Resources/Irony.dll
+Comment: Irony.dll is a prebuilt Windows binary whose source code is not
+ included in this package, so it does not belong into the Debian
+ package.
-Files: *
+Files: *
Copyright: 2009-2015 Microsoft Corporation
-License: Ms-PL
+License: Expat
-Files: debian/*
-Copyright: 2015-2016 Benjamin Barenblat
-License: Apache-2.0
+Files: debian/*
+Copyright: 2019 Fabian Wolff
+ 2015-2016 Benjamin Barenblat
+License: Expat
-License: Apache-2.0
- Licensed under the Apache License, Version 2.0 (the "License"); you may not use
- this file except in compliance with the License. You may obtain a copy of the
- License at
- .
- http://www.apache.org/licenses/LICENSE-2.0
- .
- Unless required by applicable law or agreed to in writing, software distributed
- under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR
- CONDITIONS OF ANY KIND, either express or implied. See the License for the
- specific language governing permissions and limitations under the License.
- .
- On Debian systems, the complete text of the Apache License, Version 2.0, can be
- found in "/usr/share/common-licenses/Apache-2.0".
-
-License: Ms-PL
- Microsoft Public License (Ms-PL)
- .
- This license governs use of the accompanying software. If you use the software,
- you accept this license. If you do not accept the license, do not use the
- software.
- .
- 1. Definitions
- .
- The terms "reproduce," "reproduction," "derivative works," and "distribution"
- have the same meaning here as under U.S. copyright law.
- .
- A "contribution" is the original software, or any additions or changes to the
- software.
- .
- A "contributor" is any person that distributes its contribution under this
- license.
- .
- "Licensed patents" are a contributor's patent claims that read directly on its
- contribution.
- .
- 2. Grant of Rights
- .
- (A) Copyright Grant- Subject to the terms of this license, including the license
- conditions and limitations in section 3, each contributor grants you a
- non-exclusive, worldwide, royalty-free copyright license to reproduce its
- contribution, prepare derivative works of its contribution, and distribute its
- contribution or any derivative works that you create.
- .
- (B) Patent Grant- Subject to the terms of this license, including the license
- conditions and limitations in section 3, each contributor grants you a
- non-exclusive, worldwide, royalty-free license under its licensed patents to
- make, have made, use, sell, offer for sale, import, and/or otherwise dispose of
- its contribution in the software or derivative works of the contribution in the
- software.
- .
- 3. Conditions and Limitations
- .
- (A) No Trademark License- This license does not grant you rights to use any
- contributors' name, logo, or trademarks.
- .
- (B) If you bring a patent claim against any contributor over patents that you
- claim are infringed by the software, your patent license from such contributor
- to the software ends automatically.
- .
- (C) If you distribute any portion of the software, you must retain all
- copyright, patent, trademark, and attribution notices that are present in the
- software.
- .
- (D) If you distribute any portion of the software in source code form, you may
- do so only under this license by including a complete copy of this license with
- your distribution. If you distribute any portion of the software in compiled or
- object code form, you may only do so under a license that complies with this
- license.
- .
- (E) The software is licensed "as-is." You bear the risk of using it. The
- contributors give no express warranties, guarantees or conditions. You may have
- additional consumer rights under your local laws which this license cannot
- change. To the extent permitted under your local laws, the contributors exclude
- the implied warranties of merchantability, fitness for a particular purpose and
- non-infringement.
+License: Expat
+ Permission is hereby granted, free of charge, to any person obtaining a copy of
+ this software and associated documentation files (the ""Software""), to deal in
+ the Software without restriction, including without limitation the rights to
+ use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ the Software, and to permit persons to whom the Software is furnished to do so,
+ subject to the following conditions:
+ .
+ The above copyright notice and this permission notice shall be included in all
+ copies or substantial portions of the Software.
+ .
+ THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/gbp.conf boogie-2.4.1+dfsg/debian/gbp.conf
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/gbp.conf 2016-10-30 00:40:30.000000000 +0000
+++ boogie-2.4.1+dfsg/debian/gbp.conf 2019-12-08 06:34:31.000000000 +0000
@@ -1,2 +1,4 @@
[DEFAULT]
-upstream-tree = 1f2d6c15cc587e9e1b91be70186ee9a26d5e1928
+debian-branch = master
+upstream-branch = upstream
+pristine-tar = True
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/rules boogie-2.4.1+dfsg/debian/rules
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/rules 2016-10-30 01:51:01.000000000 +0000
+++ boogie-2.4.1+dfsg/debian/rules 2019-12-08 06:34:31.000000000 +0000
@@ -1,9 +1,18 @@
#!/usr/bin/make -f
-# -*- makefile -*-
+
+# Uncomment this to turn on verbose mode
+# export DH_VERBOSE = 1
%:
dh $@ --with cli
-.PHONY: override_dh_auto_build
override_dh_auto_build:
+ # Apparently, the Mono C# compiler does not support pattern
+ # matching yet. The proper thing to do here would be to patch
+ # Witnesses.cs, but unfortunately, dpkg-source fails
+ # spectacularly when it comes to patching files with DOS
+ # (CRLF) line endings. Therefore, we need to do a "manual
+ # patch" here:
+ sed -i 's/is null/== null/g' Source/Concurrency/Witnesses.cs
xbuild /p:TargetFrameworkVersion=v4.0 Source/Boogie.sln
+ sed -i 's/is null/== null/g' Source/Concurrency/Witnesses.cs
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/tests/control boogie-2.4.1+dfsg/debian/tests/control
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/tests/control 1970-01-01 00:00:00.000000000 +0000
+++ boogie-2.4.1+dfsg/debian/tests/control 2019-12-08 06:34:31.000000000 +0000
@@ -0,0 +1,2 @@
+Tests: mccarthy-91 mccarthy-92
+Depends: @
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/tests/mccarthy-91 boogie-2.4.1+dfsg/debian/tests/mccarthy-91
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/tests/mccarthy-91 1970-01-01 00:00:00.000000000 +0000
+++ boogie-2.4.1+dfsg/debian/tests/mccarthy-91 2019-12-08 06:34:31.000000000 +0000
@@ -0,0 +1,31 @@
+#!/bin/sh
+
+set -e
+
+# Run an example stolen from https://rise4fun.com/Boogie/McCarthy-91
+
+TMPDIR=$(mktemp -d)
+trap "rm -rf $TMPDIR" EXIT
+cd $TMPDIR
+
+cat < test.bpl
+procedure F(n: int) returns (r: int)
+ ensures 100 < n ==> r == n - 10; // This postcondition is easy to check by hand
+ ensures n <= 100 ==> r == 91; // Do you believe this one is true?
+{
+ if (100 < n) {
+ r := n - 10;
+ } else {
+ call r := F(n + 11);
+ call r := F(r);
+ }
+}
+EOF
+
+cat < expected
+Boogie program verifier finished with 1 verified, 0 errors
+EOF
+
+boogie test.bpl > boogie_output
+tail -n1 boogie_output > result
+diff result expected
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/tests/mccarthy-92 boogie-2.4.1+dfsg/debian/tests/mccarthy-92
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/tests/mccarthy-92 1970-01-01 00:00:00.000000000 +0000
+++ boogie-2.4.1+dfsg/debian/tests/mccarthy-92 2019-12-08 06:34:31.000000000 +0000
@@ -0,0 +1,32 @@
+#!/bin/sh
+
+set -e
+
+# Run an example based on https://rise4fun.com/Boogie/McCarthy-91
+# This example is adapted to be wrong: We should not be able to verify it
+
+TMPDIR=$(mktemp -d)
+trap "rm -rf $TMPDIR" EXIT
+cd $TMPDIR
+
+cat < test.bpl
+procedure F(n: int) returns (r: int)
+ ensures 100 < n ==> r == n - 10;
+ ensures n <= 100 ==> r == 92; // This would have to be 91 for the program to verify
+{
+ if (100 < n) {
+ r := n - 10;
+ } else {
+ call r := F(n + 11);
+ call r := F(r);
+ }
+}
+EOF
+
+cat < expected
+Boogie program verifier finished with 0 verified, 1 error
+EOF
+
+boogie test.bpl > boogie_output
+tail -n1 boogie_output > result
+diff result expected
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/watch boogie-2.4.1+dfsg/debian/watch
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/debian/watch 2016-10-29 21:40:41.000000000 +0000
+++ boogie-2.4.1+dfsg/debian/watch 2019-12-16 13:25:20.000000000 +0000
@@ -1,4 +1,6 @@
-# Upstream does not cut releases at this point – only Git snapshots.
-# Consequently, constructing a suitable watch file is impossible.
-#
-# -- Benjamin Barenblat Tue 11 Aug 2015 19:27:24 -0400
+version=4
+opts="repacksuffix=+dfsg,repack, \
+ dversionmangle=auto, \
+ filenamemangle=s%(?:.*?)?v?(\d[\d.]*)\.tar\.gz%boogie-$1.tar.gz%" \
+ https://github.com/boogie-org/boogie/releases \
+ (?:.*?/)?v?(\d[\d.]*)\.tar\.gz
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/.gitignore boogie-2.4.1+dfsg/.gitignore
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/.gitignore 2016-10-30 01:53:09.000000000 +0000
+++ boogie-2.4.1+dfsg/.gitignore 2019-10-25 18:17:05.000000000 +0000
@@ -1,11 +1,12 @@
# Nuget
Source/packages/*
+Source/**/nupkg
# Tests
Source/UnitTests/TestResult.xml
Source/UnitTests/*/bin
Source/UnitTests/*/obj
-Test/*/Output
+Test/**/Output
TestResult.xml
# Binaries
@@ -18,6 +19,7 @@
Binaries/*.exe
Binaries/*.pdb
Binaries/*.config
+Binaries/*.vshost.exe.manifest
# Editor temporary files
.*.swp
@@ -29,3 +31,12 @@
Source/*.user
Source/*.suo
Source/*.cache
+Source/.vs/
+
+.vscode
+
+# MonoDevelop files
+Source/*.userprefs
+
+# Rider files
+.idea/
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/LICENSE.txt boogie-2.4.1+dfsg/LICENSE.txt
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/LICENSE.txt 2016-10-30 01:53:09.000000000 +0000
+++ boogie-2.4.1+dfsg/LICENSE.txt 2019-10-25 18:17:05.000000000 +0000
@@ -1,60 +1,22 @@
-Microsoft Public License (Ms-PL)
+Copyright (c) Microsoft Corporation
-This license governs use of the accompanying software. If you use the software,
-you accept this license. If you do not accept the license, do not use the
-software.
+All rights reserved.
-1. Definitions
+MIT License
-The terms "reproduce," "reproduction," "derivative works," and "distribution"
-have the same meaning here as under U.S. copyright law.
-
-A "contribution" is the original software, or any additions or changes to the
-software.
-
-A "contributor" is any person that distributes its contribution under this
-license.
-
-"Licensed patents" are a contributor's patent claims that read directly on its
-contribution.
-
-2. Grant of Rights
-
-(A) Copyright Grant- Subject to the terms of this license, including the license
-conditions and limitations in section 3, each contributor grants you a
-non-exclusive, worldwide, royalty-free copyright license to reproduce its
-contribution, prepare derivative works of its contribution, and distribute its
-contribution or any derivative works that you create.
-
-(B) Patent Grant- Subject to the terms of this license, including the license
-conditions and limitations in section 3, each contributor grants you a
-non-exclusive, worldwide, royalty-free license under its licensed patents to
-make, have made, use, sell, offer for sale, import, and/or otherwise dispose of
-its contribution in the software or derivative works of the contribution in the
-software.
-
-3. Conditions and Limitations
-
-(A) No Trademark License- This license does not grant you rights to use any
-contributors' name, logo, or trademarks.
-
-(B) If you bring a patent claim against any contributor over patents that you
-claim are infringed by the software, your patent license from such contributor
-to the software ends automatically.
-
-(C) If you distribute any portion of the software, you must retain all
-copyright, patent, trademark, and attribution notices that are present in the
-software.
-
-(D) If you distribute any portion of the software in source code form, you may
-do so only under this license by including a complete copy of this license with
-your distribution. If you distribute any portion of the software in compiled or
-object code form, you may only do so under a license that complies with this
-license.
-
-(E) The software is licensed "as-is." You bear the risk of using it. The
-contributors give no express warranties, guarantees or conditions. You may have
-additional consumer rights under your local laws which this license cannot
-change. To the extent permitted under your local laws, the contributors exclude
-the implied warranties of merchantability, fitness for a particular purpose and
-non-infringement.
+Permission is hereby granted, free of charge, to any person obtaining a copy of
+this software and associated documentation files (the ""Software""), to deal in
+the Software without restriction, including without limitation the rights to
+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+the Software, and to permit persons to whom the Software is furnished to do so,
+subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/README.md boogie-2.4.1+dfsg/README.md
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/README.md 2016-10-30 01:53:09.000000000 +0000
+++ boogie-2.4.1+dfsg/README.md 2019-10-25 18:17:05.000000000 +0000
@@ -52,7 +52,7 @@
### Requirements
- [NuGet](https://www.nuget.org/)
-- [Z3](https://github.com/Z3Prover/z3) 4.4.1 or [CVC4](http://cvc4.cs.nyu.edu/web/) **FIXME_VERSION** (note
+- [Z3](https://github.com/Z3Prover/z3) 4.8.4 (earlier versions may also work, but the test suite assumes 4.8.4 to produce the expected output) or [CVC4](http://cvc4.cs.nyu.edu/web/) **FIXME_VERSION** (note
CVC4 support is experimental)
#### Windows specific
@@ -108,7 +108,19 @@
$ ln -s /usr/bin/z3 Binaries/z3.exe
```
-You're now ready to run Boogie!
+## Running
+
+On a Windows system call the Boogie binary:
+
+```
+$ Binaries\Boogie.exe
+```
+
+On a non-Windows system use the wrapper script:
+
+```
+$ Binaries/boogie
+```
## Testing
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/AbsInt/AbsInt.csproj boogie-2.4.1+dfsg/Source/AbsInt/AbsInt.csproj
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/AbsInt/AbsInt.csproj 2016-10-30 01:53:09.000000000 +0000
+++ boogie-2.4.1+dfsg/Source/AbsInt/AbsInt.csproj 2019-10-25 18:17:05.000000000 +0000
@@ -10,7 +10,7 @@
Properties
AbsInt
BoogieAbsInt
- v4.0
+ v4.5
512
1
true
@@ -34,7 +34,7 @@
false
false
true
- Client
+
true
@@ -74,6 +74,7 @@
Full
%28none%29
AllRules.ruleset
+ false
pdbonly
@@ -83,6 +84,7 @@
prompt
4
AllRules.ruleset
+ false
true
@@ -99,6 +101,7 @@
true
4
false
+ false
true
@@ -144,6 +147,7 @@
0
4
false
+ false
true
@@ -162,6 +166,7 @@
true
4
false
+ false
bin\x86\Release\
@@ -179,6 +184,7 @@
;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
true
4
+ false
true
@@ -196,6 +202,7 @@
true
4
false
+ false
true
@@ -212,6 +219,7 @@
;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
4
false
+ false
true
@@ -221,6 +229,7 @@
AnyCPU
prompt
AllRules.ruleset
+ false
true
@@ -230,6 +239,7 @@
AnyCPU
prompt
AllRules.ruleset
+ false
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/AbsInt/AbsInt-NetCore.csproj boogie-2.4.1+dfsg/Source/AbsInt/AbsInt-NetCore.csproj
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/AbsInt/AbsInt-NetCore.csproj 1970-01-01 00:00:00.000000000 +0000
+++ boogie-2.4.1+dfsg/Source/AbsInt/AbsInt-NetCore.csproj 2019-10-25 18:17:05.000000000 +0000
@@ -0,0 +1,30 @@
+
+
+
+ Library
+ BoogieAbsInt
+ netcoreapp2.2
+ COREFX_SUBSET
+ false
+
+
+
+
+
+
+
+
+
+
+ false
+
+
+
+
+ version.cs
+
+
+
+
+
+
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/AIFramework/AIFramework.csproj boogie-2.4.1+dfsg/Source/AIFramework/AIFramework.csproj
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/AIFramework/AIFramework.csproj 2016-10-30 01:53:09.000000000 +0000
+++ boogie-2.4.1+dfsg/Source/AIFramework/AIFramework.csproj 2019-10-25 18:17:05.000000000 +0000
@@ -10,7 +10,7 @@
Properties
AIFramework
AIFramework
- v4.0
+ v4.5
512
1
true
@@ -34,7 +34,7 @@
false
false
true
- Client
+
true
@@ -74,6 +74,7 @@
Full
%28none%29
AllRules.ruleset
+ false
pdbonly
@@ -83,6 +84,7 @@
prompt
4
AllRules.ruleset
+ false
true
@@ -97,6 +99,7 @@
prompt
Migrated rules for AIFramework.ruleset
true
+ false
true
@@ -137,6 +140,7 @@
Full
Build
0
+ false
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/AIFramework/AIFramework-NetCore.csproj boogie-2.4.1+dfsg/Source/AIFramework/AIFramework-NetCore.csproj
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/AIFramework/AIFramework-NetCore.csproj 1970-01-01 00:00:00.000000000 +0000
+++ boogie-2.4.1+dfsg/Source/AIFramework/AIFramework-NetCore.csproj 2019-10-25 18:17:05.000000000 +0000
@@ -0,0 +1,26 @@
+
+
+
+ Library
+ AIFramework
+ netcoreapp2.2
+ COREFX_SUBSET
+ false
+
+
+
+
+
+
+
+
+ false
+
+
+
+
+
+
+
+
+
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/Basetypes/Basetypes.csproj boogie-2.4.1+dfsg/Source/Basetypes/Basetypes.csproj
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/Basetypes/Basetypes.csproj 2016-10-30 01:53:09.000000000 +0000
+++ boogie-2.4.1+dfsg/Source/Basetypes/Basetypes.csproj 2019-10-25 18:17:05.000000000 +0000
@@ -10,7 +10,7 @@
Properties
Basetypes
BoogieBasetypes
- v4.0
+ v4.5
512
1
true
@@ -34,7 +34,7 @@
false
false
true
- Client
+
true
@@ -74,6 +74,7 @@
Full
%28none%29
AllRules.ruleset
+ false
pdbonly
@@ -83,6 +84,7 @@
prompt
4
AllRules.ruleset
+ false
true
@@ -99,6 +101,7 @@
true
4
false
+ false
true
@@ -141,6 +144,7 @@
0
4
false
+ false
true
@@ -150,6 +154,7 @@
AnyCPU
prompt
AllRules.ruleset
+ false
@@ -162,6 +167,7 @@
version.cs
+
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/Basetypes/Basetypes-NetCore.csproj boogie-2.4.1+dfsg/Source/Basetypes/Basetypes-NetCore.csproj
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/Basetypes/Basetypes-NetCore.csproj 1970-01-01 00:00:00.000000000 +0000
+++ boogie-2.4.1+dfsg/Source/Basetypes/Basetypes-NetCore.csproj 2019-10-25 18:17:05.000000000 +0000
@@ -0,0 +1,27 @@
+
+
+
+ Library
+ BoogieBasetypes
+ netcoreapp2.2
+ COREFX_SUBSET
+ false
+
+
+
+
+
+
+
+ false
+
+
+
+
+ version.cs
+
+
+
+
+
+
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/Basetypes/BigFloat.cs boogie-2.4.1+dfsg/Source/Basetypes/BigFloat.cs
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/Basetypes/BigFloat.cs 2016-10-30 01:53:09.000000000 +0000
+++ boogie-2.4.1+dfsg/Source/Basetypes/BigFloat.cs 2019-10-25 18:17:05.000000000 +0000
@@ -5,49 +5,29 @@
//-----------------------------------------------------------------------------
using System;
-using System.Collections.Generic;
+using System.Diagnostics.Contracts;
using System.Linq;
using System.Text;
-using System.Diagnostics.Contracts;
-using System.Diagnostics;
namespace Microsoft.Basetypes
{
using BIM = System.Numerics.BigInteger;
-
+
///
- /// A representation of a 32-bit floating point value
- /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit significand
+ /// A representation of a floating-point value
+ /// Note that this value has a 1-bit sign, along with an exponent and significand whose sizes must be greater than 1
///
public struct BigFloat
{
//Please note that this code outline is copy-pasted from BigDec.cs
// the internal representation
- [Rep]
internal readonly BIM significand; //Note that the significand arrangement matches standard fp arrangement (most significant bit is farthest left)
- [Rep]
- internal readonly int significandSize;
- [Rep]
+ internal readonly int significandSize; //The bit size of the significand
internal readonly BIM exponent; //The value of the exponent is always positive as per fp representation requirements
- [Rep]
internal readonly int exponentSize; //The bit size of the exponent
- [Rep]
internal readonly String value; //Only used with second syntax
- [Rep]
- internal readonly bool isNeg;
-
- public BIM Significand {
- get {
- return significand;
- }
- }
-
- public BIM Exponent {
- get {
- return exponent;
- }
- }
+ internal readonly bool isSignBitSet; //Stores the sign bit in the fp representaiton
public int SignificandSize {
get {
@@ -61,30 +41,8 @@
}
}
- public bool IsNegative {
- get {
- return this.isNeg;
- }
- }
-
- public String Value {
- get {
- return value;
- }
- }
-
public static BigFloat ZERO = new BigFloat(false, BIM.Zero, BIM.Zero, 24, 8); //Does not include negative zero
- private static readonly BIM two = new BIM(2);
- private static readonly BIM one = new BIM(1);
- private static BIM two_n(int n) {
- BIM toReturn = one;
- for (int i = 0; i < n; i++)
- toReturn = toReturn * two;
- return toReturn;
- }
-
-
////////////////////////////////////////////////////////////////////////////
// Constructors
@@ -96,79 +54,108 @@
return new BigFloat(v.ToString(), 24, 8);
}
- public static BigFloat FromInt(int v, int significandSize, int exponentSize)
- {
+ public static BigFloat FromBigInt(BIM v, int significandSize, int exponentSize) {
return new BigFloat(v.ToString(), significandSize, exponentSize);
}
- public static BigFloat FromBigInt(BIM v) {
- return new BigFloat(v.ToString(), 24, 8);
- }
+ [Pure]
+ public static BigFloat FromString(String s) {
+ /*
+ * String must be either of the format [-]0x^.^e*f*e*
+ * or of the special value formats: 0NaN*e* 0nan*e* 0+oo*e* 0-oo*e*
+ * Where ^ indicates a hexadecimal value and * indicates an integer value
+ */
- public static BigFloat FromBigInt(BIM v, int significandSize, int exponentSize)
- {
- return new BigFloat(v.ToString(), significandSize, exponentSize);
- }
+ int posLastE = s.LastIndexOf('e');
- public static BigFloat FromBigDec(BigDec v)
- {
- return new BigFloat(v.ToDecimalString(), 24, 8);
- }
+ int expSize = int.Parse(s.Substring(posLastE + 1));
+ if (expSize <= 1) {
+ throw new FormatException("Exponent size must be greater than 1");
+ }
- public static BigFloat FromBigDec(BigDec v, int significandSize, int exponentSize)
- {
- return new BigFloat(v.ToDecimalString(), significandSize, exponentSize);
- }
+ int posLastF = s.LastIndexOf('f');
+ int posSig = posLastF + 1;
+ if (posLastF == -1) {//NaN, +oo, -oo
+ posSig = 4;
+ }
- [Pure]
- public static BigFloat FromString(String s) {
- /*
- * String must be either of the format *e*f*e*
- * or of the special value formats: 0NaN*e* 0nan*e* 0+oo*e* 0-oo*e*
- * Where * indicates an integer value (digit)
- */
- BIM sig, exp;
- int sigSize, expSize;
- bool isNeg;
-
- if (s.IndexOf('f') == -1) {
- String val = s;
- sigSize = int.Parse(s.Substring(4, s.IndexOf('e')-4));
- expSize = int.Parse(s.Substring(s.IndexOf('e') + 1));
- if (sigSize <= 0 || expSize <= 0)
- throw new FormatException("Significand and Exponent sizes must be greater than 0");
- return new BigFloat(val, sigSize, expSize);
- }
-
- sig = BIM.Parse(s.Substring(0, s.IndexOf('e')));
- exp = BIM.Parse(s.Substring(s.IndexOf('e') + 1, s.IndexOf('f') - s.IndexOf('e') - 1));
- sigSize = int.Parse(s.Substring(s.IndexOf('f') + 1, s.IndexOf('e', s.IndexOf('e') + 1) - s.IndexOf('f') - 1));
- expSize = int.Parse(s.Substring(s.IndexOf('e', s.IndexOf('e') + 1) + 1));
- isNeg = s[0] == '-'; //We do this so that -0 is parsed correctly
-
- if (sigSize <= 0 || expSize <= 0)
- throw new FormatException("Significand and Exponent sizes must be greater than 0");
-
- sigSize = sigSize - 1; //Get rid of sign bit
- sig = BIM.Abs(sig); //sig must be positive
- //Uncomment if you want to shift the exponent for the user (i.e. 0e-1f24e8 --> 0e126f24e8)
- //exp = exp + BIM.Pow(new BIM(2), expSize-1) - BIM.One;
-
- if (exp < 0 || exp >= BIM.Pow(new BIM(2), expSize))
- throw new FormatException("The given exponent " + exp + " cannot fit in the bit size " + expSize);
+ int sigSize = int.Parse(s.Substring(posSig, posLastE - posSig));
+ if (sigSize <= 1) {
+ throw new FormatException("Significand size must be greater than 1");
+ }
+
+ if (posLastF == -1) {//NaN, +oo, -oo
+ return new BigFloat(s.Substring(1, 3), sigSize, expSize);
+ }
+
+ bool isSignBitSet = s[0] == '-';
+
+ int posX = s.IndexOf('x');
+ int posSecondLastE = s.LastIndexOf('e', posLastE - 1);
+
+ string hexSig = s.Substring(posX + 1, posSecondLastE - (posX + 1));
+ BIM oldExp = BIM.Parse(s.Substring(posSecondLastE + 1, posLastF - (posSecondLastE + 1)));
+
+ string binSig = string.Join(string.Empty,
+ hexSig.Select(
+ c => (c == '.' ? "." : Convert.ToString(Convert.ToInt32(c.ToString(), 16), 2).PadLeft(4, '0'))
+ )
+ );
+
+ int posDec = binSig.IndexOf('.');
+
+ binSig = binSig.Remove(posDec, 1);
+
+ int posFirstOne = binSig.IndexOf('1');
+ int posLastOne = binSig.LastIndexOf('1');
+
+ if (posFirstOne == -1) {
+ return new BigFloat(isSignBitSet, 0, 0, sigSize, expSize);
+ }
+
+ binSig = binSig.Substring(posFirstOne, posLastOne - posFirstOne + 1);
+
+ BIM bias = BIM.Pow(2, expSize - 1) - 1;
+ BIM upperBound = 2 * bias + 1;
+
+ BIM newExp = 4 * oldExp + bias + (posDec - posFirstOne - 1);
+
+ if (newExp <= 0) {
+ if (-newExp <= (sigSize - 1) - binSig.Length) {
+ binSig = new string('0', (int) -newExp) + binSig;
+ newExp = 0;
+ }
+ } else {
+ binSig = binSig.Substring(1);
+ }
+
+ if (newExp < 0 || newExp >= upperBound) {
+ throw new FormatException("The given exponent cannot fit in the bit size " + expSize);
+ }
- if (sig >= BIM.Pow(new BIM(2), sigSize))
- throw new FormatException("The given significand " + sig + " cannot fit in the bit size " + (sigSize+1));
+ binSig = binSig.PadRight(sigSize - 1, '0');
- return new BigFloat(isNeg, sig, exp, sigSize, expSize);
+ if (binSig.Length > sigSize - 1) {
+ throw new FormatException("The given significand cannot fit in the bit size " + (sigSize - 1));
+ }
+
+ BIM newSig = 0;
+ foreach (char b in binSig) {
+ if (b != '.') {
+ newSig <<= 1;
+ newSig += b - '0';
+ }
+ }
+
+ return new BigFloat(isSignBitSet, newSig, newExp, sigSize, expSize);
}
- public BigFloat(bool isNeg, BIM significand, BIM exponent, int significandSize, int exponentSize) {
+ public BigFloat(bool isSignBitSet, BIM significand, BIM exponent, int significandSize, int exponentSize) {
this.exponentSize = exponentSize;
this.exponent = exponent;
this.significand = significand;
- this.significandSize = significandSize+1;
- this.isNeg = isNeg;
+ this.significandSize = significandSize;
+ this.isSignBitSet = isSignBitSet;
this.value = "";
}
@@ -178,21 +165,12 @@
this.exponent = BIM.Zero;
this.significand = BIM.Zero;
this.value = value;
- if (value.Equals("nan"))
+ if (value.Equals("nan")) {
this.value = "NaN";
- this.isNeg = value[0] == '-';
- }
+ }
- private BIM maxsignificand()
- {
- BIM result = one;
- for (int i = 0; i < significandSize; i++)
- result = result * two;
- return result - one;
+ this.isSignBitSet = value[0] == '-';
}
- private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; }
-
-
////////////////////////////////////////////////////////////////////////////
// Basic object operations
@@ -200,309 +178,413 @@
[Pure]
[Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object obj) {
- if (obj == null)
+ if (obj == null) {
return false;
- if (!(obj is BigFloat))
+ }
+
+ if (!(obj is BigFloat)) {
return false;
+ }
- return (this == (BigFloat)obj);
+ return (this == (BigFloat) obj);
}
[Pure]
public override int GetHashCode() {
- return significand.GetHashCode() * 13 + Exponent.GetHashCode();
+ return significand.GetHashCode() * 13 + exponent.GetHashCode();
}
[Pure]
public override string/*!*/ ToString() {
Contract.Ensures(Contract.Result() != null);
- return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;
- }
-
+ if (value == "") {
+ byte[] sigBytes = significand.ToByteArray();
+ StringBuilder binSig = new StringBuilder();
- ////////////////////////////////////////////////////////////////////////////
- // Conversion operations
-
- ///
- /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!
- /// Converts the given decimal value (provided as a string) to the nearest floating point approximation
- /// the returned fp assumes the given significand and exponent size
- ///
- ///
- ///
- ///
- ///
- public static BigFloat Round(String value, int exponentSize, int significandSize)
- {
- int i = value.IndexOf('.');
- if (i == -1)
- return Round(BIM.Parse(value), BIM.Zero, exponentSize, significandSize);
- return Round(i == 0 ? BIM.Zero : BIM.Parse(value.Substring(0, i)), BIM.Parse(value.Substring(i + 1, value.Length - i - 1)), exponentSize, significandSize);
- }
+ if (exponent == 0) {
+ binSig.Append('0');
+ } else {
+ binSig.Append('1'); //hidden bit
+ }
- ///
- /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!!
- /// Converts value.dec_value to a the closest float approximation with the given significandSize, exponentSize
- /// Returns the result of this calculation
- ///
- ///
- ///
- ///
- ///
- ///
- public static BigFloat Round(BIM value, BIM dec_value, int exponentSize, int significandSize)
- {
- int exp = 0;
- BIM one = new BIM(1);
- BIM ten = new BIM(10);
- BIM dec_max = new BIM(0); //represents the order of magnitude of dec_value for carrying during calculations
-
- //First, determine the exponent
- while (value > one) { //Divide by two, increment exponent by 1
- if (!(value % two).IsZero) { //Add "1.0" to the decimal
- dec_max = new BIM(10);
- while (dec_max < dec_value)
- dec_max = dec_max * ten;
- dec_value = dec_value + dec_max;
- }
- value = value / two;
- if (!(dec_value % ten).IsZero)
- dec_value = dec_value * ten; //Creates excess zeroes to avoid losing data during division
- dec_value = dec_value / two;
- exp++;
- }
- if (value.IsZero && !dec_value.IsZero) {
- dec_max = new BIM(10);
- while (dec_max < dec_value)
- dec_max = dec_max * ten;
- while (value.IsZero) {//Multiply by two, decrement exponent by 1
- dec_value = dec_value * two;
- if (dec_value >= dec_max) {
- dec_value = dec_value - dec_max;
- value = value + one;
+ for (int i = significandSize - 2; i >= 0; --i) { //little endian
+ if (i / 8 < sigBytes.Length) {
+ binSig.Append((char) ('0' + ((sigBytes[i / 8] >> (i % 8)) & 1)));
+ } else {
+ binSig.Append('0');
}
- exp--;
}
- }
- //Second, calculate the significand
- value = new BIM(0); //remove implicit bit
- dec_max = new BIM(10);
- while (dec_max < dec_value)
- dec_max = dec_max * ten;
- for (int i = significandSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the significand is fully calculated
- dec_value = dec_value * two;
- if (dec_value >= dec_max) {
- dec_value = dec_value - dec_max;
- value = value + two_n(i); //Note that i is decrementing so that the most significant bit is left-most in the representation
+ BIM bias = BIM.Pow(2, exponentSize - 1) - 1;
+ if (exponent == 0) {
+ --bias;
}
- }
- return new BigFloat(false, BIM.Zero, BIM.Parse(value.ToString()), exponentSize, significandSize); //Sign not actually checked...
+ int moveDec = ((int) ((exponent - bias) % 4) + 4) % 4;
+ BIM finalExp = (exponent - bias - moveDec) / 4;
+
+ string leftBinSig = binSig.ToString().Substring(0, moveDec + 1);
+ string rightBinSig = binSig.ToString().Substring(moveDec + 1);
+
+ leftBinSig = new string('0', 4 - leftBinSig.Length % 4) + leftBinSig;
+ rightBinSig = rightBinSig + new string('0', 4 - rightBinSig.Length % 4);
+
+ StringBuilder leftHexSig = new StringBuilder();
+ StringBuilder rightHexSig = new StringBuilder();
+
+ for (int i = 0; i < leftBinSig.Length / 4; ++i) {
+ leftHexSig.AppendFormat("{0:X}", Convert.ToByte(leftBinSig.Substring(i * 4, 4), 2));
+ }
+ for (int i = 0; i < rightBinSig.Length / 4; ++i) {
+ rightHexSig.AppendFormat("{0:X}", Convert.ToByte(rightBinSig.Substring(i * 4, 4), 2));
+ }
+
+ return String.Format("{0}0x{1}.{2}e{3}f{4}e{5}", isSignBitSet ? "-" : "", leftHexSig, rightHexSig, finalExp, significandSize, exponentSize);
+ }
+ return String.Format("0{0}{1}e{2}", value, significandSize, exponentSize);
}
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Conversion operations
+
// ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
///
- /// NOTE: This may give wrong results, it hasn't been tested extensively
- /// If you're getting weird bugs, you may want to check this function out...
/// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative
/// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way.
///
- /// The Floor (rounded towards negative infinity)
+ /// Floor (rounded towards negative infinity)
/// Ceiling (rounded towards positive infinity)
- public void FloorCeiling(out BIM floor, out BIM ceiling)
- {
- BIM two = new BIM(2);
+ public void FloorCeiling(out BIM floor, out BIM ceiling) {
+ Contract.Requires(value == "");
+
+ BIM sig = significand;
+ BIM exp = exponent;
- BIM sig = Significand + BIM.Pow(two, SignificandSize); //Add hidden bit
- BIM exp = Exponent - BIM.Pow(two, ExponentSize-1) + 1;
+ BIM hiddenBitPow = BIM.Pow(2, significandSize - 1);
- while (exp > BIM.Zero) {
- exp--;
- sig = sig << 1;
+ if (exponent > 0) {
+ sig += hiddenBitPow;
+ } else {
+ ++exp;
}
- sig = sig >> SignificandSize;
+ exp -= (BIM.Pow(2, exponentSize - 1) - 1) + (significandSize - 1);
+
+ if (exp >= BIM.Zero) {
+ while (exp >= int.MaxValue) {
+ sig <<= int.MaxValue;
+ exp -= int.MaxValue;
+ }
+
+ sig <<= (int) exp;
+ floor = ceiling = (isSignBitSet ? -sig : sig);
+ } else {
+ exp = -exp;
- if (isNeg) {
- ceiling = -sig + 1;
- floor = -sig;
+ if (exp > significandSize) {
+ if (sig == 0) {
+ floor = ceiling = 0;
+ } else {
+ ceiling = isSignBitSet ? 0 : 1;
+ floor = ceiling - 1;
+ }
+ } else {
+ BIM frac = sig & ((BIM.One << (int) exp) - 1);
+ sig >>= (int) exp; //Guaranteed to fit in a 32-bit integer
+
+ if (frac == 0) {
+ floor = ceiling = (isSignBitSet ? -sig : sig);
+ } else {
+ ceiling = isSignBitSet ? -sig : sig + 1;
+ floor = ceiling - 1;
+ }
+ }
}
- else {
- ceiling = sig + 1;
- floor = sig;
+ }
+
+ public String ToBVString() {
+ if (value != "") {
+ return "_ " + value + " " + exponentSize + " " + significandSize;
+ } else if (value == "") {
+ return "fp (_ bv" + (isSignBitSet ? "1" : "0") + " 1) (_ bv" + exponent + " " + exponentSize + ") (_ bv" + significand + " " + (significandSize - 1) + ")";
+ } else {
+ return "(_ to_fp " + exponentSize + " " + significandSize + ") (_ bv" + value + " " + (exponentSize + significandSize).ToString() + ")";
}
}
+ ////////////////////////////////////////////////////////////////////////////
+ // Basic arithmetic operations
+
[Pure]
- public String ToDecimalString(int maxDigits) {
- //TODO: fix for fp functionality
- {
- throw new NotImplementedException();
+ public static BigFloat operator -(BigFloat x) {
+ if (x.value != "") {
+ if (x.value[0] == '-') {
+ return new BigFloat("+oo", x.significandSize, x.exponentSize);
+ }
+
+ if (x.value[0] == '+') {
+ return new BigFloat("-oo", x.significandSize, x.exponentSize);
+ }
+
+ return new BigFloat("NaN", x.significandSize, x.exponentSize);
}
+
+ return new BigFloat(!x.isSignBitSet, x.significand, x.exponent, x.significandSize, x.exponentSize);
}
- public String ToBVString(){
- if (this.IsSpecialType) {
- return "_ " + this.value + " " + this.exponentSize + " " + this.significandSize;
+ [Pure]
+ public static BigFloat operator +(BigFloat x, BigFloat y) {
+ Contract.Requires(x.exponentSize == y.exponentSize);
+ Contract.Requires(x.significandSize == y.significandSize);
+
+ if (x.value != "" || y.value != "") {
+ if (x.value == "NaN" || y.value == "NaN" || x.value == "+oo" && y.value == "-oo" || x.value == "-oo" && y.value == "+oo") {
+ return new BigFloat("NaN", x.significandSize, x.exponentSize);
+ }
+
+ if (x.value != "") {
+ return new BigFloat(x.value, x.significandSize, x.exponentSize);
+ }
+
+ return new BigFloat(y.value, y.significandSize, y.exponentSize);
}
- else if (this.Value == "") {
- return "fp (_ bv" + (this.isNeg ? "1" : "0") + " 1) (_ bv" + this.exponent + " " + this.exponentSize + ") (_ bv" + this.significand + " " + (this.significandSize-1) + ")";
+
+ if (x.exponent > y.exponent) {
+ BigFloat temp = x;
+ x = y;
+ y = temp;
}
- else {
- return "(_ to_fp " + this.exponentSize + " " + this.significandSize + ") (_ bv" + this.value + " " + (this.exponentSize + this.significandSize).ToString() + ")";
+
+ BIM xsig = x.significand, ysig = y.significand;
+ BIM xexp = x.exponent, yexp = y.exponent;
+
+ if (yexp - xexp > x.significandSize) //One of the numbers is relatively insignificant
+ {
+ return new BigFloat(y.isSignBitSet, y.significand, y.exponent, y.significandSize, y.exponentSize);
}
- }
- [Pure]
- public string ToDecimalString() {
- Contract.Ensures(Contract.Result() != null);
- return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;
- }
+ BIM hiddenBitPow = BIM.Pow(2, x.significandSize - 1);
- [Pure]
- public static string Zeros(int n) {
- //TODO: fix for fp functionality
- Contract.Requires(0 <= n);
- if (n <= 10) {
- var tenZeros = "0000000000";
- return tenZeros.Substring(0, n);
+ if (xexp > 0) {
+ xsig += hiddenBitPow;
} else {
- var d = n / 2;
- var s = Zeros(d);
- if (n % 2 == 0) {
- return s + s;
- } else {
- return s + s + "0";
- }
+ ++xexp;
}
- }
+ if (yexp > 0) {
+ ysig += hiddenBitPow;
+ } else {
+ ++yexp;
+ }
- ////////////////////////////////////////////////////////////////////////////
- // Basic arithmetic operations
+ if (x.isSignBitSet) {
+ xsig = -xsig;
+ }
+ if (y.isSignBitSet) {
+ ysig = -ysig;
+ }
- [Pure]
- public BigFloat Abs {
- get {
- return new BigFloat(true, Exponent, Significand, ExponentSize, SignificandSize);
+ xsig >>= (int) (yexp - xexp); //Guaranteed to fit in a 32-bit integer
+
+ ysig += xsig;
+
+ bool isNeg = ysig < 0;
+
+ ysig = BIM.Abs(ysig);
+
+ if (ysig == 0) {
+ return new BigFloat(x.isSignBitSet && y.isSignBitSet, 0, 0, x.significandSize, x.exponentSize);
}
- }
- [Pure]
- public BigFloat Negate {
- get {
- if (value != "")
- return value[0] == '-' ? new BigFloat(value.Remove(0, 1), ExponentSize, significandSize) : new BigFloat("-" + value, ExponentSize, significandSize);
- return new BigFloat(!isNeg, Exponent, Significand, ExponentSize, SignificandSize);
+ if (ysig >= hiddenBitPow * 2) {
+ ysig >>= 1;
+ ++yexp;
}
- }
- [Pure]
- public static BigFloat operator -(BigFloat x) {
- return x.Negate;
- }
+ while (ysig < hiddenBitPow && yexp > 1) {
+ ysig <<= 1;
+ --yexp;
+ }
- [Pure]
- public static BigFloat operator +(BigFloat x, BigFloat y) {
- //TODO: Modify for correct fp functionality
- Contract.Requires(x.ExponentSize == y.ExponentSize);
- Contract.Requires(x.significandSize == y.significandSize);
- BIM m1 = x.significand;
- BIM e1 = x.Exponent;
- BIM m2 = y.significand;
- BIM e2 = y.Exponent;
- m1 = m1 + two_n(x.significandSize + 1); //Add implicit bit
- m2 = m2 + two_n(y.significandSize + 1);
- if (e2 > e1) {
- m1 = y.significand;
- e1 = y.Exponent;
- m2 = x.significand;
- e2 = x.Exponent;
- }
-
- while (e2 < e1) {
- m2 = m2 / two;
- e2 = e2 + one;
+ if (ysig < hiddenBitPow) {
+ yexp = 0;
+ } else {
+ ysig -= hiddenBitPow;
}
- return new BigFloat(false, e1, m1 + m2, x.significandSize, x.ExponentSize);
+ if (yexp >= BIM.Pow(2, x.exponentSize) - 1) {
+ return new BigFloat(y.isSignBitSet ? "-oo" : "+oo", x.significandSize, x.exponentSize);
+ }
+
+ return new BigFloat(isNeg, ysig, yexp, x.significandSize, x.exponentSize);
}
[Pure]
public static BigFloat operator -(BigFloat x, BigFloat y) {
- return x + y.Negate;
+ return x + -y;
}
[Pure]
public static BigFloat operator *(BigFloat x, BigFloat y) {
- Contract.Requires(x.ExponentSize == y.ExponentSize);
+ Contract.Requires(x.exponentSize == y.exponentSize);
Contract.Requires(x.significandSize == y.significandSize);
- return new BigFloat(x.isNeg ^ y.isNeg, x.Exponent + y.Exponent, x.significand * y.significand, x.significandSize, x.ExponentSize);
- }
+ if (x.value == "NaN" || y.value == "NaN" || (x.value == "+oo" || x.value == "-oo") && y.IsZero || (y.value == "+oo" || y.value == "-oo") && x.IsZero) {
+ return new BigFloat("NaN", x.significandSize, x.exponentSize);
+ }
- ////////////////////////////////////////////////////////////////////////////
- // Some basic comparison operations
+ if (x.value != "" || y.value != "") {
+ bool xSignBitSet = x.value == "" ? x.isSignBitSet : x.value[0] == '-';
+ bool ySignBitSet = y.value == "" ? y.isSignBitSet : y.value[0] == '-';
+ return new BigFloat((xSignBitSet ^ ySignBitSet ? "-" : "+") + "oo", x.significandSize, x.exponentSize);
+ }
- public bool IsSpecialType {
- get {
- if (value == "")
- return false;
- return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("zero") || value.Equals("-zero"));
+ BIM xsig = x.significand, ysig = y.significand;
+ BIM xexp = x.exponent, yexp = y.exponent;
+
+ BIM hiddenBitPow = BIM.Pow(2, x.significandSize - 1);
+
+ if (xexp > 0) {
+ xsig += hiddenBitPow;
+ } else {
+ ++xexp;
}
- }
- public bool IsPositive {
- get {
- return !IsNegative;
+ if (yexp > 0) {
+ ysig += hiddenBitPow;
+ } else {
+ ++yexp;
+ }
+
+ ysig *= xsig;
+ yexp += xexp - (BIM.Pow(2, x.exponentSize - 1) - 1) - (x.significandSize - 1);
+
+ while (ysig >= hiddenBitPow * 2 || yexp <= 0) {
+ ysig >>= 1;
+ ++yexp;
+ }
+
+ while (ysig < hiddenBitPow && yexp > 1) {
+ ysig <<= 1;
+ --yexp;
+ }
+
+ if (ysig < hiddenBitPow) {
+ yexp = 0;
+ } else {
+ ysig -= hiddenBitPow;
+ }
+
+ if (yexp >= BIM.Pow(2, x.exponentSize) - 1) {
+ return new BigFloat(x.isSignBitSet ^ y.isSignBitSet ? "-oo" : "+oo", x.significandSize, x.exponentSize);
}
+
+ return new BigFloat(x.isSignBitSet ^ y.isSignBitSet, ysig, yexp, x.significandSize, x.exponentSize);
}
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Some basic comparison operations
+
public bool IsZero {
get {
- return significand.Equals(BigNum.ZERO) && Exponent == BIM.Zero;
+ return value == "" && significand.IsZero && exponent.IsZero;
}
}
+ ///
+ /// This method follows the specification for C#'s Single.CompareTo method.
+ /// As a result, it handles NaNs differently than how the ==, !=, <, >, <=, and >= operators do.
+ /// For example, the expression (0.0f / 0.0f).CompareTo(0.0f / 0.0f) should return 0,
+ /// whereas the expression (0.0f / 0.0f) == (0.0f / 0.0f) should return false.
+ ///
[Pure]
public int CompareTo(BigFloat that) {
- if (this.exponent > that.exponent)
- return 1;
- if (this.exponent < that.exponent)
- return -1;
- if (this.significand == that.significand)
+ Contract.Requires(exponentSize == that.exponentSize);
+ Contract.Requires(significandSize == that.significandSize);
+
+ if (value == "" && that.value == "") {
+ int cmpThis = IsZero ? 0 : isSignBitSet ? -1 : 1;
+ int cmpThat = that.IsZero ? 0 : that.isSignBitSet ? -1 : 1;
+
+ if (cmpThis == cmpThat) {
+ if (exponent == that.exponent) {
+ return cmpThis * significand.CompareTo(that.significand);
+ }
+
+ return cmpThis * exponent.CompareTo(that.exponent);
+ }
+
+ if (cmpThis == 0) {
+ return -cmpThat;
+ }
+
+ return cmpThis;
+ }
+
+ if (value == that.value) {
return 0;
- return this.significand > that.significand ? 1 : -1;
+ }
+
+ if (value == "NaN" || that.value == "+oo" || value == "-oo" && that.value != "NaN") {
+ return -1;
+ }
+
+ return 1;
}
[Pure]
public static bool operator ==(BigFloat x, BigFloat y) {
+ if (x.value == "NaN" || y.value == "NaN") {
+ return false;
+ }
+
return x.CompareTo(y) == 0;
}
[Pure]
public static bool operator !=(BigFloat x, BigFloat y) {
+ if (x.value == "NaN" || y.value == "NaN") {
+ return true;
+ }
+
return x.CompareTo(y) != 0;
}
[Pure]
public static bool operator <(BigFloat x, BigFloat y) {
+ if (x.value == "NaN" || y.value == "NaN") {
+ return false;
+ }
+
return x.CompareTo(y) < 0;
}
[Pure]
public static bool operator >(BigFloat x, BigFloat y) {
+ if (x.value == "NaN" || y.value == "NaN") {
+ return false;
+ }
+
return x.CompareTo(y) > 0;
}
[Pure]
public static bool operator <=(BigFloat x, BigFloat y) {
+ if (x.value == "NaN" || y.value == "NaN") {
+ return false;
+ }
+
return x.CompareTo(y) <= 0;
}
[Pure]
public static bool operator >=(BigFloat x, BigFloat y) {
+ if (x.value == "NaN" || y.value == "NaN") {
+ return false;
+ }
+
return x.CompareTo(y) >= 0;
}
}
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/Basetypes/RoundingMode.cs boogie-2.4.1+dfsg/Source/Basetypes/RoundingMode.cs
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/Basetypes/RoundingMode.cs 1970-01-01 00:00:00.000000000 +0000
+++ boogie-2.4.1+dfsg/Source/Basetypes/RoundingMode.cs 2019-10-25 18:17:05.000000000 +0000
@@ -0,0 +1,75 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Basetypes
+{
+
+ ///
+ /// A representation of a rounding mode
+ ///
+ public class RoundingMode
+ {
+ private string val;
+
+ public static readonly RoundingMode RNE = new RoundingMode("RNE");
+ public static readonly RoundingMode RNA = new RoundingMode("RNA");
+ public static readonly RoundingMode RTP = new RoundingMode("RTP");
+ public static readonly RoundingMode RTN = new RoundingMode("RTN");
+ public static readonly RoundingMode RTZ = new RoundingMode("RTZ");
+
+ private RoundingMode(string val)
+ {
+ this.val = val;
+ }
+
+ [Pure]
+ public static RoundingMode FromString(String s)
+ {
+ if (s.Equals("RNE") || s.Equals("roundNearestTiesToEven")) return RNE;
+ if (s.Equals("RNA") || s.Equals("roundNearestTiesToAway")) return RNA;
+ if (s.Equals("RTP") || s.Equals("roundTowardPositive")) return RTP;
+ if (s.Equals("RTN") || s.Equals("roundTowardNegative")) return RTN;
+ if (s.Equals("RTZ") || s.Equals("roundTowardZero")) return RTZ;
+ throw new FormatException(s + " is not a valid rounding mode.");
+ }
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj)
+ {
+ RoundingMode rm = obj as RoundingMode;
+ return rm != null && this == rm;
+ }
+
+ [Pure]
+ public override int GetHashCode()
+ {
+ return val.GetHashCode();
+ }
+
+ [Pure]
+ public override string/*!*/ ToString()
+ {
+ Contract.Ensures(Contract.Result() != null);
+ return val;
+ }
+
+ [Pure]
+ public static bool operator ==(RoundingMode a, RoundingMode b)
+ {
+ return a.val.Equals(b.val);
+ }
+
+ [Pure]
+ public static bool operator !=(RoundingMode a, RoundingMode b)
+ {
+ return !a.val.Equals(b.val);
+ }
+ }
+}
\ No newline at end of file
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/BoogieDriver/app.config boogie-2.4.1+dfsg/Source/BoogieDriver/app.config
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/BoogieDriver/app.config 1970-01-01 00:00:00.000000000 +0000
+++ boogie-2.4.1+dfsg/Source/BoogieDriver/app.config 2019-10-25 18:17:05.000000000 +0000
@@ -0,0 +1,3 @@
+
+
+
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/BoogieDriver/BoogieDriver.csproj boogie-2.4.1+dfsg/Source/BoogieDriver/BoogieDriver.csproj
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/BoogieDriver/BoogieDriver.csproj 2016-10-30 01:53:09.000000000 +0000
+++ boogie-2.4.1+dfsg/Source/BoogieDriver/BoogieDriver.csproj 2019-10-25 18:17:05.000000000 +0000
@@ -10,7 +10,7 @@
Properties
BoogieDriver
Boogie
- v4.0
+ v4.5
512
1
true
@@ -74,6 +74,7 @@
Full
%28none%29
AllRules.ruleset
+ false
pdbonly
@@ -83,6 +84,7 @@
prompt
4
AllRules.ruleset
+ false
true
@@ -99,6 +101,7 @@
true
4
false
+ false
true
@@ -141,6 +144,7 @@
0
4
false
+ false
true
@@ -158,6 +162,7 @@
;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
4
false
+ false
bin\x86\Release\
@@ -175,6 +180,7 @@
;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
false
4
+ false
true
@@ -192,6 +198,7 @@
true
4
false
+ false
true
@@ -210,6 +217,7 @@
false
4
false
+ false
true
@@ -219,6 +227,7 @@
AnyCPU
prompt
AllRules.ruleset
+ false
true
@@ -229,6 +238,7 @@
prompt
AllRules.ruleset
false
+ false
@@ -313,6 +323,9 @@
true
+
+
+
-
+
\ No newline at end of file
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/CodeContractsExtender/CodeContractsExtender.csproj boogie-2.4.1+dfsg/Source/CodeContractsExtender/CodeContractsExtender.csproj
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/CodeContractsExtender/CodeContractsExtender.csproj 2016-10-30 01:53:09.000000000 +0000
+++ boogie-2.4.1+dfsg/Source/CodeContractsExtender/CodeContractsExtender.csproj 2019-10-25 18:17:05.000000000 +0000
@@ -10,7 +10,7 @@
Properties
CodeContractsExtender
BoogieCodeContractsExtender
- v4.0
+ v4.5
512
true
..\InterimKey.snk
@@ -34,7 +34,7 @@
false
false
true
- Client
+
true
@@ -74,6 +74,7 @@
Full
%28none%29
AllRules.ruleset
+ false
pdbonly
@@ -83,6 +84,7 @@
prompt
4
AllRules.ruleset
+ false
true
@@ -99,6 +101,7 @@
true
4
false
+ false
true
@@ -141,6 +144,7 @@
0
4
false
+ false
true
@@ -150,6 +154,7 @@
AnyCPU
prompt
AllRules.ruleset
+ false
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/CodeContractsExtender/CodeContractsExtender-NetCore.csproj boogie-2.4.1+dfsg/Source/CodeContractsExtender/CodeContractsExtender-NetCore.csproj
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/CodeContractsExtender/CodeContractsExtender-NetCore.csproj 1970-01-01 00:00:00.000000000 +0000
+++ boogie-2.4.1+dfsg/Source/CodeContractsExtender/CodeContractsExtender-NetCore.csproj 2019-10-25 18:17:05.000000000 +0000
@@ -0,0 +1,11 @@
+
+
+
+ Library
+ BoogieCodeContractsExtender
+ netcoreapp2.2
+ COREFX_SUBSET
+ false
+
+
+
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/Concurrency/App.config boogie-2.4.1+dfsg/Source/Concurrency/App.config
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/Concurrency/App.config 2016-10-30 01:53:09.000000000 +0000
+++ boogie-2.4.1+dfsg/Source/Concurrency/App.config 2019-10-25 18:17:05.000000000 +0000
@@ -1,6 +1,6 @@
-
+
diff -Nru boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/Concurrency/CivlRefinement.cs boogie-2.4.1+dfsg/Source/Concurrency/CivlRefinement.cs
--- boogie-2.3.0.61016+dfsg+3.gbp1f2d6c1/Source/Concurrency/CivlRefinement.cs 2016-10-30 01:53:09.000000000 +0000
+++ boogie-2.4.1+dfsg/Source/Concurrency/CivlRefinement.cs 1970-01-01 00:00:00.000000000 +0000
@@ -1,1230 +0,0 @@
-using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Threading.Tasks;
-using Microsoft.Boogie;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using Microsoft.Boogie.GraphUtil;
-
-namespace Microsoft.Boogie
-{
- public class MyDuplicator : Duplicator
- {
- CivlTypeChecker civlTypeChecker;
- public int layerNum;
- Procedure enclosingProc;
- Implementation enclosingImpl;
- public Dictionary procMap; /* Original -> Duplicate */
- public Dictionary absyMap; /* Duplicate -> Original */
- public Dictionary implMap; /* Duplicate -> Original */
- public HashSet yieldingProcs;
- public List impls;
-
- public MyDuplicator(CivlTypeChecker civlTypeChecker, int layerNum)
- {
- this.civlTypeChecker = civlTypeChecker;
- this.layerNum = layerNum;
- this.enclosingProc = null;
- this.enclosingImpl = null;
- this.procMap = new Dictionary();
- this.absyMap = new Dictionary();
- this.implMap = new Dictionary();
- this.yieldingProcs = new HashSet();
- this.impls = new List();
- }
-
- private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List newCmds)
- {
- int enclosingProcLayerNum = civlTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;
- Procedure originalProc = originalCallCmd.Proc;
-
- if (civlTypeChecker.procToAtomicProcedureInfo.ContainsKey(originalProc))
- {
- if (civlTypeChecker.CallExists(originalCallCmd, enclosingProcLayerNum, layerNum))
- {
- newCmds.Add(callCmd);
- }
- }
- else if (civlTypeChecker.procToActionInfo.ContainsKey(originalProc))
- {
- AtomicActionInfo atomicActionInfo = civlTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo;
- if (atomicActionInfo != null && atomicActionInfo.gate.Count > 0 && layerNum == enclosingProcLayerNum)
- {
- newCmds.Add(new HavocCmd(Token.NoToken, new List(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) })));
- Dictionary map = new Dictionary();
- for (int i = 0; i < originalProc.InParams.Count; i++)
- {
- map[originalProc.InParams[i]] = callCmd.Ins[i];
- }
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- foreach (AssertCmd assertCmd in atomicActionInfo.gate)
- {
- newCmds.Add(Substituter.Apply(subst, assertCmd));
- }
- }
- newCmds.Add(callCmd);
- }
- else
- {
- Debug.Assert(false);
- }
- }
-
- private void ProcessParCallCmd(ParCallCmd originalParCallCmd, ParCallCmd parCallCmd, List newCmds)
- {
- int maxCalleeLayerNum = 0;
- foreach (CallCmd iter in originalParCallCmd.CallCmds)
- {
- int calleeLayerNum = civlTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum;
- if (calleeLayerNum > maxCalleeLayerNum)
- maxCalleeLayerNum = calleeLayerNum;
- }
- if (layerNum > maxCalleeLayerNum)
- {
- for (int i = 0; i < parCallCmd.CallCmds.Count; i++)
- {
- ProcessCallCmd(originalParCallCmd.CallCmds[i], parCallCmd.CallCmds[i], newCmds);
- absyMap[parCallCmd.CallCmds[i]] = originalParCallCmd;
- }
- }
- else
- {
- newCmds.Add(parCallCmd);
- }
- }
-
- public override List VisitCmdSeq(List cmdSeq)
- {
- List cmds = base.VisitCmdSeq(cmdSeq);
- List newCmds = new List();
- for (int i = 0; i < cmds.Count; i++)
- {
- Cmd originalCmd = cmdSeq[i];
- Cmd cmd = cmds[i];
-
- CallCmd originalCallCmd = originalCmd as CallCmd;
- if (originalCallCmd != null)
- {
- ProcessCallCmd(originalCallCmd, cmd as CallCmd, newCmds);
- continue;
- }
-
- ParCallCmd originalParCallCmd = originalCmd as ParCallCmd;
- if (originalParCallCmd != null)
- {
- ProcessParCallCmd(originalParCallCmd, cmd as ParCallCmd, newCmds);
- continue;
- }
-
- newCmds.Add(cmd);
- }
- return newCmds;
- }
-
- public override YieldCmd VisitYieldCmd(YieldCmd node)
- {
- YieldCmd yieldCmd = base.VisitYieldCmd(node);
- absyMap[yieldCmd] = node;
- return yieldCmd;
- }
-
- public override Block VisitBlock(Block node)
- {
- Block block = base.VisitBlock(node);
- absyMap[block] = node;
- return block;
- }
-
- public override Cmd VisitCallCmd(CallCmd node)
- {
- CallCmd callCmd = (CallCmd) base.VisitCallCmd(node);
- callCmd.Proc = VisitProcedure(callCmd.Proc);
- callCmd.callee = callCmd.Proc.Name;
- absyMap[callCmd] = node;
- return callCmd;
- }
-
- public override Cmd VisitParCallCmd(ParCallCmd node)
- {
- ParCallCmd parCallCmd = (ParCallCmd) base.VisitParCallCmd(node);
- absyMap[parCallCmd] = node;
- return parCallCmd;
- }
-
- public override Procedure VisitProcedure(Procedure node)
- {
- if (!civlTypeChecker.procToActionInfo.ContainsKey(node))
- return node;
- if (!procMap.ContainsKey(node))
- {
- enclosingProc = node;
- Procedure proc = (Procedure)node.Clone();
- proc.Name = string.Format("{0}_{1}", node.Name, layerNum);
- proc.InParams = this.VisitVariableSeq(node.InParams);
- proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies);
- proc.OutParams = this.VisitVariableSeq(node.OutParams);
-
- ActionInfo actionInfo = civlTypeChecker.procToActionInfo[node];
- if (actionInfo.createdAtLayerNum < layerNum)
- {
- proc.Requires = new List();
- proc.Ensures = new List();
- Implementation impl;
- AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
- if (atomicActionInfo != null)
- {
- CodeExpr action = (CodeExpr)VisitCodeExpr(atomicActionInfo.action);
- List cmds = new List();
- foreach (AssertCmd assertCmd in atomicActionInfo.gate)
- {
- cmds.Add(new AssumeCmd(Token.NoToken, (Expr)Visit(assertCmd.Expr)));
- }
- Block newInitBlock = new Block(Token.NoToken, "_init", cmds,
- new GotoCmd(Token.NoToken, new List(new string[] { action.Blocks[0].Label }),
- new List(new Block[] { action.Blocks[0] })));
- List newBlocks = new List();
- newBlocks.Add(newInitBlock);
- newBlocks.AddRange(action.Blocks);
- impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, action.LocVars, newBlocks);
- }
- else
- {
- Block newInitBlock = new Block(Token.NoToken, "_init", new List(), new ReturnCmd(Token.NoToken));
- List newBlocks = new List();
- newBlocks.Add(newInitBlock);
- impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, new List(), newBlocks);
- }
- impl.Proc = proc;
- impl.Proc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- impl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- impls.Add(impl);
- }
- else
- {
- yieldingProcs.Add(proc);
- proc.Requires = this.VisitRequiresSeq(node.Requires);
- proc.Ensures = this.VisitEnsuresSeq(node.Ensures);
- }
- procMap[node] = proc;
- proc.Modifies = new List();
- civlTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));
- }
- return procMap[node];
- }
-
- private Variable dummyLocalVar;
- public override Implementation VisitImplementation(Implementation node)
- {
- enclosingImpl = node;
- dummyLocalVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_dummy", Type.Bool));
- Implementation impl = base.VisitImplementation(node);
- implMap[impl] = node;
- impl.LocVars.Add(dummyLocalVar);
- impl.Name = impl.Proc.Name;
- return impl;
- }
-
- public override Requires VisitRequires(Requires node)
- {
- Requires requires = base.VisitRequires(node);
- if (node.Free)
- return requires;
- if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum))
- requires.Condition = Expr.True;
- return requires;
- }
-
- public override Ensures VisitEnsures(Ensures node)
- {
- Ensures ensures = base.VisitEnsures(node);
- if (node.Free)
- return ensures;
- AtomicActionInfo atomicActionInfo = civlTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo;
- bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node;
- if (isAtomicSpecification || !civlTypeChecker.absyToLayerNums[node].Contains(layerNum))
- {
- ensures.Condition = Expr.True;
- ensures.Attributes = CivlRefinement.RemoveMoverAttribute(ensures.Attributes);
- }
- return ensures;
- }
-
- public override Cmd VisitAssertCmd(AssertCmd node)
- {
- AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node);
- if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum))
- assertCmd.Expr = Expr.True;
- return assertCmd;
- }
- }
-
- public class CivlRefinement
- {
- LinearTypeChecker linearTypeChecker;
- CivlTypeChecker civlTypeChecker;
- Dictionary absyMap;
- Dictionary implMap;
- HashSet yieldingProcs;
- int layerNum;
- List globalMods;
- Dictionary asyncAndParallelCallDesugarings;
- List yieldCheckerProcs;
- List yieldCheckerImpls;
- Procedure yieldProc;
-
- Variable pc;
- Variable ok;
- Expr alpha;
- Expr beta;
- HashSet frame;
-
- public CivlRefinement(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, MyDuplicator duplicator)
- {
- this.linearTypeChecker = linearTypeChecker;
- this.civlTypeChecker = civlTypeChecker;
- this.absyMap = duplicator.absyMap;
- this.layerNum = duplicator.layerNum;
- this.implMap = duplicator.implMap;
- this.yieldingProcs = duplicator.yieldingProcs;
- Program program = linearTypeChecker.program;
- globalMods = new List();
- foreach (Variable g in civlTypeChecker.SharedVariables)
- {
- globalMods.Add(Expr.Ident(g));
- }
- asyncAndParallelCallDesugarings = new Dictionary();
- yieldCheckerProcs = new List();
- yieldCheckerImpls = new List();
- yieldProc = null;
- }
-
- private IEnumerable AvailableLinearVars(Absy absy)
- {
- HashSet availableVars = new HashSet(linearTypeChecker.AvailableLinearVars(absyMap[absy]));
- foreach (var g in civlTypeChecker.globalVarToSharedVarInfo.Keys)
- {
- SharedVariableInfo info = civlTypeChecker.globalVarToSharedVarInfo[g];
- if (!(info.introLayerNum <= layerNum && layerNum <= info.hideLayerNum))
- {
- availableVars.Remove(g);
- }
- }
- foreach (var v in civlTypeChecker.localVarToLocalVariableInfo.Keys)
- {
- LocalVariableInfo info = civlTypeChecker.localVarToLocalVariableInfo[v];
- if (layerNum < info.layer)
- {
- availableVars.Remove(v);
- }
- }
- return availableVars;
- }
-
- private CallCmd CallToYieldProc(IToken tok, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar)
- {
- List exprSeq = new List();
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName]));
- }
- foreach (IdentifierExpr ie in globalMods)
- {
- exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl]));
- }
- if (yieldProc == null)
- {
- List inputs = new List();
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- var domain = linearTypeChecker.linearDomains[domainName];
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List(), new List { domain.elementType }, Type.Bool)), true);
- inputs.Add(f);
- }
- foreach (IdentifierExpr ie in globalMods)
- {
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);
- inputs.Add(f);
- }
- yieldProc = new Procedure(Token.NoToken, string.Format("og_yield_{0}", layerNum), new List(), inputs, new List(), new List(), new List(), new List());
- yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- }
- CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List());
- yieldCallCmd.Proc = yieldProc;
- return yieldCallCmd;
- }
-
- private void AddCallToYieldProc(IToken tok, List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar)
- {
- if (!CommandLineOptions.Clo.TrustNonInterference)
- {
- CallCmd yieldCallCmd = CallToYieldProc(tok, ogOldGlobalMap, domainNameToLocalVar);
- newCmds.Add(yieldCallCmd);
- }
-
- if (pc != null)
- {
- Expr aa = OldEqualityExprForGlobals(ogOldGlobalMap);
- Expr bb = OldEqualityExpr(ogOldGlobalMap);
-
- // assert pc || g_old == g || beta(i, g_old, o, g);
- Expr assertExpr = Expr.Or(Expr.Ident(pc), Expr.Or(aa, beta));
- assertExpr.Typecheck(new TypecheckingContext(null));
- AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, assertExpr);
- skipOrBetaAssertCmd.ErrorData = "Transition invariant in initial state violated";
- newCmds.Add(skipOrBetaAssertCmd);
-
- // assert pc ==> o_old == o && g_old == g;
- assertExpr = Expr.Imp(Expr.Ident(pc), bb);
- assertExpr.Typecheck(new TypecheckingContext(null));
- AssertCmd skipAssertCmd = new AssertCmd(tok, assertExpr);
- skipAssertCmd.ErrorData = "Transition invariant in final state violated"; ;
- newCmds.Add(skipAssertCmd);
-
- // pc, ok := g_old == g ==> pc, ok || beta(i, g_old, o, g);
- List pcUpdateLHS = new List(
- new AssignLhs[] {
- new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)),
- new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok))
- });
- List pcUpdateRHS = new List(
- new Expr[] {
- Expr.Imp(aa, Expr.Ident(pc)),
- Expr.Or(Expr.Ident(ok), beta)
- });
- foreach (Expr e in pcUpdateRHS)
- {
- e.Typecheck(new TypecheckingContext(null));
- }
- newCmds.Add(new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS));
- }
- }
-
- private Dictionary ComputeAvailableExprs(IEnumerable availableLinearVars, Dictionary domainNameToInputVar)
- {
- Dictionary domainNameToExpr = new Dictionary();
- foreach (var domainName in linearTypeChecker.linearDomains.Keys)
- {
- var expr = Expr.Ident(domainNameToInputVar[domainName]);
- expr.Resolve(new ResolutionContext(null));
- expr.Typecheck(new TypecheckingContext(null));
- domainNameToExpr[domainName] = expr;
- }
- foreach (Variable v in availableLinearVars)
- {
- var domainName = linearTypeChecker.FindDomainName(v);
- if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
- var domain = linearTypeChecker.linearDomains[domainName];
- if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;
- Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List { Expr.Ident(v) });
- var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { ie, domainNameToExpr[domainName] });
- expr.Resolve(new ResolutionContext(null));
- expr.Typecheck(new TypecheckingContext(null));
- domainNameToExpr[domainName] = expr;
- }
- return domainNameToExpr;
- }
-
- private void AddUpdatesToOldGlobalVars(List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar, Dictionary domainNameToExpr)
- {
- List lhss = new List();
- List rhss = new List();
- foreach (var domainName in linearTypeChecker.linearDomains.Keys)
- {
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName])));
- rhss.Add(domainNameToExpr[domainName]);
- }
- foreach (Variable g in ogOldGlobalMap.Keys)
- {
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g])));
- rhss.Add(Expr.Ident(g));
- }
- if (lhss.Count > 0)
- {
- newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
- }
- }
-
- private Expr OldEqualityExpr(Dictionary ogOldGlobalMap)
- {
- Expr bb = Expr.True;
- foreach (Variable o in ogOldGlobalMap.Keys)
- {
- if (o is GlobalVariable && !frame.Contains(o)) continue;
- bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));
- bb.Type = Type.Bool;
- }
- return bb;
- }
-
- private Expr OldEqualityExprForGlobals(Dictionary ogOldGlobalMap)
- {
- Expr bb = Expr.True;
- foreach (Variable o in ogOldGlobalMap.Keys)
- {
- if (o is GlobalVariable && frame.Contains(o))
- {
- bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));
- bb.Type = Type.Bool;
- }
- }
- return bb;
- }
-
- private void DesugarYield(YieldCmd yieldCmd, List cmds, List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar)
- {
- AddCallToYieldProc(yieldCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
-
- if (globalMods.Count > 0)
- {
- newCmds.Add(new HavocCmd(Token.NoToken, globalMods));
- if (pc != null)
- {
- // assume pc || alpha(i, g);
- Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
- assumeExpr.Type = Type.Bool;
- newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
- }
- }
-
- Dictionary domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(yieldCmd), domainNameToInputVar);
- AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
-
- for (int j = 0; j < cmds.Count; j++)
- {
- PredicateCmd predCmd = (PredicateCmd)cmds[j];
- newCmds.Add(new AssumeCmd(Token.NoToken, predCmd.Expr));
- }
- }
-
- public void DesugarParallelCallCmd(List newCmds, ParCallCmd parCallCmd)
- {
- List parallelCalleeNames = new List();
- List ins = new List();
- List outs = new List();
- string procName = "og";
- foreach (CallCmd callCmd in parCallCmd.CallCmds)
- {
- procName = procName + "_" + callCmd.Proc.Name;
- ins.AddRange(callCmd.Ins);
- outs.AddRange(callCmd.Outs);
- }
- Procedure proc;
- if (asyncAndParallelCallDesugarings.ContainsKey(procName))
- {
- proc = asyncAndParallelCallDesugarings[procName];
- }
- else
- {
- List inParams = new List();
- List outParams = new List();
- List requiresSeq = new List();
- List ensuresSeq = new List();
- int count = 0;
- foreach (CallCmd callCmd in parCallCmd.CallCmds)
- {
- Dictionary map = new Dictionary();
- foreach (Variable x in callCmd.Proc.InParams)
- {
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), true);
- inParams.Add(y);
- map[x] = Expr.Ident(y);
- }
- foreach (Variable x in callCmd.Proc.OutParams)
- {
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), false);
- outParams.Add(y);
- map[x] = Expr.Ident(y);
- }
- Contract.Assume(callCmd.Proc.TypeParameters.Count == 0);
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- foreach (Requires req in callCmd.Proc.Requires)
- {
- requiresSeq.Add(new Requires(req.tok, req.Free, Substituter.Apply(subst, req.Condition), null, req.Attributes));
- }
- foreach (Ensures ens in callCmd.Proc.Ensures)
- {
- ensuresSeq.Add(new Ensures(ens.tok, ens.Free, Substituter.Apply(subst, ens.Condition), null, ens.Attributes));
- }
- count++;
- }
- proc = new Procedure(Token.NoToken, procName, new List(), inParams, outParams, requiresSeq, globalMods, ensuresSeq);
- asyncAndParallelCallDesugarings[procName] = proc;
- }
- CallCmd dummyCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes);
- dummyCallCmd.Proc = proc;
- newCmds.Add(dummyCallCmd);
- }
-
- private void CreateYieldCheckerImpl(Implementation impl, List> yields)
- {
- if (yields.Count == 0) return;
-
- Dictionary map = new Dictionary();
- foreach (Variable local in impl.LocVars)
- {
- var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type));
- map[local] = Expr.Ident(copy);
- }
-
- Program program = linearTypeChecker.program;
- List locals = new List();
- List inputs = new List();
- foreach (IdentifierExpr ie in map.Values)
- {
- locals.Add(ie.Decl);
- }
- for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
- {
- Variable inParam = impl.InParams[i];
- Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
- locals.Add(copy);
- map[impl.InParams[i]] = Expr.Ident(copy);
- }
- {
- int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count;
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- Variable inParam = impl.InParams[i];
- Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true);
- inputs.Add(copy);
- map[impl.InParams[i]] = Expr.Ident(copy);
- i++;
- }
- }
- for (int i = 0; i < impl.OutParams.Count; i++)
- {
- Variable outParam = impl.OutParams[i];
- var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type));
- locals.Add(copy);
- map[impl.OutParams[i]] = Expr.Ident(copy);
- }
- Dictionary ogOldLocalMap = new Dictionary();
- Dictionary assumeMap = new Dictionary(map);
- foreach (IdentifierExpr ie in globalMods)
- {
- Variable g = ie.Decl;
- var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_local_old_{0}", g.Name), g.TypedIdent.Type));
- locals.Add(copy);
- ogOldLocalMap[g] = Expr.Ident(copy);
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type), true);
- inputs.Add(f);
- assumeMap[g] = Expr.Ident(f);
- }
-
- Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap);
- Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap);
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- List yieldCheckerBlocks = new List();
- List labels = new List();
- List labelTargets = new List();
- Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List(), new ReturnCmd(Token.NoToken));
- labels.Add(yieldCheckerBlock.Label);
- labelTargets.Add(yieldCheckerBlock);
- yieldCheckerBlocks.Add(yieldCheckerBlock);
- int yieldCount = 0;
- foreach (List cs in yields)
- {
- List newCmds = new List();
- foreach (Cmd cmd in cs)
- {
- PredicateCmd predCmd = (PredicateCmd)cmd;
- newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr)));
- }
- foreach (Cmd cmd in cs)
- {
- PredicateCmd predCmd = (PredicateCmd)cmd;
- var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);
- if (predCmd is AssertCmd)
- {
- AssertCmd assertCmd = new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes);
- assertCmd.ErrorData = "Non-interference check failed";
- newCmds.Add(assertCmd);
- }
- else
- {
- newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));
- }
- }
- newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
- yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken));
- labels.Add(yieldCheckerBlock.Label);
- labelTargets.Add(yieldCheckerBlock);
- yieldCheckerBlocks.Add(yieldCheckerBlock);
- }
- yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List(), new GotoCmd(Token.NoToken, labels, labelTargets)));
-
- // Create the yield checker procedure
- var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", "Impl", impl.Name);
- var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List(), new List(), new List(), new List());
- yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- yieldCheckerProcs.Add(yieldCheckerProc);
-
- // Create the yield checker implementation
- var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List(), locals, yieldCheckerBlocks);
- yieldCheckerImpl.Proc = yieldCheckerProc;
- yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- yieldCheckerImpls.Add(yieldCheckerImpl);
- }
-
- private bool IsYieldingHeader(Graph graph, Block header)
- {
- foreach (Block backEdgeNode in graph.BackEdgeNodes(header))
- {
- foreach (Block x in graph.NaturalLoops(header, backEdgeNode))
- {
- foreach (Cmd cmd in x.Cmds)
- {
- if (cmd is YieldCmd)
- return true;
- if (cmd is ParCallCmd)
- return true;
- CallCmd callCmd = cmd as CallCmd;
- if (callCmd == null) continue;
- if (yieldingProcs.Contains(callCmd.Proc))
- return true;
- }
- }
- }
- return false;
- }
-
- private Graph ComputeYieldingLoopHeaders(Implementation impl, out HashSet yieldingHeaders)
- {
- Graph graph;
- impl.PruneUnreachableBlocks();
- impl.ComputePredecessorsForBlocks();
- graph = Program.GraphFromImpl(impl);
- graph.ComputeLoops();
- if (!graph.Reducible)
- {
- throw new Exception("Irreducible flow graphs are unsupported.");
- }
- yieldingHeaders = new HashSet();
- IEnumerable sortedHeaders = graph.SortHeadersByDominance();
- foreach (Block header in sortedHeaders)
- {
- if (yieldingHeaders.Any(x => graph.DominatorMap.DominatedBy(x, header)))
- {
- yieldingHeaders.Add(header);
- }
- else if (IsYieldingHeader(graph, header))
- {
- yieldingHeaders.Add(header);
- }
- else
- {
- continue;
- }
- }
- return graph;
- }
-
- private void SetupRefinementCheck(Implementation impl,
- out List newLocalVars,
- out Dictionary domainNameToInputVar, out Dictionary domainNameToLocalVar, out Dictionary ogOldGlobalMap)
- {
- pc = null;
- ok = null;
- alpha = null;
- beta = null;
- frame = null;
-
- newLocalVars = new List();
- Program program = linearTypeChecker.program;
- ogOldGlobalMap = new Dictionary();
- foreach (IdentifierExpr ie in globalMods)
- {
- Variable g = ie.Decl;
- LocalVariable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type));
- ogOldGlobalMap[g] = l;
- newLocalVars.Add(l);
- }
-
- Procedure originalProc = implMap[impl].Proc;
- ActionInfo actionInfo = civlTypeChecker.procToActionInfo[originalProc];
- if (actionInfo.createdAtLayerNum == this.layerNum)
- {
- pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool));
- newLocalVars.Add(pc);
- ok = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_ok", Type.Bool));
- newLocalVars.Add(ok);
- Dictionary alwaysMap = new Dictionary();
- for (int i = 0; i < originalProc.InParams.Count; i++)
- {
- alwaysMap[originalProc.InParams[i]] = Expr.Ident(impl.InParams[i]);
- }
- for (int i = 0; i < originalProc.OutParams.Count; i++)
- {
- alwaysMap[originalProc.OutParams[i]] = Expr.Ident(impl.OutParams[i]);
- }
- Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap);
- Dictionary foroldMap = new Dictionary();
- foreach (IdentifierExpr ie in globalMods)
- {
- foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);
- }
- Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);
- frame = new HashSet(civlTypeChecker.SharedVariables);
- foreach (Variable v in civlTypeChecker.SharedVariables)
- {
- if (civlTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum ||
- civlTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum)
- {
- frame.Remove(v);
- }
- }
- AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
- if (atomicActionInfo == null)
- {
- beta = Expr.True;
- foreach (var v in frame)
- {
- beta = Expr.And(beta, Expr.Eq(Expr.Ident(v), foroldMap[v]));
- }
- alpha = Expr.True;
- }
- else
- {
- Expr betaExpr = (new MoverCheck.TransitionRelationComputation(civlTypeChecker.program, atomicActionInfo, frame, new HashSet())).TransitionRelationCompute(true);
- beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr);
- Expr alphaExpr = Expr.True;
- foreach (AssertCmd assertCmd in atomicActionInfo.gate)
- {
- alphaExpr = Expr.And(alphaExpr, assertCmd.Expr);
- alphaExpr.Type = Type.Bool;
- }
- alpha = Substituter.Apply(always, alphaExpr);
- }
- foreach (Variable f in impl.OutParams)
- {
- LocalVariable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_old_{0}", f.Name), f.TypedIdent.Type));
- newLocalVars.Add(copy);
- ogOldGlobalMap[f] = copy;
- }
- }
-
- domainNameToInputVar = new Dictionary();
- domainNameToLocalVar = new Dictionary();
- {
- int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count;
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- Variable inParam = impl.InParams[i];
- domainNameToInputVar[domainName] = inParam;
- Variable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name + "_local", inParam.TypedIdent.Type));
- domainNameToLocalVar[domainName] = l;
- newLocalVars.Add(l);
- i++;
- }
- }
- }
-
- private void TransformImpl(Implementation impl)
- {
- HashSet yieldingHeaders;
- Graph graph = ComputeYieldingLoopHeaders(impl, out yieldingHeaders);
-
- List newLocalVars;
- Dictionary domainNameToInputVar, domainNameToLocalVar;
- Dictionary ogOldGlobalMap;
- SetupRefinementCheck(impl, out newLocalVars, out domainNameToInputVar, out domainNameToLocalVar, out ogOldGlobalMap);
-
- List> yields = CollectAndDesugarYields(impl, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap);
-
- List oldPcs, oldOks;
- ProcessLoopHeaders(impl, graph, yieldingHeaders, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap, out oldPcs, out oldOks);
-
- AddInitialBlock(impl, oldPcs, oldOks, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap);
-
- CreateYieldCheckerImpl(impl, yields);
-
- impl.LocVars.AddRange(newLocalVars);
- impl.LocVars.AddRange(oldPcs);
- impl.LocVars.AddRange(oldOks);
-
- UnifyCallsToYieldProc(impl, ogOldGlobalMap, domainNameToLocalVar);
- }
-
- private void UnifyCallsToYieldProc(Implementation impl, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar)
- {
- CallCmd yieldCallCmd = CallToYieldProc(Token.NoToken, ogOldGlobalMap, domainNameToLocalVar);
- Block yieldCheckBlock = new Block(Token.NoToken, "CallToYieldProc", new List(new Cmd[] { yieldCallCmd, new AssumeCmd(Token.NoToken, Expr.False) }), new ReturnCmd(Token.NoToken));
- List newBlocks = new List();
- foreach (Block b in impl.Blocks)
- {
- TransferCmd transferCmd = b.TransferCmd;
- List newCmds = new List();
- for (int i = b.Cmds.Count-1; i >= 0; i--)
- {
- CallCmd callCmd = b.Cmds[i] as CallCmd;
- if (callCmd == null || callCmd.Proc != yieldProc)
- {
- newCmds.Insert(0, b.Cmds[i]);
- }
- else
- {
- Block newBlock = new Block(Token.NoToken, b.Label + i, newCmds, transferCmd);
- newCmds = new List();
- transferCmd = new GotoCmd(Token.NoToken, new List(new string[] { newBlock.Label, yieldCheckBlock.Label }),
- new List(new Block[] { newBlock, yieldCheckBlock }));
- newBlocks.Add(newBlock);
- }
- }
- b.Cmds = newCmds;
- b.TransferCmd = transferCmd;
- }
- impl.Blocks.AddRange(newBlocks);
- impl.Blocks.Add(yieldCheckBlock);
- }
-
- private List> CollectAndDesugarYields(Implementation impl,
- Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap)
- {
- // Collect the yield predicates and desugar yields
- List> yields = new List>();
- List cmds = new List();
- foreach (Block b in impl.Blocks)
- {
- YieldCmd yieldCmd = null;
- List newCmds = new List();
- for (int i = 0; i < b.Cmds.Count; i++)
- {
- Cmd cmd = b.Cmds[i];
- if (cmd is YieldCmd)
- {
- yieldCmd = (YieldCmd)cmd;
- continue;
- }
- if (yieldCmd != null)
- {
- PredicateCmd pcmd = cmd as PredicateCmd;
- if (pcmd == null)
- {
- DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar);
- if (cmds.Count > 0)
- {
- yields.Add(cmds);
- cmds = new List();
- }
- yieldCmd = null;
- }
- else
- {
- cmds.Add(pcmd);
- }
- }
-
- if (cmd is CallCmd)
- {
- CallCmd callCmd = cmd as CallCmd;
- if (yieldingProcs.Contains(callCmd.Proc))
- {
- AddCallToYieldProc(callCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
- }
- if (callCmd.IsAsync)
- {
- if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name))
- {
- asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List(), new List());
- }
- var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];
- CallCmd dummyCallCmd = new CallCmd(callCmd.tok, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs, callCmd.Attributes);
- dummyCallCmd.Proc = dummyAsyncTargetProc;
- newCmds.Add(dummyCallCmd);
- }
- else
- {
- newCmds.Add(callCmd);
- }
- if (yieldingProcs.Contains(callCmd.Proc))
- {
- HashSet availableLinearVars = new HashSet(AvailableLinearVars(callCmd));
- linearTypeChecker.AddAvailableVars(callCmd, availableLinearVars);
-
- if (!callCmd.IsAsync && globalMods.Count > 0 && pc != null)
- {
- // assume pc || alpha(i, g);
- Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
- assumeExpr.Type = Type.Bool;
- newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
- }
-
- Dictionary domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
- AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
- }
- }
- else if (cmd is ParCallCmd)
- {
- ParCallCmd parCallCmd = cmd as ParCallCmd;
- AddCallToYieldProc(parCallCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
- DesugarParallelCallCmd(newCmds, parCallCmd);
- HashSet availableLinearVars = new HashSet(AvailableLinearVars(parCallCmd));
- linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars);
-
- if (globalMods.Count > 0 && pc != null)
- {
- // assume pc || alpha(i, g);
- Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
- assumeExpr.Type = Type.Bool;
- newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
- }
-
- Dictionary domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
- AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
- }
- else
- {
- newCmds.Add(cmd);
- }
- }
- if (yieldCmd != null)
- {
- DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar);
- if (cmds.Count > 0)
- {
- yields.Add(cmds);
- cmds = new List();
- }
- }
- if (b.TransferCmd is ReturnCmd)
- {
- AddCallToYieldProc(b.TransferCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
- if (pc != null)
- {
- AssertCmd assertCmd = new AssertCmd(b.TransferCmd.tok, Expr.Ident(ok));
- assertCmd.ErrorData = "Failed to execute atomic action before procedure return";
- newCmds.Add(assertCmd);
- }
- }
- b.Cmds = newCmds;
- }
- return yields;
- }
-
- private void ProcessLoopHeaders(Implementation impl, Graph graph, HashSet yieldingHeaders,
- Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap,
- out List oldPcs, out List oldOks)
- {
- oldPcs = new List();
- oldOks = new List();
- foreach (Block header in yieldingHeaders)
- {
- LocalVariable oldPc = null;
- LocalVariable oldOk = null;
- if (pc != null)
- {
- oldPc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", pc.Name, header.Label), Type.Bool));
- oldPcs.Add(oldPc);
- oldOk = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", ok.Name, header.Label), Type.Bool));
- oldOks.Add(oldOk);
- }
- Dictionary domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(header), domainNameToInputVar);
- foreach (Block pred in header.Predecessors)
- {
- AddCallToYieldProc(header.tok, pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);
- if (pc != null && !graph.BackEdgeNodes(header).Contains(pred))
- {
- pred.Cmds.Add(new AssignCmd(Token.NoToken, new List(
- new AssignLhs[] { new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)), new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)) }),
- new List(new Expr[] { Expr.Ident(pc), Expr.Ident(ok) })));
- }
- AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
- }
- List newCmds = new List();
- if (pc != null)
- {
- AssertCmd assertCmd;
- assertCmd = new AssertCmd(header.tok, Expr.Eq(Expr.Ident(oldPc), Expr.Ident(pc)));
- assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";
- newCmds.Add(assertCmd);
- assertCmd = new AssertCmd(header.tok, Expr.Imp(Expr.Ident(oldOk), Expr.Ident(ok)));
- assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";
- newCmds.Add(assertCmd);
- }
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));
- }
- foreach (Variable v in ogOldGlobalMap.Keys)
- {
- newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(v), Expr.Ident(ogOldGlobalMap[v]))));
- }
- newCmds.AddRange(header.Cmds);
- header.Cmds = newCmds;
- }
- }
-
- private void AddInitialBlock(Implementation impl, List oldPcs, List oldOks,
- Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap)
- {
- // Add initial block
- List lhss = new List();
- List rhss = new List();
- if (pc != null)
- {
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)));
- rhss.Add(Expr.False);
- foreach (Variable oldPc in oldPcs)
- {
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)));
- rhss.Add(Expr.False);
- }
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)));
- rhss.Add(Expr.False);
- foreach (Variable oldOk in oldOks)
- {
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)));
- rhss.Add(Expr.False);
- }
- }
- Dictionary domainNameToExpr = new Dictionary();
- foreach (var domainName in linearTypeChecker.linearDomains.Keys)
- {
- domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]);
- }
- for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
- {
- Variable v = impl.InParams[i];
- var domainName = linearTypeChecker.FindDomainName(v);
- if (domainName == null) continue;
- if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
- var domain = linearTypeChecker.linearDomains[domainName];
- if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;
- Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List { Expr.Ident(v) });
- domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { ie, domainNameToExpr[domainName] });
- }
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName])));
- rhss.Add(domainNameToExpr[domainName]);
- }
- foreach (Variable g in ogOldGlobalMap.Keys)
- {
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g])));
- rhss.Add(Expr.Ident(g));
- }
- if (lhss.Count > 0)
- {
- Block initBlock = new Block(Token.NoToken, "og_init", new List { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] }));
- impl.Blocks.Insert(0, initBlock);
- }
- }
-
- private void AddYieldProcAndImpl(List decls)
- {
- if (yieldProc == null) return;
-
- Program program = linearTypeChecker.program;
- List inputs = new List();
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- var domain = linearTypeChecker.linearDomains[domainName];
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List(), new List { domain.elementType }, Type.Bool)), true);
- inputs.Add(f);
- }
- foreach (IdentifierExpr ie in globalMods)
- {
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);
- inputs.Add(f);
- }
- List blocks = new List();
- TransferCmd transferCmd = new ReturnCmd(Token.NoToken);
- if (yieldCheckerProcs.Count > 0)
- {
- List blockTargets = new List();
- List labelTargets = new List();
- int labelCount = 0;
- foreach (Procedure proc in yieldCheckerProcs)
- {
- List