instead of changing the drop-box

We need to work around the max execution time with refresh and offsetting

We're going to need to come up with some sort of testing strategy, since if we get the simplification rules wrong nothing will tell us, we will be silently and subtly wrong. One easy-ish thing to do is in a debug mode, accumulate guards WITHOUT any simplification, and when we pass a guard check, run through all of them to ensure that they are all satisfied. (I suppose we could also run through all of them when we fail a guard check too.) This will require some nontrivial Dynamo extra scaffolding.

But for the logic here, hmm, a good start would be to write manual test cases that trigger all of the branches in the logic here. That will at least give us confidence that it is not horribly wrong. Another possibility is to beef up debug checking inside the simplification code itself. For example, after we refine ranges, we can test some randomly sample some points (maybe deterministically sample points on the boundary of the ranges) and check that the ranges are consistent. IDK if @nunoplopes has some other ideas.

Agreed. A sort of translation validation would be great. You just need to check that the guards before and after simplification are equivalent. The problem is that sympy can't do that equivalence check, you would need Z3. And then we are back to the problem of do you want to go all in on Z3, do you want to have a translation between sympy and Z3 expressions and run translation validation only when Z3 is enabled.

Generating tests is also good, but since this code requires a sequence of bounds, it requires a lot of tests to trigger all cases. It's unlikely our generator would cover all cases. Hence the usefulness of the translation validation.

php 7 compat

github patch: check if branch exists

debug cron job for find github PRs

besides sending email on cron failure, also display them

fix call to array_unique

We have positives in GVN because of missing support for tail calls. see, e.g.: https://github.com/llvm/llvm-project/issues/61670 https://alive2.llvm.org/ce/z/GssD2L

define i64 @src(i64 noundef %arg) {
  %call2 = alloca i64
  %call3 = alloca i64
  store i64 %arg, ptr %call2, align 8
  tail call void @llvm.memcpy.p0.p0.i64(ptr %call3, ptr %call2, i64 8, i1 false)
  %load1 = load i64, ptr %call3, align 8
  ret i64 %load1
}

declare void @llvm.memcpy.p0.p0.i64(ptr noalias nocapture writeonly, ptr noalias nocapture readonly, i64, i1 immarg)

$ opt -p gvn
define i64 @src(i64 %arg) {
  %call2 = alloca i64, align 8
  %call3 = alloca i64, align 8
  store i64 %arg, ptr %call2, align 8
  tail call void @llvm.memcpy.p0.p0.i64(ptr %call3, ptr %call2, i64 8, i1 false)
  ret i64 undef
}

Perf test from John:

define ptr @src(ptr noundef %0, i64 noundef %1) {
2:
   %_t = trunc i64 %1 to i32
   %3 = getelementptr inbounds i8, ptr %0, i32 8
   store i32 %_t, ptr %3, align 4
   ret ptr %3
}

define ptr @tgt(ptr noundef %0, i64 noundef %1) {
i32_8:
   %2 = ptrtoint ptr %0 to i64
   %a0_38 = freeze i64 %1
   %a0_39 = trunc i64 %a0_38 to i32
   %a0_44 = add i64 %2, 8
   %3 = inttoptr i64 %a0_44 to ptr
   store i32 %a0_39, ptr %3, align 1
   ret ptr %3
}

TODO:

• link group to group's page
• In addition to patch's author, list student that submitted the patch (needs update to data model)

I am verifying a large scale software production in 64bit OS with 32G RAM, 3.39GHz and 3.40G Hz processors. It is beyond the ability of the z3. When I try the experiment in 64bit OS with 128G RAM with the same processors. The solver is still out of memory. So, the conclusion comes out: the memory is not the bottleneck for a large scale software. Another question appears: what is the real bottleneck of the solver? If a machine provide 1T RAM, whether it can increase the ability of formal verification?

Thanks

Z3 is solving a NP-hard problem (or worse), so it's normal it's slow. CPUs with more cache are usually faster, since the cache hit in SMT solvers is usually slow. But the solution to speed things up and reduce memory consumption lies in the frontend that produces these constraints. You've to optimize that. Z3 isn't magical. If you are verifying a large-scale production system I'm sure you've verification experts to help you with the tunning of the verification tool.

fix email_group: email of shift prof wasn't set properly

cron: don't commit to DB on error to avoid half-backed state

or a clickable link

php < 8 compat fix

make github_parse_date throw an exception on parse failure

fix ProjGroup::__toString()

Clang is now using it, which makes it more urgent to support this intrinsic. https://llvm.org/docs/LangRef.html#llvm-ptrmask-intrinsic

fix unit test (const select expr no longer exists in LLVM)

opt -enable-new-pm=0 is gone

We should allow opening up the form for a specific group only.

fix regression in LLVM unit test because align should be 64-bits repro: llvm/llvm/test/Transforms/InstCombine/deref-alloc-fns.ll