Vectorisation, loops, and division improvements

[katrinafyi]

From @ncough, to support arm-tv work.

[katrinafyi]

Looking at updating dune runtest and it looks like some extensions which were removed aren't anymore. For example add w2, w21, #1,

   "0x110006a2"
-  Stmt_Assign(LExpr_Array(LExpr_Var("_R"),2),Expr_TApply("ZeroExtend.0",[32;64],[Expr_TApply("add_bits.0",[32],[Expr_Slices(Expr_Array(Expr_Var("_R"),21),[Slice_LoWd(0,32)]);'00000000000000000000000000000001']);64]))
+  Stmt_Assign(LExpr_Array(LExpr_Var("_R"),2),Expr_TApply("ZeroExtend.0",[32;64],[Expr_Slices(Expr_TApply("add_bits.0",[64],[Expr_TApply("ZeroExtend.0",[32;64],[Expr_Slices(Expr_Array(Expr_Var("_R"),21),[Slice_LoWd(0,32)]);64]);'0000000000000000000000000000000000000000000000000000000000000001']),[Slice_LoWd(0,32)]);64]))

251bc09

[ncough]

IntToBits was disabled in the online lifter path, as it was leading to some stranger behaviours with the power-of-2 bitwidths. I have re-enabled it, along with fixes to the CaseSimp pass related to the bitwidths. This should correct issues with the larger bit vector expressions.

Also have a fix for the termination issues with offline, StatefulIntToBits was not converging on a fixed point due to a mistake in modelling integers.

[katrinafyi]

Thanks for the fixes. Let me know when you're happy with it and I'll merge it in.

[ncough]

I'm happy with it all, keen to see if it makes any difference. Thanks for cleaning up all of the integration mess!

[katrinafyi]

From a subset of the LLVM tests, there seems to be less timeouts and more correct outcomes!