Merge pull request #795 from goblint/issue-792

Fix ARINC testing

Author: sim642

src/analyses/arinc.ml

@@ -26,7 +26,7 @@ module Functions = struct
   let ret_no_timeout = List.remove ret_any TIMED_OUT
   (* abstract value for return codes *)
   (* TODO: Check whether Cil.IInt is correct here *)
-  let vd ret = `Int (ValueDomain.ID.(List.map (of_int Cil.IInt % BI.of_int % return_code_to_enum) ret |> List.fold_left join (bot ()))) (* ana.int.enums should be enabled *)
+  let vd ret = `Int (ValueDomain.ID.(List.map (of_int Cil.IInt % BI.of_int % return_code_to_enum) ret |> List.fold_left join (bot_of IInt))) (* ana.int.enums should be enabled *)
   let effects fname args =
     if not (List.mem fname arinc_special) || List.is_empty args then None
     else

src/analyses/mutexEventsAnalysis.ml

@@ -73,6 +73,7 @@ struct
       ctx.emit (Events.Lock (verifier_atomic, true))
 
   let special (ctx: (unit, _, _, _) ctx) lv f arglist : D.t =
+    let is_activated a = List.mem a (GobConfig.get_string_list "ana.activated") in (* TODO: proper LibraryFunctions group selection *)
     let remove_rw x = x in
     let unlock remove_fn =
       match f.vname, arglist with
@@ -82,6 +83,11 @@ struct
             ctx.split () [Events.Unlock (remove_fn e)]
           ) (eval_exp_addr (Analyses.ask_of_ctx ctx) arg);
         raise Analyses.Deadcode
+      | "LAP_Se_SignalSemaphore", [Lval arg; _] when is_activated "arinc" || is_activated "extract_arinc" ->
+        List.iter (fun e ->
+            ctx.split () [Events.Unlock (remove_fn e)]
+          ) (eval_exp_addr (Analyses.ask_of_ctx ctx) (Cil.mkAddrOf arg));
+        raise Analyses.Deadcode
       | _ -> failwith "unlock has multiple arguments"
     in
     let desc = LF.find f in
@@ -96,6 +102,9 @@ struct
         | "spin_lock_irqsave", [arg; _] ->
           (*print_endline @@ "Mutex `Lock "^f.vname;*)
           lock ctx rw failing nonzero_return_when_aquired (Analyses.ask_of_ctx ctx) lv arg
+        | "LAP_Se_WaitSemaphore", [Lval arg; _; _] when is_activated "arinc" || is_activated "extract_arinc" ->
+          (*print_endline @@ "Mutex `Lock "^f.vname;*)
+          lock ctx rw failing nonzero_return_when_aquired (Analyses.ask_of_ctx ctx) lv (Cil.mkAddrOf arg)
         | _ -> failwith "lock has multiple arguments"
       end
     | Unlock _, "__raw_read_unlock"

tests/regression/17-arinc/01-sema.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] extract_arinc --set ana.activated[+] thread --set solver slr3 --disable ana.arinc.export
+// PARAM: --set ana.activated[+] arinc --set ana.activated[+] thread --set solver slr3 --disable ana.arinc.export
 
 typedef char * SEMAPHORE_NAME_TYPE;
 typedef int    SEMAPHORE_ID_TYPE;

tests/regression/17-arinc/02-unique_proc.c

@@ -1,4 +1,4 @@
-// NOMARSHAL PARAM: --set ana.activated[+] extract_arinc --set ana.activated[+] thread --set solver slr3t --disable ana.arinc.export
+// NOMARSHAL PARAM: --set ana.activated[+] arinc --set ana.activated[+] thread --set solver slr3t --disable ana.arinc.export
 
 typedef char * SEMAPHORE_NAME_TYPE;
 typedef int    SEMAPHORE_ID_TYPE;

tests/regression/17-arinc/03-preemt_lock.c

@@ -1,4 +1,6 @@
-// SKIP PARAM: --set ana.activated[+] extract_arinc --set ana.activated[+] thread --disable ana.arinc.export
+// SKIP PARAM: --set ana.activated[+] arinc --set ana.activated[+] thread --disable ana.arinc.export
+// probably doesn't pass because some preemption-based privatization was removed in b2fba1f43c402d3a3811502d6ea1079f22fe8d21
+#include <assert.h>
 
 typedef char * SEMAPHORE_NAME_TYPE;
 typedef int    SEMAPHORE_ID_TYPE;
@@ -60,7 +62,6 @@ extern void LAP_Se_SetPartitionMode (
 
 // -----------------------
 
-extern void assert(int);
 int g;
 
 void P1(void){
@@ -69,7 +70,7 @@ void P1(void){
   while (1){
      LAP_Se_LockPreemption(&ll,&r);
      g = 1;
-     assert(g==1);
+     assert(g==1); // TODO: privatization by preemption?
      LAP_Se_UnlockPreemption(&ll,&r);
   }
   return;

tests/regression/17-arinc/04-sema-strcpy.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] extract_arinc --set ana.activated[+] thread --set solver slr3 --disable ana.arinc.export
+// SKIP PARAM: --set ana.activated[+] arinc --set ana.activated[+] thread --set solver slr3 --disable ana.arinc.export
 
 typedef char * SEMAPHORE_NAME_TYPE;
 typedef int    SEMAPHORE_ID_TYPE;