new version from Vincent

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@1854 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/goto-instrument/Makefile

@@ -5,7 +5,10 @@ SRC = main.cpp parseoptions.cpp document_claims.cpp languages.cpp \
       weak_memory.cpp nondet_volatile.cpp interrupt.cpp \
       mmio.cpp stack_depth.cpp nondet_static.cpp \
       cfg_dominators.cpp natural_loops.cpp concurrency.cpp \
-      is_threaded.cpp dump_c.cpp dot.cpp
+      dump_c.cpp dot.cpp \
+      fence.cpp weak_memory.cpp\
+      event_graph.cpp goto2graph.cpp \
+      is_threaded.cpp
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
@@ -18,7 +21,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
 
 INCLUDES= -I .. -I ../util
 
-LIBS =
+LIBS = 
 
 CLEANFILES = goto-instrument$(EXEEXT)
 

src/goto-instrument/goto2graph.cpp

@@ -920,11 +920,15 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet& cyc)
   this_interleaving.function_map = map;
   optionst no_option;
   null_message_handlert no_message;
+  
+  #if 0
   bmct bmc(no_option, context, no_message);
 
   bool is_spurious = bmc.run(this_interleaving);
+  
   DEBUG_MESSAGE("CFG:"<<is_spurious);
   return is_spurious;
+  #endif
 }
 
 /*******************************************************************\

src/goto-instrument/parseoptions.cpp

@@ -186,7 +186,7 @@ int goto_instrument_parseoptionst::doit()
 
     if(cmdline.isset("interpreter"))
     {
-      status("Starting interpeter");
+      status("Starting interpreter");
       interpreter(context, goto_functions);
       return 0;
     }
@@ -225,13 +225,11 @@ int goto_instrument_parseoptionst::doit()
       return 0;
     }
 
-    // experimental: print structs
     if(cmdline.isset("show-struct-alignment"))
     {
       print_struct_alignment_problems(context, std::cout);
       return 0;
     }
-    // end of experiment
 
     if(cmdline.isset("show-locations"))
     {
@@ -426,6 +424,32 @@ void goto_instrument_parseoptionst::instrument_goto_program(
   if(cmdline.isset("error-label"))
     options.set_option("error-label", cmdline.getval("error-label"));
 
+  // unwind loops 
+  if(cmdline.isset("unwind"))
+  {
+    status("Unwinding loops");
+    options.set_option("unwind", cmdline.getval("unwind"));
+  }
+
+  // max number of variables in a cycle (default 0: no max)
+  if(cmdline.isset("max-var"))
+    options.set_option("max-var", cmdline.getval("max-var"));
+
+  // max number of transition by po (default 0: no limit)
+  if(cmdline.isset("max-po-trans"))
+    options.set_option("max-po-trans", cmdline.getval("max-po-trans"));
+
+  // strategy of instrumentation
+  if(cmdline.isset("one-event-per-cycle"))
+    options.set_option("event-strategy", 1);
+  else if(cmdline.isset("minimum-interference"))
+    options.set_option("event-strategy", 2);
+  else if(cmdline.isset("my-events"))
+    options.set_option("event-strategy", 3);
+  else
+    options.set_option("event-strategy", 0);
+
+ 
   namespacet ns(context);
 
   // add generic checks, if needed
@@ -465,7 +489,7 @@ void goto_instrument_parseoptionst::instrument_goto_program(
      cmdline.isset("race-check") ||
      cmdline.isset("tso") ||
      cmdline.isset("pso") ||
-     cmdline.isset("rso") ||
+     cmdline.isset("rmo") ||
      cmdline.isset("power") ||
      cmdline.isset("isr") ||
      cmdline.isset("concurrency"))
@@ -506,71 +530,95 @@ void goto_instrument_parseoptionst::instrument_goto_program(
         goto_functions);
     }
 
-    //const unsigned unwind_loops=
-    //  cmdline.isset("unwind")?options.get_int_option("unwind"):0;
+    const unsigned unwind_loops = 
+      ( cmdline.isset("unwind")?options.get_int_option("unwind"):0 );
+    const unsigned max_var =
+      ( cmdline.isset("max-var")?options.get_int_option("max-var"):0 );
+    const unsigned max_po_trans =
+      ( cmdline.isset("max-po-trans")?options.get_int_option("max-po-trans"):0 );
 
     if(cmdline.isset("tso"))
     {
-      #if 0
       status("Adding weak memory (TSO) Instrumentation");
       weak_memory(
         TSO,
         value_set_analysis,
         context,
         goto_functions,
-        cmdline.isset("one-partition"),
-        cmdline.isset("one-event-per-cycle"),
-        cmdline.isset("my-events"),
-        unwind_loops);
-      #endif
+        cmdline.isset("scc"),
+        options.get_int_option("event-strategy"),
+        unwind_loops,
+        !cmdline.isset("cfg-kill"),
+        cmdline.isset("no-dependencies"),
+        max_var,
+        max_po_trans,
+        !cmdline.isset("no-po-rendering"),
+        cmdline.isset("render-cluster-file"),
+        cmdline.isset("render-cluster-function"),
+        cmdline.isset("cav11"));
     }
 
     if(cmdline.isset("pso"))
     {
-      #if 0
       status("Adding weak memory (PSO) Instrumentation");
       weak_memory(
         PSO,
         value_set_analysis,
         context,
         goto_functions,
-        cmdline.isset("one-partition"),
-        cmdline.isset("one-event-per-cycle"),
-        cmdline.isset("my-events"),
-        unwind_loops);
-      #endif
+        cmdline.isset("scc"),
+        options.get_int_option("event-strategy"),
+        unwind_loops,
+        !cmdline.isset("cfg-kill"),
+        cmdline.isset("no-dependencies"),
+        max_var,
+        max_po_trans,
+        !cmdline.isset("no-po-rendering"),
+        cmdline.isset("render-cluster-file"),
+        cmdline.isset("render-cluster-function"),
+        cmdline.isset("cav11"));
     }
 
     if(cmdline.isset("rmo"))
     {
-      #if 0
       status("Adding weak memory (RMO) Instrumentation");
       weak_memory(
         RMO,
         value_set_analysis,
         context,
         goto_functions,
-        cmdline.isset("one-partition"),
-        cmdline.isset("one-event-per-cycle"),
-        cmdline.isset("my-events"),
-        unwind_loops);
-      #endif
+        cmdline.isset("scc"),
+        options.get_int_option("event-strategy"),
+        unwind_loops,
+        !cmdline.isset("cfg-kill"),
+        cmdline.isset("no-dependencies"),
+        max_var,
+        max_po_trans,
+        !cmdline.isset("no-po-rendering"),
+        cmdline.isset("render-cluster-file"),
+        cmdline.isset("render-cluster-function"),
+        cmdline.isset("cav11"));
     }
 
     if(cmdline.isset("power"))
     {
-      #if 0
       status("Adding weak memory (Power) Instrumentation");
       weak_memory(
         POWER,
         value_set_analysis,
         context,
         goto_functions,
-        cmdline.isset("one-partition"),
-        cmdline.isset("one-event-per-cycle"),
-        cmdline.isset("my-events"),
-        unwind_loops);
-      #endif
+        cmdline.isset("scc"),
+        options.get_int_option("event-strategy"),
+        unwind_loops,
+        !cmdline.isset("cfg-kill"),
+        cmdline.isset("no-dependencies"),
+        max_var,
+        max_po_trans,
+        !cmdline.isset("no-po-rendering"),
+        cmdline.isset("render-cluster-file"),
+        cmdline.isset("render-cluster-function"),
+        cmdline.isset("cav11"));
     }
 
     // Interrupt handler
@@ -602,7 +650,6 @@ void goto_instrument_parseoptionst::instrument_goto_program(
         context,
         goto_functions);
     }
-
   }  
 
   // add failed symbols
@@ -691,9 +738,26 @@ void goto_instrument_parseoptionst::help()
     "\n"
     "Semantic transformations:\n"
     " --nondet-volatile            makes reads from volatile variables non-deterministic\n"
+    " --unwind <n>                 unwinds the loops <n> times\n"
     " --isr function               instruments an interrupt service routine\n"
     " --mmio                       instruments memory-mapped I/O\n"
     " --nondet-static              add nondeterministic initialization of variables with static lifetime\n"
+    " --check-invariant function   instruments invariant checking function\n"
+    "\n"
+    "Memory model instrumentations:\n"
+    " --tso                        instruments weak memory models with buffers (TSO)\n"
+    " --pso                        instruments weak memory models with buffers (PSO)\n"
+    " --rmo                        instruments weak memory models with buffers (RMO)\n"
+    " --power                      instruments weak memory models with buffers and cache (Power)\n"
+    " --scc                        detects critical cycles per SCC (one thread per SCC)\n"
+    " --one-event-per-cycle        only instruments one event per cycle\n"
+    " --minimum-interference       instruments an optimal number of events\n"
+    " --my-events                  only instruments the events whose ids appear in inst.evt\n"
+    " --cfg-kill                   enables symbolic execution used to reduce spurious cycles\n"
+    " --no-dependencies            no dependency analysis\n"
+    " --no-po-rendering            no representation of the threads in the dot\n"
+    "  --render-cluster-file       clusterises the dot into files of the program"
+    "  --render-cluster-function   clusterises the dot into functions of the program" 
     "\n"
     "Slicing:\n"
     " --reachability-slicer        slice away instructions that can't reach assertions\n"