goto symex now handles function pointers

Author: kroening

src/goto-symex/goto_symex.h

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 
 class address_of_exprt;
 class code_function_callt;
+class dereference_exprt;
 class function_application_exprt;
 class goto_symex_statet;
 class path_storaget;
@@ -459,6 +460,20 @@ class goto_symext
     const symbol_exprt &function,
     const exprt::operandst &arguments);
 
+  /// Symbolic execution of a call to a function given via a pointer.
+  /// \param get_goto_function: The delegate to retrieve function bodies (see
+  ///   \ref get_goto_functiont)
+  /// \param state: Symbolic execution state for current instruction
+  /// \param lhs: nil or the lhs of the function call instruction
+  /// \param function: the dereference expression for the function to call
+  /// \param arguments: the arguments of the function call
+  virtual void symex_function_call_dereference(
+    const get_goto_functiont &get_goto_function,
+    statet &state,
+    const exprt &lhs,
+    const dereference_exprt &function,
+    const exprt::operandst &arguments);
+
   /// Symbolic execution of a function call by inlining.
   /// Records the call in \p target by appending a function call step and:
   ///   - if the body is available create a new frame, assigns the parameters,

src/goto-symex/symex_function_call.cpp

@@ -178,17 +178,26 @@ void goto_symext::symex_function_call(
 {
   const exprt &function = instruction.call_function();
 
-  // If at some point symex_function_call can support more
-  // expression ids(), like ID_Dereference, please expand the
-  // precondition appropriately.
-  PRECONDITION(function.id() == ID_symbol);
-
-  symex_function_call_symbol(
-    get_goto_function,
-    state,
-    instruction.call_lhs(),
-    to_symbol_expr(instruction.call_function()),
-    instruction.call_arguments());
+  PRECONDITION(function.id() == ID_symbol || function.id() == ID_dereference);
+
+  if(function.id() == ID_symbol)
+  {
+    symex_function_call_symbol(
+      get_goto_function,
+      state,
+      instruction.call_lhs(),
+      to_symbol_expr(function),
+      instruction.call_arguments());
+  }
+  else if(function.id() == ID_dereference)
+  {
+    symex_function_call_dereference(
+      get_goto_function,
+      state,
+      instruction.call_lhs(),
+      to_dereference_expr(function),
+      instruction.call_arguments());
+  }
 }
 
 void goto_symext::symex_function_call_symbol(
@@ -218,6 +227,19 @@ void goto_symext::symex_function_call_symbol(
     get_goto_function, state, cleaned_lhs, function, cleaned_arguments);
 }
 
+void goto_symext::symex_function_call_dereference(
+  const get_goto_functiont &get_goto_function,
+  statet &state,
+  const exprt &lhs,
+  const dereference_exprt &function,
+  const exprt::operandst &arguments)
+{
+  // need to clean the function pointer expression
+  auto cleaned_function = clean_expr(function, state, false);
+
+  // we get an if-then-else nest that contains symbols
+}
+
 void goto_symext::symex_function_call_post_clean(
   const get_goto_functiont &get_goto_function,
   statet &state,