Merge pull request #1210 from goblint/longjmp-top

Fix longjmp crash on Uninitialized

src/analyses/base.ml

@@ -1231,9 +1231,16 @@ struct
               if copied then
                 M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a contains values that were copied here instead of being set by setjmp. This is Undefined Behavior." d_exp e;
               x
-            | y -> failwith (GobPretty.sprintf "problem?! is %a %a:\n state is %a" CilType.Exp.pretty e VD.pretty y D.pretty ctx.local)
+            | Top
+            | Bot ->
+              JmpBufDomain.JmpBufSet.top ()
+            | y ->
+              M.debug ~category:Imprecise "EvalJmpBuf %a is %a, not JmpBuf." CilType.Exp.pretty e VD.pretty y;
+              JmpBufDomain.JmpBufSet.top ()
           end
-        | _ -> failwith "problem?!"
+        | _ ->
+          M.debug ~category:Imprecise "EvalJmpBuf is not Address";
+          JmpBufDomain.JmpBufSet.top ()
       end
     | Q.EvalInt e ->
       query_evalint (Analyses.ask_of_ctx ctx) ctx.global ctx.local e

src/framework/constraints.ml

@@ -1663,7 +1663,8 @@ struct
         if M.tracing then Messages.tracel "longjmp" "Jumping to %a\n" JmpBufDomain.JmpBufSet.pretty targets;
         let handle_target target = match target with
           | JmpBufDomain.BufferEntryOrTop.AllTargets ->
-            M.warn ~category:Imprecise "Longjmp to potentially invalid target, as contents of buffer %a may be unknown! (imprecision due to heap?)" d_exp env
+            M.warn ~category:Imprecise "Longjmp to potentially invalid target, as contents of buffer %a may be unknown! (imprecision due to heap?)" d_exp env;
+            M.msg_final Error ~category:Unsound ~tags:[Category Imprecise; Category Call] "Longjmp to unknown target ignored"
           | Target (target_node, target_context) ->
             let target_fundec = Node.find_fundec target_node in
             if CilType.Fundec.equal target_fundec current_fundec && ControlSpecC.equal target_context (ctx.control_context ()) then (

tests/regression/68-longjmp/56-longjmp-top.c

@@ -0,0 +1,21 @@
+// Extracted from concrat/pigz.
+#include <setjmp.h>
+#include <pthread.h>
+#include <goblint.h>
+
+pthread_key_t buf_key;
+
+int main() {
+  jmp_buf buf;
+  pthread_setspecific(buf_key, &buf);
+
+  if (!setjmp(buf)) {
+    jmp_buf *buf_ptr;
+    buf_ptr = pthread_getspecific(buf_key);
+    longjmp(*buf_ptr, 1); // NO CRASH: problem?!
+  }
+  else {
+    __goblint_check(1); // TODO reachable: https://github.com/goblint/analyzer/pull/1210#discussion_r1350021903
+  }
+  return 0;
+}