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

Author: adpaco-aws

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 } => {

rust-tests/cbmc-reg/Count/Unstable/Ctlz/fixme_main_fail.rs rust-tests/cbmc-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;

rust-tests/cbmc-reg/Count/Unstable/Cttz/fixme_main_fail.rs rust-tests/cbmc-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;

rust-tests/cbmc-reg/Count/Unstable/Cttz/fixme_main.rs rust-tests/cbmc-reg/Count/Unstable/Cttz/main.rs

@@ -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

rust-tests/run.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