Complete count intrinsics codegen and testing (rust-lang#155)

celinval · May 28, 2021 · c05f711 · c05f711
1 parent 4debde2
commit c05f711
Show file tree

Hide file tree

Showing 6 changed files with 13 additions and 6 deletions.
diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/irep/to_irep.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/irep/to_irep.rs
@@ -278,15 +278,15 @@ impl ToIrep for ExprValue {
                 sub: vec![e.to_irep(mm)],
                 named_sub: btree_map![(
                     IrepId::CBoundsCheck,
-                    if *allow_zero { Irep::one() } else { Irep::zero() }
+                    if *allow_zero { Irep::zero() } else { Irep::one() }
                 )],
             },
             ExprValue::UnOp { op: UnaryOperand::CountTrailingZeros { allow_zero }, e } => Irep {
                 id: IrepId::CountTrailingZeros,
                 sub: vec![e.to_irep(mm)],
                 named_sub: btree_map![(
                     IrepId::CBoundsCheck,
-                    if *allow_zero { Irep::one() } else { Irep::zero() }
+                    if *allow_zero { Irep::zero() } else { Irep::one() }
                 )],
             },
             ExprValue::UnOp { op, e } => {

diff --git a/...eg/Count/Unstable/Ctlz/fixme_main_fail.rs → ...mc-reg/Count/Unstable/Ctlz/bounds_fail.rs b/...eg/Count/Unstable/Ctlz/fixme_main_fail.rs → ...mc-reg/Count/Unstable/Ctlz/bounds_fail.rs
@@ -3,6 +3,7 @@
 #![feature(core_intrinsics)]
 use std::intrinsics::ctlz_nonzero;
 
+/// rmc bounds_fail.rs -- --bounds-check
 fn main() {
     let uv8: u8 = 0;
     let uv16: u16 = 0;

diff --git a/...eg/Count/Unstable/Cttz/fixme_main_fail.rs → ...mc-reg/Count/Unstable/Cttz/bounds_fail.rs b/...eg/Count/Unstable/Cttz/fixme_main_fail.rs → ...mc-reg/Count/Unstable/Cttz/bounds_fail.rs
@@ -3,6 +3,7 @@
 #![feature(core_intrinsics)]
 use std::intrinsics::cttz_nonzero;
 
+/// rmc bounds_fail.rs -- --bounds-check
 fn main() {
     let uv8: u8 = 0;
     let uv16: u16 = 0;

diff --git a/...bmc-reg/Count/Unstable/Cttz/fixme_main.rs → ...ests/cbmc-reg/Count/Unstable/Cttz/main.rs b/...bmc-reg/Count/Unstable/Cttz/fixme_main.rs → ...ests/cbmc-reg/Count/Unstable/Cttz/main.rs
diff --git a/rust-tests/run.sh b/rust-tests/run.sh
@@ -23,7 +23,12 @@ for f in `find $TEST_DIR -name '*.rs'`; do
         continue
     fi
 
-    rmc $f -- --object-bits 11 --unwind $UNWIND > .sandbox/"$NAME".output
+    EXTRA_ARGS=""
+    if [[ "$f" == *bounds* ]]; then
+        EXTRA_ARGS+="--bounds-check"
+    fi
+
+    rmc $f -- --object-bits 11 --unwind $UNWIND $EXTRA_ARGS > .sandbox/"$NAME".output
 
     CODE=$?
     if [[ $CODE == 0 ]]; then

diff --git a/scripts/setup/ubuntu-20.04/install_cbmc.sh b/scripts/setup/ubuntu-20.04/install_cbmc.sh
@@ -4,7 +4,7 @@
 
 set -eux
 
-# Install CBMC 5.27 for Ubuntu 20.04
-wget https://github.com/diffblue/cbmc/releases/download/cbmc-5.27.0/ubuntu-20.04-cbmc-5.27.0-Linux.deb \
-  && sudo dpkg -i ubuntu-20.04-cbmc-5.27.0-Linux.deb \
+# Install CBMC 5.30.1 for Ubuntu 20.04
+wget https://github.com/diffblue/cbmc/releases/download/cbmc-5.30.1/ubuntu-20.04-cbmc-5.30.1-Linux.deb \
+  && sudo dpkg -i ubuntu-20.04-cbmc-5.30.1-Linux.deb \
   && cbmc --version